Integral over a torus in ℂⁿ

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 torusMap (c : ℂⁿ) (R θ : ℝⁿ) to be the point in ℂⁿ given by $z_k=c_k+R_k{e}^{{\theta }_{k}i}$, where $i$ is the imaginary unit, then define torusIntegral f c R as the integral over the cube $[0,(fu{n}_{\mapsto }2\pi )]=\{\theta \Vert \forall k,0\le {\theta }_k\le 2\pi \}$ of the Jacobian of the torusMap multiplied by f (torusMap c R θ).

We also define a predicate saying that f ∘ torusMap c R is integrable on the cube [0, (fun _ ↦ 2π)].

Main definitions

• torusMap c R: the generalized multidimensional exponential map from ℝⁿ to ℂⁿ that sends $\theta =({\theta }_0,\dots ,{\theta }_{n-1})$ to $z=(z_0,\dots ,z_{n-1})$, where $z_k=c_k+R_k{e}^{{\theta }_{k}i}$;

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

• torusIntegral f c R: the integral of a function f : ℂⁿ → E over a torus with center c ∈ ℂⁿ and radius R ∈ ℝⁿ defined as ${\iiint }_{[0,2\ast \pi ]}({\prod }_{k=1}^{n}i{R}_k{e}^{{\theta }_k\ast i})•f(c+R{e}^{{\theta }_{k}i})d{\theta }_0\dots d{\theta }_{k-1}$.

Main statements

• torusIntegral_dim0, torusIntegral_dim1, torusIntegral_succ: formulas for torusIntegral 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 torusIntegral f c R;
• ∮ z in C(c, R), f z: notation for circleIntegral f c R, defined elsewhere;
• ∏ k, f k: notation for Finset.prod, defined elsewhere;
• π: notation for Real.pi, defined elsewhere.

Tags

integral, torus

torusMap, a parametrization of a torus

def torusMap {n : ℕ} (c : Fin n → ℂ) (R : Fin n → ℝ) : (Fin n → ℝ) → Fin n → ℂ

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

Equations

• torusMap c R θ i = c i + ↑(R i) * Complex.exp (↑(θ i) * Complex.I)

theorem torusMap_sub_center {n : ℕ} (c : Fin n → ℂ) (R : Fin n → ℝ) (θ : Fin n → ℝ) : torusMap c R θ - c = torusMap 0 R θ

theorem torusMap_eq_center_iff {n : ℕ} {c : Fin n → ℂ} {R : Fin n → ℝ} {θ : Fin n → ℝ} : torusMap c R θ = c ↔ R = 0

@[simp]

theorem torusMap_zero_radius {n : ℕ} (c : Fin n → ℂ) : torusMap c 0 = Function.const (Fin n → ℝ) c

Integrability of a function on a generalized torus

def TorusIntegrable {n : ℕ} {E : Type u_1} [NormedAddCommGroup E] (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 ∘ torusMap c R θ is integrable on Icc (0 : ℝⁿ) (fun _ ↦ 2 * π).

Equations

• TorusIntegrable f c R = MeasureTheory.IntegrableOn (fun (θ : Fin n → ℝ) => f (torusMap c R θ)) (Set.Icc 0 fun (x : Fin n) => 2 * Real.pi) MeasureTheory.volume

theorem TorusIntegrable.torusIntegrable_const {n : ℕ} {E : Type u_1} [NormedAddCommGroup E] (a : E) (c : Fin n → ℂ) (R : Fin n → ℝ) : TorusIntegrable (fun (x : Fin n → ℂ) => a) c R

Constant functions are torus integrable

theorem TorusIntegrable.neg {n : ℕ} {E : Type u_1} [NormedAddCommGroup E] {f : (Fin n → ℂ) → E} {c : Fin n → ℂ} {R : Fin n → ℝ} (hf : TorusIntegrable f c R) : TorusIntegrable (-f) c R

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

theorem TorusIntegrable.add {n : ℕ} {E : Type u_1} [NormedAddCommGroup E] {f : (Fin n → ℂ) → E} {g : (Fin n → ℂ) → E} {c : Fin n → ℂ} {R : Fin n → ℝ} (hf : TorusIntegrable f c R) (hg : TorusIntegrable g c R) : TorusIntegrable (f + g) c R

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

theorem TorusIntegrable.sub {n : ℕ} {E : Type u_1} [NormedAddCommGroup E] {f : (Fin n → ℂ) → E} {g : (Fin n → ℂ) → E} {c : Fin n → ℂ} {R : Fin n → ℝ} (hf : TorusIntegrable f c R) (hg : TorusIntegrable g c R) : TorusIntegrable (f - g) c R

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

theorem TorusIntegrable.torusIntegrable_zero_radius {n : ℕ} {E : Type u_1} [NormedAddCommGroup E] {f : (Fin n → ℂ) → E} {c : Fin n → ℂ} : TorusIntegrable f c 0

theorem TorusIntegrable.function_integrable {n : ℕ} {E : Type u_1} [NormedAddCommGroup E] {f : (Fin n → ℂ) → E} {c : Fin n → ℂ} {R : Fin n → ℝ} [NormedSpace ℂ E] (hf : TorusIntegrable f c R) : MeasureTheory.IntegrableOn (fun (θ : Fin n → ℝ) => (∏ i : Fin n, ↑(R i) * Complex.exp (↑(θ i) * Complex.I) * Complex.I) • f (torusMap c R θ)) (Set.Icc 0 fun (x : Fin n) => 2 * Real.pi) MeasureTheory.volume

The function given in the definition of torusIntegral is integrable.

def torusIntegral {n : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : (Fin n → ℂ) → E) (c : Fin n → ℂ) (R : Fin n → ℝ) : E

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

Equations

• torusIntegral f c R = ∫ (θ : Fin n → ℝ) in Set.Icc 0 fun (x : Fin n) => 2 * Real.pi, (∏ i : Fin n, ↑(R i) * Complex.exp (↑(θ i) * Complex.I) * Complex.I) • f (torusMap c R θ)

def «term∯_InT(_,_),_».delab : Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

Equations

• One or more equations did not get rendered due to their size.

def «term∯_InT(_,_),_» : Lean.ParserDescr

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

Equations

• One or more equations did not get rendered due to their size.

theorem torusIntegral_radius_zero {n : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (hn : n ≠ 0) (f : (Fin n → ℂ) → E) (c : Fin n → ℂ) : (∯ (x : Fin n → ℂ) in T(c, 0), f x) = 0

theorem torusIntegral_neg {n : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ 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 torusIntegral_add {n : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : (Fin n → ℂ) → E} {g : (Fin n → ℂ) → E} {c : Fin n → ℂ} {R : Fin n → ℝ} (hf : TorusIntegrable f c R) (hg : TorusIntegrable g c 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 torusIntegral_sub {n : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : (Fin n → ℂ) → E} {g : (Fin n → ℂ) → E} {c : Fin n → ℂ} {R : Fin n → ℝ} (hf : TorusIntegrable f c R) (hg : TorusIntegrable g c 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 torusIntegral_smul {n : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {𝕜 : Type u_2} [RCLike 𝕜] [NormedSpace 𝕜 E] [SMulCommClass 𝕜 ℂ 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 torusIntegral_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_torusIntegral_le_of_norm_le_const {n : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : (Fin n → ℂ) → E} {c : Fin n → ℂ} {R : Fin n → ℝ} {C : ℝ} (hf : ∀ (θ : Fin n → ℝ), ‖f (torusMap c R θ)‖ ≤ C) : ‖∯ (x : Fin n → ℂ) in T(c, R), f x‖ ≤ ((2 * Real.pi) ^ n * ∏ i : Fin n, |R i|) * C

If for all θ : ℝⁿ, ‖f (torusMap 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 torusIntegral_dim0 {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] (f : (Fin 0 → ℂ) → E) (c : Fin 0 → ℂ) (R : Fin 0 → ℝ) : (∯ (x : Fin 0 → ℂ) in T(c, R), f x) = f c

theorem torusIntegral_dim1 {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ 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 fun (x : Fin 1) => z

In dimension one, torusIntegral is the same as circleIntegral (up to the natural equivalence between ℂ and Fin 1 → ℂ).

theorem torusIntegral_succAbove {n : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : (Fin (n + 1) → ℂ) → E} {c : Fin (n + 1) → ℂ} {R : Fin (n + 1) → ℝ} (hf : TorusIntegrable f c 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.succAbove, R ∘ i.succAbove), f (i.insertNth x y)

Recurrent formula for torusIntegral, see also torusIntegral_succ.

theorem torusIntegral_succ {n : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : (Fin (n + 1) → ℂ) → E} {c : Fin (n + 1) → ℂ} {R : Fin (n + 1) → ℝ} (hf : TorusIntegrable f c R) : (∯ (x : Fin (n + 1) → ℂ) in T(c, R), f x) = ∮ (x : ℂ) in C(c 0, R 0), ∯ (y : Fin n → ℂ) in T(c ∘ Fin.succ, R ∘ Fin.succ), f (Fin.cons x y)

Recurrent formula for torusIntegral, see also torusIntegral_succAbove.