# mathlib3documentation

measure_theory.integral.torus_integral

# Integral over a torus in ℂⁿ#

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In this file we define the integral of a function f : ℂⁿ → E over a torus {z : ℂⁿ | ∀ i, z i ∈ metric.sphere (c i) (R i)}. In order to do this, we define torus_map (c : ℂⁿ) (R θ : ℝⁿ) to be the point in ℂⁿ given by $z_k=c_k+R_ke^{θ_ki}$, where $i$ is the imaginary unit, then define torus_integral f c R as the integral over the cube $[0, (λ _, 2π)] = \{θ\|∀ k, 0 ≤ θ_k ≤ 2π\}$ of the Jacobian of the torus_map multiplied by f (torus_map c R θ).

We also define a predicate saying that f ∘ torus_map c R is integrable on the cube [0, (λ _, 2\pi)].

## Main definitions #

• torus_map c R: the generalized multidimensional exponential map from ℝⁿ to ℂⁿ that sends $θ=(θ_0,…,θ_{n-1})$ to $z=(z_0,…,z_{n-1})$, where $z_k= c_k + R_ke^{θ_k i}$;

• torus_integrable f c R: a function f : ℂⁿ → E is integrable over the generalized torus with center c : ℂⁿ and radius R : ℝⁿ if f ∘ torus_map c R is integrable on the closed cube Icc (0 : ℝⁿ) (λ _, 2 * π);

• torus_integral f c R: the integral of a function f : ℂⁿ → E over a torus with center c ∈ ℂⁿ and radius R ∈ ℝⁿ defined as $\iiint_{[0, 2 * π]} (∏_{k = 1}^{n} i R_k e^{θ_k * i}) • f (c + Re^{θ_k i})\,dθ_0…dθ_{k-1}$.

## Main statements #

• torus_integral_dim0, torus_integral_dim1, torus_integral_succ: formulas for torus_integral in cases of dimension 0, 1, and n + 1.

## Notations #

• ℝ⁰, ℝ¹, ℝⁿ, ℝⁿ⁺¹: local notation for fin 0 → ℝ, fin 1 → ℝ, fin n → ℝ, and fin (n + 1) → ℝ, respectively;
• ℂ⁰, ℂ¹, ℂⁿ, ℂⁿ⁺¹: local notation for fin 0 → ℂ, fin 1 → ℂ, fin n → ℂ, and fin (n + 1) → ℂ, respectively;
• ∯ z in T(c, R), f z: notation for torus_integral f c R;
• ∮ z in C(c, R), f z: notation for circle_integral f c R, defined elsewhere;
• ∏ k, f k: notation for finset.prod, defined elsewhere;
• π: notation for real.pi, defined elsewhere.

## Tags #

integral, torus

### torus_map, a generalization of a torus #

noncomputable def torus_map {n : } (c : fin n ) (R : fin n ) :

The n dimensional exponential map $θ_i ↦ c + R e^{θ_i*I}, θ ∈ ℝⁿ$ representing a torus in ℂⁿ with center c ∈ ℂⁿ and generalized radius R ∈ ℝⁿ, so we can adjust it to every n axis.

Equations
theorem torus_map_sub_center {n : } (c : fin n ) (R θ : fin n ) :
R θ - c = R θ
theorem torus_map_eq_center_iff {n : } {c : fin n } {R θ : fin n } :
R θ = c R = 0
@[simp]
theorem torus_map_zero_radius {n : } (c : fin n ) :

### Integrability of a function on a generalized torus #

def torus_integrable {n : } {E : Type u_1} (f : (fin n ) E) (c : fin n ) (R : fin n ) :
Prop

A function f : ℂⁿ → E is integrable on the generalized torus if the function f ∘ torus_map c R θ is integrable on Icc (0 : ℝⁿ) (λ _, 2 * π)

Equations
theorem torus_integrable.torus_integrable_const {n : } {E : Type u_1} (a : E) (c : fin n ) (R : fin n ) :
torus_integrable (λ (_x : fin n ), a) c R

Constant functions are torus integrable

@[protected]
theorem torus_integrable.neg {n : } {E : Type u_1} {f : (fin n ) E} {c : fin n } {R : fin n } (hf : R) :
c R

If f is torus integrable then -f is torus integrable.

@[protected]
theorem torus_integrable.add {n : } {E : Type u_1} {f g : (fin n ) E} {c : fin n } {R : fin n } (hf : R) (hg : R) :

If f and g are two torus integrable functions, then so is f + g.

@[protected]
theorem torus_integrable.sub {n : } {E : Type u_1} {f g : (fin n ) E} {c : fin n } {R : fin n } (hf : R) (hg : R) :

If f and g are two torus integrable functions, then so is f - g.

theorem torus_integrable.torus_integrable_zero_radius {n : } {E : Type u_1} {f : (fin n ) E} {c : fin n } :
0
theorem torus_integrable.function_integrable {n : } {E : Type u_1} {f : (fin n ) E} {c : fin n } {R : fin n } [ E] (hf : R) :

The function given in the definition of torus_integral is integrable.

noncomputable def torus_integral {n : } {E : Type u_1} [ E] (f : (fin n ) E) (c : fin n ) (R : fin n ) :
E

The definition of the integral over a generalized torus with center c ∈ ℂⁿ and radius R ∈ ℝⁿ as the •-product of the derivative of torus_map and f (torus_map c R θ)

Equations
theorem torus_integral_radius_zero {n : } {E : Type u_1} [ E] (hn : n 0) (f : (fin n ) E) (c : fin n ) :
(x : fin n ) in T(c, 0), f x = 0
theorem torus_integral_neg {n : } {E : Type u_1} [ E] (f : (fin n ) E) (c : fin n ) (R : fin n ) :
(x : fin n ) in T(c, R), -f x = - (x : fin n ) in T(c, R), f x
theorem torus_integral_add {n : } {E : Type u_1} [ E] {f g : (fin n ) E} {c : fin n } {R : fin n } (hf : R) (hg : R) :
(x : fin n ) in T(c, R), f x + g x = ( (x : fin n ) in T(c, R), f x) + (x : fin n ) in T(c, R), g x
theorem torus_integral_sub {n : } {E : Type u_1} [ E] {f g : (fin n ) E} {c : fin n } {R : fin n } (hf : R) (hg : R) :
(x : fin n ) in T(c, R), f x - g x = ( (x : fin n ) in T(c, R), f x) - (x : fin n ) in T(c, R), g x
theorem torus_integral_smul {n : } {E : Type u_1} [ E] {𝕜 : Type u_2} [is_R_or_C 𝕜] [ E] [ E] (a : 𝕜) (f : (fin n ) E) (c : fin n ) (R : fin n ) :
(x : fin n ) in T(c, R), a f x = a (x : fin n ) in T(c, R), f x
theorem torus_integral_const_mul {n : } (a : ) (f : (fin n ) ) (c : fin n ) (R : fin n ) :
(x : fin n ) in T(c, R), a * f x = a * (x : fin n ) in T(c, R), f x
theorem norm_torus_integral_le_of_norm_le_const {n : } {E : Type u_1} [ E] {f : (fin n ) E} {c : fin n } {R : fin n } {C : } (hf : (θ : fin n ), f R θ) C) :
(x : fin n ) in T(c, R), f x (2 * real.pi) ^ n * finset.univ.prod (λ (i : fin n), |R i|) * C

If for all θ : ℝⁿ, ‖f (torus_map c R θ)‖ is less than or equal to a constant C : ℝ, then ‖∯ x in T(c, R), f x‖ is less than or equal to (2 * π)^n * (∏ i, |R i|) * C

@[simp]
theorem torus_integral_dim0 {E : Type u_1} [ E] (f : (fin 0 ) E) (c : fin 0 ) (R : fin 0 ) :
(x : fin 0 ) in T(c, R), f x = f c
theorem torus_integral_dim1 {E : Type u_1} [ E] (f : (fin 1 ) E) (c : fin 1 ) (R : fin 1 ) :
(x : fin 1 ) in T(c, R), f x = (z : ) in C(c 0, R 0), f (λ (_x : fin 1), z)

In dimension one, torus_integral is the same as circle_integral (up to the natural equivalence between ℂ and fin 1 → ℂ).

theorem torus_integral_succ_above {n : } {E : Type u_1} [ E] {f : (fin (n + 1) ) E} {c : fin (n + 1) } {R : fin (n + 1) } (hf : R) (i : fin (n + 1)) :
(x : fin (n + 1) ) in T(c, R), f x = (x : ) in C(c i, R i), (y : fin n ) in T(c (i.succ_above), R (i.succ_above)), f (i.insert_nth x y)

Recurrent formula for torus_integral, see also torus_integral_succ.

theorem torus_integral_succ {n : } {E : Type u_1} [ E] {f : (fin (n + 1) ) E} {c : fin (n + 1) } {R : fin (n + 1) } (hf : R) :
(x : fin (n + 1) ) in T(c, R), f x = (x : ) in C(c 0, R 0), (y : fin n ) in T(, ), f (fin.cons x y)

Recurrent formula for torus_integral, see also torus_integral_succ_above.