TorusIntegrable.torusIntegrable_const
theorem TorusIntegrable.torusIntegrable_const :
∀ {n : ℕ} {E : Type u_1} [inst : NormedAddCommGroup E] (a : E) (c : Fin n → ℂ) (R : Fin n → ℝ),
TorusIntegrable (fun x => a) c R
This theorem states that for any natural number `n`, any type `E` that forms a normed additive commutative group, any constant function `a : E`, and any functions `c : Fin n → ℂ` and `R : Fin n → ℝ`, the constant function is integrable on the generalized torus. In other words, the integrability of the composition of the constant function and a torus map (defined by `c` and `R`) over the interval from 0 to \(2\pi\) (for all components) is guaranteed.
More concisely: For any natural number `n`, any constant function `a : X` over a normed additive commutative group `X`, and functions `c : Fin n → ℝ` and `R : Fin n → ℝ`, the constant function is integrable over the generalized torus with parameter `(c, R)` on the interval `[0, 2π]`.
|
TorusIntegrable.neg
theorem TorusIntegrable.neg :
∀ {n : ℕ} {E : Type u_1} [inst : NormedAddCommGroup E] {f : (Fin n → ℂ) → E} {c : Fin n → ℂ} {R : Fin n → ℝ},
TorusIntegrable f c R → TorusIntegrable (-f) c R
The theorem `TorusIntegrable.neg` states that for any natural number `n`, any normed addition commutative group `E`, any function `f` mapping from a `n`-dimensional complex space to `E`, and any vectors `c` and `R` in `n`-dimensional complex and real space respectively, if `f` is torus integrable (i.e., the function `f` followed by the torus map with parameters `c` and `R` is integrable on the interval from `0` to `2π`), then the negation of `f`, denoted as `-f`, is also torus integrable.
More concisely: If a function from an n-dimensional complex space to a normed addition commutative group is torus integrable, then its negation is also torus integrable.
|
TorusIntegrable.sub
theorem TorusIntegrable.sub :
∀ {n : ℕ} {E : Type u_1} [inst : NormedAddCommGroup E] {f g : (Fin n → ℂ) → E} {c : Fin n → ℂ} {R : Fin n → ℝ},
TorusIntegrable f c R → TorusIntegrable g c R → TorusIntegrable (f - g) c R
The theorem `TorusIntegrable.sub` states that if we have two functions `f` and `g` that are torus integrable, meaning they are integrable when composed with the torus map, then the function obtained by subtracting `g` from `f` is also torus integrable. This applies for any complex values `c` and real values `R` which are used to define the torus map, and in any normed additive commutative group `E`. The dimensionality of the complex space is given by a natural number `n`.
More concisely: If `f` and `g` are torus integrable functions on a normed additive commutative group `E` of dimension `n` with respect to a complex number `c` and real value `R`, then `f - g` is also torus integrable.
|
torusIntegral_succAbove
theorem torusIntegral_succAbove :
∀ {n : ℕ} {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : (Fin (n + 1) → ℂ) → E}
{c : Fin (n + 1) → ℂ} {R : Fin (n + 1) → ℝ},
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)
This theorem, named `torusIntegral_succAbove`, establishes a recurrent formula for the `torusIntegral` function. Given a function `f` from complex vectors of size `n + 1` to some normed add-commutative group `E`, as well as complex vector `c` and real vector `R` (both also of size `n + 1`), if `f` is torus-integrable on the generalized torus mapped by `c` and `R`, then for any index `i` of size `n + 1`, the `torusIntegral` of `f` over the generalized torus `T(c, R)` equals the circular integral over circle `C(c i, R i)` of the `torusIntegral` of `f` over the generalized torus mapped by `i.succAbove` transformations of `c` and `R`, where the input to `f` is a vector constructed by inserting `x` at index `i` into vector `y`. The theorem thus describes a kind of decomposition of the `torusIntegral` into simpler integrals.
More concisely: Given a torus-integrable function `f` and complex vectors `c` and `R` of size `n+1`, the `torusIntegral` of `f` over the generalized torus `T(c, R)` equals the circular integral over each circle `C(ci, Ri)` of the `torusIntegral` of `f` over the generalized torus `T(i.succAbove . c, i.succAbove . R)`.
|
TorusIntegrable.function_integrable
theorem TorusIntegrable.function_integrable :
∀ {n : ℕ} {E : Type u_1} [inst : NormedAddCommGroup E] {f : (Fin n → ℂ) → E} {c : Fin n → ℂ} {R : Fin n → ℝ}
[inst_1 : NormedSpace ℂ E],
TorusIntegrable f c R →
MeasureTheory.IntegrableOn
(fun θ => (Finset.univ.prod fun i => ↑(R i) * (↑(θ i) * Complex.I).exp * Complex.I) • f (torusMap c R θ))
(Set.Icc 0 fun x => 2 * Real.pi) MeasureTheory.volume
This theorem states that for any natural number `n`, any type `E` that forms a Normed Additive Commutative Group, any function `f` from `ℂⁿ` to `E`, any `ℂⁿ` vector `c`, and any `ℝⁿ` vector `R` that forms a Normed Space over `ℂ` and `E`, if `f` is Torus Integrable for `c` and `R`, then the function, which maps `θ` to the scalar product of the function `f` evaluated at the torus map of `c`, `R` and `θ` and the product over all elements of `ℂⁿ` of the complex multiplication of `R i`, the exponential of the complex multiplication of `θ i` and the imaginary unit, and the imaginary unit, is integrable over the interval from `0` to `2π` with respect to the Lebesgue measure.
More concisely: For any Normed Additive Commutative Group `E`, any torus integrable function `f` from `ℂ^n` to `E`, any `ℝ^n` vector `R` forming a Normed Space over `ℂ` and `E`, the function mapping `θ` to the scalar product of `f(Exp(θ∘c)⊤R`, `I` \* Exp(θ) \* I, where `c` is in `ℂ^n`, `I` is the imaginary unit, and `θ` is in `[0, 2π]`, is integrable over `[0, 2π]` with respect to the Lebesgue measure.
|
norm_torusIntegral_le_of_norm_le_const
theorem norm_torusIntegral_le_of_norm_le_const :
∀ {n : ℕ} {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : (Fin n → ℂ) → E}
{c : Fin n → ℂ} {R : Fin n → ℝ} {C : ℝ},
(∀ (θ : Fin n → ℝ), ‖f (torusMap c R θ)‖ ≤ C) →
‖∯ (x : Fin n → ℂ) in T(c, R), f x‖ ≤ ((2 * Real.pi) ^ n * Finset.univ.prod fun i => |R i|) * C
The theorem `norm_torusIntegral_le_of_norm_le_const` states that for any positive integer `n`, any normed add comutative group `E` with a normed space over the complex numbers, any function `f` from `n`-tuples of complex numbers to `E`, any `n`-tuples `c` of complex numbers and `R` of real numbers, and any real constant `C`, if the norm of `f` composed with the torus map with parameters `c` and `R` applied to any `n`-tuple of real numbers `θ` is at most `C`, then the norm of the integral of `f` over the torus determined by `c` and `R` is at most the product of `(2 * pi)^n`, the product of the absolute values of the entries of `R`, and `C`. In other words, if a function's norm is bounded on the torus, then the norm of its integral over the torus is also bounded, with the bound depending on the dimension of the torus, the "radii" of the torus, and the original bound.
More concisely: For any normed additive commutative group E over the complex numbers, any function f from n-tuples of complex numbers to E, any real constants C and R with positive entries, and any n-tuple c of complex numbers, if the norm of f composed with the torus map with parameters c and R is bounded by C, then the norm of the integral of f over the n-dimensional complex torus with radii R is bounded by (2π)^n * C * ∏(R_i), where R_i denote the entries of R.
|
torusIntegral_dim1
theorem torusIntegral_dim1 :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : 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 => z
This theorem states that for functions in one dimension, the integral of the function over a torus (as computed by the `torusIntegral` function) is the same as the integral of the function over a circle (as computed by the `circleIntegral` function). This equivalence holds up to a natural equivalence between complex numbers `ℂ` and functions from `Fin 1` to `ℂ`. This applies for any function `f` from `Fin 1 → ℂ` to a certain type `E`, a complex number `c` which acts as the center of the circle/torus and a real number `R` which acts as the radius of the circle/torus. The theorem essentially asserts that in one dimension, integrating over a torus reduces to integrating over a circle.
More concisely: For any function `f : Fin 1 → ℂ`, the integral of `f` over a torus in one dimension, with center `c` and radius `R`, is equal to the integral of `f` over a circle in one dimension, with center `c` and radius `R`. (This equivalence holds up to the identification of complex numbers with functions from `Fin 1` to `ℂ`.)
|
TorusIntegrable.add
theorem TorusIntegrable.add :
∀ {n : ℕ} {E : Type u_1} [inst : NormedAddCommGroup E] {f g : (Fin n → ℂ) → E} {c : Fin n → ℂ} {R : Fin n → ℝ},
TorusIntegrable f c R → TorusIntegrable g c R → TorusIntegrable (f + g) c R
The theorem `TorusIntegrable.add` states that for any natural number `n` and any normed additive commutative group `E`, if `f` and `g` are two functions from `ℂⁿ` (a `n`-dimensional complex space) to `E` that are integrable on the generalized torus (meaning that the function composed with the torus map is integrable on the interval `[0, 2π]`), then the function `f + g` (the function obtained by pointwise addition of `f` and `g`) is also integrable on the generalized torus. This is under the assumption that the torus is characterized by complex numbers `c` and real numbers `R`.
More concisely: If `f` and `g` are integrable functions from `ℂⁿ` to a normed additive commutative group `E` with respect to the generalized torus `[0, 2π]^n` characterized by complex numbers `c` and real numbers `R`, then `f + g` is also integrable on this torus.
|
torusIntegral_succ
theorem torusIntegral_succ :
∀ {n : ℕ} {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : (Fin (n + 1) → ℂ) → E}
{c : Fin (n + 1) → ℂ} {R : Fin (n + 1) → ℝ},
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)
The theorem `torusIntegral_succ` is a recurrent formula for `torusIntegral`. It states that for any natural number `n`, and any normed add commutative group `E` which is also a normed space over the complex numbers, given a function `f` from `n+1`-tuples of complex numbers to `E`, and given `n+1`-tuples `c` and `R` of complex numbers and real numbers respectively, if `f` is integrable on the generalized torus (as defined by `TorusIntegrable`), then the torus integral of `f` over the torus `T(c, R)` equals the contour integral over the circle `C(c 0, R 0)` of the torus integral over the torus `T(c ∘ Fin.succ, R ∘ Fin.succ)` of `f` evaluated at the `n+1`-tuple formed by appending an element at the beginning of an `n`-tuple. This element is the variable of integration for the contour integral. In simpler terms, it breaks down the computation of a torus integral in `n+1` dimensions into a contour integral in one dimension and a torus integral in `n` dimensions.
More concisely: For any integrable function `f` on a generalized `n`-dimensional torus `T(c, R)` over a normed add commutative group `E` and for any `n+1` complex numbers `c` and real numbers `R`, the torus integral of `f` over `T(c, R)` equals the contour integral over the unit circle `C(1, 0)` of the torus integral of `f` over `T(c ∘ succ, R ∘ succ)`.
|