Documentation

Mathlib.MeasureTheory.Integral.TorusIntegral

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_ke^{θ_ki}$, where $i$ is the imaginary unit, then define torusIntegral f c R as the integral over the cube $[0, (fun _ ↦ 2π)] = \{θ\|∀ k, 0 ≤ θ_k ≤ 2π\}$ 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 #

Main statements #

Notations #

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 $θ_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
Instances For
    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) :

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

    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
    Instances For
      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) :

      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} :
      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
      Instances For

        Pretty printer defined by notation3 command.

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

          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.
          Instances For
            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.