mathlib3 documentation

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 → ℝ) :

(fin n → ℝ) → 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

torus_map c R = λ (θ : fin n → ℝ) (i : fin n), c i + ↑(R i) * cexp (↑(θ i) * complex.I)

theorem torus_map_sub_center {n : ℕ} (c : fin n → ℂ) (R θ : fin n → ℝ) :

torus_map c R θ - c = torus_map 0 R θ

theorem torus_map_eq_center_iff {n : ℕ} {c : fin n → ℂ} {R θ : fin n → ℝ} :

torus_map c R θ = c ↔ R = 0

@[simp]

theorem torus_map_zero_radius {n : ℕ} (c : fin n → ℂ) :

torus_map c 0 = function.const (fin n → ℝ) c

Integrability of a function on a generalized torus #

def torus_integrable {n : ℕ} {E : Type u_1} [normed_add_comm_group 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 ∘ torus_map c R θ is integrable on Icc (0 : ℝⁿ) (λ _, 2 * π)

Equations

torus_integrable f c R = measure_theory.integrable_on (λ (θ : fin n → ℝ), f (torus_map c R θ)) (set.Icc 0 (λ (_x : fin n), 2 * real.pi)) measure_theory.measure_space.volume

theorem torus_integrable.torus_integrable_const {n : ℕ} {E : Type u_1} [normed_add_comm_group E] (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} [normed_add_comm_group E] {f : (fin n → ℂ) → E} {c : fin n → ℂ} {R : fin n → ℝ} (hf : torus_integrable f c R) :

torus_integrable (-f) c R

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

@[protected]

theorem torus_integrable.add {n : ℕ} {E : Type u_1} [normed_add_comm_group E] {f g : (fin n → ℂ) → E} {c : fin n → ℂ} {R : fin n → ℝ} (hf : torus_integrable f c R) (hg : torus_integrable g c R) :

torus_integrable (f + g) c 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} [normed_add_comm_group E] {f g : (fin n → ℂ) → E} {c : fin n → ℂ} {R : fin n → ℝ} (hf : torus_integrable f c R) (hg : torus_integrable g c R) :

torus_integrable (f - g) c 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} [normed_add_comm_group E] {f : (fin n → ℂ) → E} {c : fin n → ℂ} :

torus_integrable f c 0

theorem torus_integrable.function_integrable {n : ℕ} {E : Type u_1} [normed_add_comm_group E] {f : (fin n → ℂ) → E} {c : fin n → ℂ} {R : fin n → ℝ} [normed_space ℂ E] (hf : torus_integrable f c R) :

measure_theory.integrable_on (λ (θ : fin n → ℝ), finset.univ.prod (λ (i : fin n), ↑(R i) * cexp (↑(θ i) * complex.I) * complex.I) • f (torus_map c R θ)) (set.Icc 0 (λ (_x : fin n), 2 * real.pi)) measure_theory.measure_space.volume

The function given in the definition of torus_integral is integrable.

noncomputable def torus_integral {n : ℕ} {E : Type u_1} [normed_add_comm_group E] [normed_space ℂ E] [complete_space 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

torus_integral f c R = ∫ (θ : fin n → ℝ) in set.Icc 0 (λ (_x : fin n), 2 * real.pi), finset.univ.prod (λ (i : fin n), ↑(R i) * cexp (↑(θ i) * complex.I) * complex.I) • f (torus_map c R θ)

theorem torus_integral_radius_zero {n : ℕ} {E : Type u_1} [normed_add_comm_group E] [normed_space ℂ E] [complete_space 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} [normed_add_comm_group E] [normed_space ℂ E] [complete_space 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} [normed_add_comm_group E] [normed_space ℂ E] [complete_space E] {f g : (fin n → ℂ) → E} {c : fin n → ℂ} {R : fin n → ℝ} (hf : torus_integrable f c R) (hg : torus_integrable 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 torus_integral_sub {n : ℕ} {E : Type u_1} [normed_add_comm_group E] [normed_space ℂ E] [complete_space E] {f g : (fin n → ℂ) → E} {c : fin n → ℂ} {R : fin n → ℝ} (hf : torus_integrable f c R) (hg : torus_integrable 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 torus_integral_smul {n : ℕ} {E : Type u_1} [normed_add_comm_group E] [normed_space ℂ E] [complete_space E] {𝕜 : Type u_2} [is_R_or_C 𝕜] [normed_space 𝕜 E] [smul_comm_class 𝕜 ℂ 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} [normed_add_comm_group E] [normed_space ℂ E] [complete_space E] {f : (fin n → ℂ) → E} {c : fin n → ℂ} {R : fin n → ℝ} {C : ℝ} (hf : ∀ (θ : fin n → ℝ), ‖f (torus_map c 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} [normed_add_comm_group E] [normed_space ℂ E] [complete_space 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} [normed_add_comm_group E] [normed_space ℂ E] [complete_space 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} [normed_add_comm_group E] [normed_space ℂ E] [complete_space E] {f : (fin (n + 1) → ℂ) → E} {c : fin (n + 1) → ℂ} {R : fin (n + 1) → ℝ} (hf : torus_integrable 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.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} [normed_add_comm_group E] [normed_space ℂ E] [complete_space E] {f : (fin (n + 1) → ℂ) → E} {c : fin (n + 1) → ℂ} {R : fin (n + 1) → ℝ} (hf : torus_integrable 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 torus_integral, see also torus_integral_succ_above.