Composition.sizeUpTo_sizeUpTo_add
theorem Composition.sizeUpTo_sizeUpTo_add :
∀ {n : ℕ} (a : Composition n) (b : Composition a.length) {i j : ℕ} (hi : i < b.length),
j < b.blocksFun ⟨i, hi⟩ →
a.sizeUpTo (b.sizeUpTo i + j) = (a.gather b).sizeUpTo i + (a.sigmaCompositionAux b ⟨i, ⋯⟩).sizeUpTo j
This theorem, named `Composition.sizeUpTo_sizeUpTo_add`, states that for any natural number `n`, any composition `a` of `n`, any composition `b` of `a.length`, and for any natural numbers `i` and `j` such that `i` is less than `b.length` and `j` is less than the `i`th block size of `b`, the size up to `b.sizeUpTo i + j` in `a` is equal to the size up to `i` in `a.gather b` plus the size up to `j` in the next block of `a.sigmaCompositionAux b`. This lemma is used as an auxiliary step in proving that the composition of formal multilinear series is associative. It essentially describes how to compute the total size of certain blocks in a composition by adding together sizes from two different compositions.
More concisely: For any natural numbers `n`, `i`, `j`, and given compositions `a` of length `n` and `b` of length `a.length`, the size up to `b.sizeUpTo i + j` in `a` equals the size up to `i` in `a.gather b` plus the size up to `j` in the next block of `a.sigmaCompositionAux b`.
|
FormalMultilinearSeries.id_apply_one
theorem FormalMultilinearSeries.id_apply_one :
∀ (𝕜 : Type u_1) (E : Type u_2) [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] (v : Fin 1 → E), (FormalMultilinearSeries.id 𝕜 E 1) v = v 0
The theorem `FormalMultilinearSeries.id_apply_one` states that for any type 𝕜, which is a non-trivially normed field, and any type E, which is a normed additive commutative group and a normed space over 𝕜, the first coefficient of the identity formal multilinear series of 𝕜 and E (denoted as `FormalMultilinearSeries.id 𝕜 E 1`) applied to any function v from a 1-element finite set to E is equal to v at 0. In other words, the identity formal multilinear series of 𝕜 and E behaves like the identity function at the first coefficient.
More concisely: For any non-trivially normed field 𝕜 and normed additive commutative group/space E over 𝕜, the first coefficient of the identity formal multilinear series of 𝕜 and E applied to any function v from a 1-element set maps v at 0.
|
FormalMultilinearSeries.comp_coeff_one
theorem FormalMultilinearSeries.comp_coeff_one :
∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : CommRing 𝕜] [inst_1 : AddCommGroup E]
[inst_2 : AddCommGroup F] [inst_3 : AddCommGroup G] [inst_4 : Module 𝕜 E] [inst_5 : Module 𝕜 F]
[inst_6 : Module 𝕜 G] [inst_7 : TopologicalSpace E] [inst_8 : TopologicalSpace F] [inst_9 : TopologicalSpace G]
[inst_10 : TopologicalAddGroup E] [inst_11 : ContinuousConstSMul 𝕜 E] [inst_12 : TopologicalAddGroup F]
[inst_13 : ContinuousConstSMul 𝕜 F] [inst_14 : TopologicalAddGroup G] [inst_15 : ContinuousConstSMul 𝕜 G]
(q : FormalMultilinearSeries 𝕜 F G) (p : FormalMultilinearSeries 𝕜 E F) (v : Fin 1 → E),
(q.comp p 1) v = (q 1) fun _i => (p 1) v
This theorem states that for any formal multilinear series `p` and `q` defined over a commutative ring `𝕜` and topological vector spaces `E`, `F`, and `G`, the first coefficient of the composition of `p` and `q` is equal to the composition of the first coefficients of `p` and `q`. This composition is viewed as continuous linear maps. The input to this composition is a function `v` that maps a singleton (a finite set with one element) to `E`.
More concisely: For any commutative ring 𝕜 and topological vector spaces E, F, and G, the first coefficient of the composition of two formal multilinear series p and q, viewed as continuous linear maps, is equal to the composition of their first coefficients as functions mapping singletons to E.
|
Composition.sigma_composition_eq_iff
theorem Composition.sigma_composition_eq_iff :
∀ {n : ℕ} (i j : (a : Composition n) × Composition a.length),
i = j ↔ i.fst.blocks = j.fst.blocks ∧ i.snd.blocks = j.snd.blocks
This theorem, `Composition.sigma_composition_eq_iff`, states that for any natural number `n` and any two pairs of compositions `i` and `j`, where each pair consists of a composition of `n` and another composition of the length of the first composition, `i` is equal to `j` if and only if the blocks of the first compositions in `i` and `j` are equal and the blocks of the second compositions in `i` and `j` are also equal. Here, a composition refers to a way of writing `n` as a sum of positive integers, and the blocks are the positive integers in the sum.
More concisely: For natural numbers n and compositions i and j of length n, i = j if and only if the blocks of their first compositions (the positive integers in the sums) are equal and the blocks of their second compositions are equal.
|
FormalMultilinearSeries.comp_coeff_zero''
theorem FormalMultilinearSeries.comp_coeff_zero'' :
∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : CommRing 𝕜] [inst_1 : AddCommGroup E]
[inst_2 : AddCommGroup F] [inst_3 : Module 𝕜 E] [inst_4 : Module 𝕜 F] [inst_5 : TopologicalSpace E]
[inst_6 : TopologicalSpace F] [inst_7 : TopologicalAddGroup E] [inst_8 : ContinuousConstSMul 𝕜 E]
[inst_9 : TopologicalAddGroup F] [inst_10 : ContinuousConstSMul 𝕜 F] (q : FormalMultilinearSeries 𝕜 E F)
(p : FormalMultilinearSeries 𝕜 E E), q.comp p 0 = q 0
This theorem states that the `0`-th coefficient of the composition of two formal multilinear series `q` and `p` is equal to the `0`-th coefficient of `q`. This is true within the context of a commutative ring `𝕜` and two additively commutative groups `E` and `F` which are modules over `𝕜`. Both `E` and `F` are assumed to be topological spaces, topological additive groups, and equipped with scalar multiplication that is continuous with respect to `𝕜`. The series `q` maps from `E` to `F` and `p` maps from `E` to `E`. This theorem is essentially about the behavior of the composition of two formal multilinear series at the zeroth term.
More concisely: The theorem asserts that that the zero-th coefficient of the composition of two formal multilinear series `q` and `p` is equal to the zero-th coefficient of `q`, under the assumptions that `𝕜` is a commutative ring, `E` and `F` are topological additive groups modules over `𝕜`, both are topological spaces with continuous scalar multiplication, `q` maps from `E` to `F`, and `p` maps from `E` to `E`.
|
Composition.sigma_pi_composition_eq_iff
theorem Composition.sigma_pi_composition_eq_iff :
∀ {n : ℕ} (u v : (c : Composition n) × ((i : Fin c.length) → Composition (c.blocksFun i))),
u = v ↔ (List.ofFn fun i => (u.snd i).blocks) = List.ofFn fun i => (v.snd i).blocks
This theorem, `Composition.sigma_pi_composition_eq_iff`, states that for any natural number `n`, and for any two tuples `u` and `v` where each tuple consists of a composition of `n` and a function from a finite number `i` (with `i` less than the length of the composition) to a composition of the block at `i`, `u` and `v` are equal if and only if the lists of blocks of the compositions given by the functions in `u` and `v` are the same.
In other words, when we create a list from the blocks of each composition produced by the function in the tuples `u` and `v`, if these two lists are equal, then the tuples `u` and `v` themselves are equal and vice versa. This theorem links the concept of equality in dependent and non-dependent terms when dealing with compositions and lists of blocks.
More concisely: Given natural numbers n and tuples u and v of compositions of length n, u = v if and only if the lists of blocks in the compositions given by the functions in u and v are equal.
|
FormalMultilinearSeries.comp_summable_nnreal
theorem FormalMultilinearSeries.comp_summable_nnreal :
∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
[inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F]
[inst_4 : NormedSpace 𝕜 F] [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G]
(q : FormalMultilinearSeries 𝕜 F G) (p : FormalMultilinearSeries 𝕜 E F),
0 < q.radius → 0 < p.radius → ∃ r > 0, Summable fun i => ‖q.compAlongComposition p i.snd‖₊ * r ^ i.fst
The theorem `FormalMultilinearSeries.comp_summable_nnreal` asserts that if we have two formal multilinear series q and p, both with positive radius of convergence, then the terms in the definition of their composition are also summable. More specifically, these terms, when multiplied by a suitable positive geometric term, maintain the property of summability. This means there exists a positive real number r, such that the sum of the norms of the compositions of q along p, times r to the power of their index, exists. Here the norm ‖•‖₊ refers to the non-negative version of the norm, ensuring the output is a non-negative real number suitable for the summation in the definition of summability.
More concisely: Given two formal multilinear series q and p with positive radius of convergence in Lean 4, their composition terms, when multiplied by a suitable positive geometric term, have summable norms.
|
FormalMultilinearSeries.id_apply_one'
theorem FormalMultilinearSeries.id_apply_one' :
∀ (𝕜 : Type u_1) (E : Type u_2) [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] {n : ℕ} (h : n = 1) (v : Fin n → E), (FormalMultilinearSeries.id 𝕜 E n) v = v ⟨0, ⋯⟩
The theorem `FormalMultilinearSeries.id_apply_one'` states that for any nontrivially normed field `𝕜` and normed additive commutative group `E` that is also a normed space over `𝕜`, the nth coefficient of the formal multilinear series `id 𝕜 E` is the identity function when `n = 1`. More precisely, for any natural number `n` equal to 1 and any function `v` from a finite set of size `n` to `E`, the application of the nth coefficient of `id 𝕜 E` to `v` equals the value of `v` at the zeroth element.
More concisely: For any nontrivially normed field `𝕜` and normed additive commutative group `E` that is also a normed space over `𝕜`, the nth coefficient of the formal multilinear series `id 𝕜 E` is the identity function on `E` when `n = 1`. In other words, applying the first coefficient of `id 𝕜 E` to any finite sequence `v` of length 1 from `E` results in the value of `v` at the zero element of `E`.
|
FormalMultilinearSeries.removeZero_comp_of_pos
theorem FormalMultilinearSeries.removeZero_comp_of_pos :
∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : CommRing 𝕜] [inst_1 : AddCommGroup E]
[inst_2 : AddCommGroup F] [inst_3 : AddCommGroup G] [inst_4 : Module 𝕜 E] [inst_5 : Module 𝕜 F]
[inst_6 : Module 𝕜 G] [inst_7 : TopologicalSpace E] [inst_8 : TopologicalSpace F] [inst_9 : TopologicalSpace G]
[inst_10 : TopologicalAddGroup E] [inst_11 : ContinuousConstSMul 𝕜 E] [inst_12 : TopologicalAddGroup F]
[inst_13 : ContinuousConstSMul 𝕜 F] [inst_14 : TopologicalAddGroup G] [inst_15 : ContinuousConstSMul 𝕜 G]
(q : FormalMultilinearSeries 𝕜 F G) (p : FormalMultilinearSeries 𝕜 E F) {n : ℕ},
0 < n → q.removeZero.comp p n = q.comp p n
This theorem states that for any formal multilinear series `q` (a sequence of multilinear maps) on the fields `F` and `G`, and any formal multilinear series `p` on the fields `E` and `F`, if `n` is a positive natural number, then the `n`-th term in the composition of the `q.removeZero` (the series obtained by removing the zero-th term from `q`) with `p` is equal to the `n`-th term in the composition of `q` with `p`. So, only the zero-th term of the composition `q.comp p` depends on the zero-th term of `q`.
More concisely: For any multilinear series $q$ on fields $F$ and $G$, and multilinear series $p$ on fields $E$ and $F$, the $(n+1)$-th term of the composition $p \circ q$ equals the $n$-th term of the composition $(q \backslash 0) \circ p$, where $\backslash 0$ denotes the removal of the zeroth term from $q$.
|
AnalyticOn.comp'
theorem AnalyticOn.comp' :
∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
[inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F]
[inst_4 : NormedSpace 𝕜 F] [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {s : Set E} {g : F → G}
{f : E → F}, AnalyticOn 𝕜 g (f '' s) → AnalyticOn 𝕜 f s → AnalyticOn 𝕜 (g ∘ f) s
The theorem `AnalyticOn.comp'` states that for any type `𝕜` which is a nontrivially normed field, types `E`, `F`, and `G` which are normed add commutative groups and normed spaces over `𝕜`, a set `s` of type `E`, and functions `f: E → F` and `g: F → G`, if the function `g` is analytic on the image of `s` under `f`, and `f` is analytic on `s`, then the composition of `g` and `f` (denoted `g ∘ f`) is analytic on `s`. In other words, the analyticity of `f` and `g` is preserved under their composition.
More concisely: If `𝕜` is a nontrivially normed field, `f: E → F` and `g: F → G` are analytic functions with `E`, `F`, and `G` being normed add commutative groups and normed spaces over `𝕜`, and `s` is a subset of `E`, then the composition `g ∘ f` is analytic on `s` if both `f` and `g` are analytic on `s`.
|
FormalMultilinearSeries.applyComposition_update
theorem FormalMultilinearSeries.applyComposition_update :
∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : CommRing 𝕜] [inst_1 : AddCommGroup E]
[inst_2 : AddCommGroup F] [inst_3 : Module 𝕜 E] [inst_4 : Module 𝕜 F] [inst_5 : TopologicalSpace E]
[inst_6 : TopologicalSpace F] [inst_7 : TopologicalAddGroup E] [inst_8 : ContinuousConstSMul 𝕜 E]
[inst_9 : TopologicalAddGroup F] [inst_10 : ContinuousConstSMul 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) {n : ℕ}
(c : Composition n) (j : Fin n) (v : Fin n → E) (z : E),
p.applyComposition c (Function.update v j z) =
Function.update (p.applyComposition c v) (c.index j)
((p (c.blocksFun (c.index j))) (Function.update (v ∘ ⇑(c.embedding (c.index j))) (c.invEmbedding j) z))
The theorem `FormalMultilinearSeries.applyComposition_update` states that for any formal multilinear series `p` over fields `𝕜`, source type `E` and target type `F`, with given structures, any composition `c` of a natural number `n`, an index `j` from a finite set of size `n`, a function `v` from this finite set to `E`, and a value `z` in `E`, the result of applying the composition `c` to the function `v` updated at `j` with `z`, is equal to updating the result of applying the composition `c` to `v` at the index corresponding to `j` in `c`, with the result of applying the `p` to the block of `c` corresponding to `j`, evaluated at the function obtained by updating `v` composed with the embedding of `c` at `c.index j` with `z` at the index `c.invEmbedding j`. This lemma is a crucial step in proving that functions constructed from `apply_composition` retain multilinearity.
More concisely: For any formal multilinear series `p` and composition `c` over a field, the result of updating the application of `c` to a function `v` at index `j` with `z`, is equal to updating the application of `c` to `v` at index `j` with the evaluation of `p` on the composition `c` and the updated function `v`.
|
FormalMultilinearSeries.comp_coeff_zero
theorem FormalMultilinearSeries.comp_coeff_zero :
∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : CommRing 𝕜] [inst_1 : AddCommGroup E]
[inst_2 : AddCommGroup F] [inst_3 : AddCommGroup G] [inst_4 : Module 𝕜 E] [inst_5 : Module 𝕜 F]
[inst_6 : Module 𝕜 G] [inst_7 : TopologicalSpace E] [inst_8 : TopologicalSpace F] [inst_9 : TopologicalSpace G]
[inst_10 : TopologicalAddGroup E] [inst_11 : ContinuousConstSMul 𝕜 E] [inst_12 : TopologicalAddGroup F]
[inst_13 : ContinuousConstSMul 𝕜 F] [inst_14 : TopologicalAddGroup G] [inst_15 : ContinuousConstSMul 𝕜 G]
(q : FormalMultilinearSeries 𝕜 F G) (p : FormalMultilinearSeries 𝕜 E F) (v : Fin 0 → E) (v' : Fin 0 → F),
(q.comp p 0) v = (q 0) v'
This theorem asserts that for two formal multilinear series `p` and `q`, when you compose `q` with `p` and look at the `0`-th coefficient, it equals to the `0`-th coefficient of `q` itself. This is stated in a somewhat convoluted way due to the fact that these are multilinear maps in zero variables, but on different spaces. Therefore, we can't state it directly, so it's stated when applied to arbitrary vectors, which must be zero vectors.
More concisely: The theorem asserts that the coefficient of the zero vector in the product of two multilinear series is equal to the coefficient of the zero vector in the second series.
|
FormalMultilinearSeries.compChangeOfVariables_sum
theorem FormalMultilinearSeries.compChangeOfVariables_sum :
∀ {α : Type u_6} [inst : AddCommMonoid α] (m M N : ℕ) (f : (n : ℕ) × (Fin n → ℕ) → α)
(g : (n : ℕ) × Composition n → α),
(∀ (e : (n : ℕ) × (Fin n → ℕ)) (he : e ∈ FormalMultilinearSeries.compPartialSumSource m M N),
f e = g (FormalMultilinearSeries.compChangeOfVariables m M N e he)) →
((FormalMultilinearSeries.compPartialSumSource m M N).sum fun e => f e) =
(FormalMultilinearSeries.compPartialSumTarget m M N).sum fun e => g e
The theorem `FormalMultilinearSeries.compChangeOfVariables_sum` states that the function `compChangeOfVariables` is essentially a bijection (though not directly, as the function is dependent) between the sets `compPartialSumSource m M N` and `compPartialSumTarget m M N`. More specifically, for any two functions `f` and `g` from these sets to an additive commutative monoid `α`, if every element `e` in `compPartialSumSource m M N` maps under `f` to the same value as it does under `g` composed with `compChangeOfVariables`, then the sum over `compPartialSumSource m M N` under `f` is equal to the sum over `compPartialSumTarget m M N` under `g`. This essentially captures the property that the bijection preserves the sum operation.
More concisely: If `f` and `g` agree on the images of elements in `compPartialSumSource m M N` under `compChangeOfVariables`, then the sum of `f` over `compPartialSumSource m M N` equals the sum of `g` over `compPartialSumTarget m M N`.
|
FormalMultilinearSeries.compAlongComposition_norm
theorem FormalMultilinearSeries.compAlongComposition_norm :
∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
[inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F]
[inst_4 : NormedSpace 𝕜 F] [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {n : ℕ}
(q : FormalMultilinearSeries 𝕜 F G) (p : FormalMultilinearSeries 𝕜 E F) (c : Composition n),
‖q.compAlongComposition p c‖ ≤ ‖q c.length‖ * Finset.univ.prod fun i => ‖p (c.blocksFun i)‖
This theorem states that for any nontrivially normed field `𝕜`, normed add-commutative groups `E`, `F`, and `G`, and normed vector spaces over `𝕜` for `E`, `F`, and `G`, given natural number `n` and formal multilinear series `q` and `p`, the norm of the composition of `q` along `p` and a composition `c` of `n` is less than or equal to the product of the norm of `q` at the length of `c` and the product of the norms of `p` at the function value of the composition blocks of `c`, taken over all elements in the universal set of `c`'s blocks.
More concisely: For any nontrivially normed field `𝕜`, normed add-commutative groups `E`, `F`, `G`, and normed vector spaces `V`, `W`, `X` over `𝕜` for `E`, `F`, `G`, and a natural number `n`, formal multilinear series `q : V ⊎ ... ⊎ X → W` and `p : (A → E) → F`, and a composition `c : (A^n) → A`, we have `‖q ∘ p ∘ c‖ ≤ ‖q‖(length c) * ∏ (i : ℕ) ‖p (c ! 𝟙 i)‖`, where `A` is the universal set of `c`'s blocks.
|
FormalMultilinearSeries.comp_partialSum
theorem FormalMultilinearSeries.comp_partialSum :
∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
[inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F]
[inst_4 : NormedSpace 𝕜 F] [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G]
(q : FormalMultilinearSeries 𝕜 F G) (p : FormalMultilinearSeries 𝕜 E F) (N : ℕ) (z : E),
q.partialSum N ((Finset.Ico 1 N).sum fun i => (p i) fun _j => z) =
(FormalMultilinearSeries.compPartialSumTarget 0 N N).sum fun i =>
(q.compAlongComposition p i.snd) fun _j => z
This theorem states that for any nontrivially normed field `𝕜`, normed addition-commutative groups `E`, `F`, `G` and normed spaces `E`, `F`, `G` over `𝕜`, and for any formal multilinear series `q` from `F` to `G`, `p` from `E` to `F`, any natural number `N` and any element `z` of `E`, the partial sum of the series `q` up to the `N`th term, evaluated at the sum of series `p` (from `1` to `N`) evaluated at `z`, is equal to the sum over all compositions in the target set of the composition of partial sums from `0` to `N`, where each term is the composition of `q` along the composition `p` evaluated at `z`.
This theorem is the reason for the definition of the function `FormalMultilinearSeries.compPartialSumTarget`. It essentially states that composing the partial sums of two multilinear series coincides with the sum over all compositions in a certain target set.
More concisely: For any nontrivially normed field `𝕜`, normed addition-commutative groups `E`, `F`, `G`, and normed spaces `E`, `F`, `G` over `𝕜`, and for any formal multilinear series `q` from `F` to `G` and `p` from `E` to `F`, the partial sum of `q` composed with the partial sum of `p` evaluated at an element `z` in `E` is equal to the sum of all compositions of `q` along `p` evaluated at `z`.
|
Composition.length_gather
theorem Composition.length_gather :
∀ {n : ℕ} (a : Composition n) (b : Composition a.length), (a.gather b).length = b.length
The `Composition.length_gather` theorem states that for any natural number `n` and any composition `a` of `n`, if `b` is a composition of the length of `a`, then the length of the composition formed by gathering all the blocks of `a` corresponding to a block of `b` (`Composition.gather a b`) is equal to the length of `b`. In other words, the act of gathering blocks according to another composition does not change the number of blocks in the composition.
More concisely: For any natural numbers `n` and compositions `a` and `b` of `n` with `b` being a block of `a`, the length of the composition obtained by gathering all blocks of `a` corresponding to `b` is equal to the length of `b`.
|
FormalMultilinearSeries.le_comp_radius_of_summable
theorem FormalMultilinearSeries.le_comp_radius_of_summable :
∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
[inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F]
[inst_4 : NormedSpace 𝕜 F] [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G]
(q : FormalMultilinearSeries 𝕜 F G) (p : FormalMultilinearSeries 𝕜 E F) (r : NNReal),
(Summable fun i => ‖q.compAlongComposition p i.snd‖₊ * r ^ i.fst) → ↑r ≤ (q.comp p).radius
The theorem `FormalMultilinearSeries.le_comp_radius_of_summable` states that for any nonnegative real number `r`, and any two formal multilinear series `p` (from a normed space over a field `𝕜` to another normed space) and `q` (from the latter normed space to a third normed space), if the series comprising the norm of the composition of `q` and `p` along any composition `i`, multiplied by `r` raised to the power of the first component of `i`, is summable, then `r` is less than or equal to the radius of the composition of `q` and `p`. In simpler terms, it provides a lower bound of the radius of the composition of two formal multilinear series provided that a certain series is summable.
More concisely: If the series representing the norm of the composition of two formal multilinear series, when weighted by the first component of the composition index and summed over all compositions, is summable, then the radius of the composition is less than or equal to the weight.
|
HasFPowerSeriesAt.comp
theorem HasFPowerSeriesAt.comp :
∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
[inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F]
[inst_4 : NormedSpace 𝕜 F] [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {g : F → G} {f : E → F}
{q : FormalMultilinearSeries 𝕜 F G} {p : FormalMultilinearSeries 𝕜 E F} {x : E},
HasFPowerSeriesAt g q (f x) → HasFPowerSeriesAt f p x → HasFPowerSeriesAt (g ∘ f) (q.comp p) x
This theorem states that if we have two functions `g` and `f` where `g` has a power series `q` at point `f(x)` and `f` has a power series `p` at point `x`, then the composition of `g` and `f` (i.e., `g ∘ f`) admits the power series `q.comp p` at the same point `x`. This is under the context where `𝕜` is a nontrivial normed field, `E`, `F`, `G` are all normed spaces over `𝕜`, and `g` is a function from `F` to `G` and `f` is a function from `E` to `F`. Here, `q` is a formal multilinear series from `F` to `G` and `p` is a formal multilinear series from `E` to `F`.
More concisely: If functions `g : F -> G` and `f : E -> F` have power series `q` and `p` at `x` and `f(x)`, respectively, then `g ∘ f` has the power series `q.comp p` at point `x`.
|
FormalMultilinearSeries.compAlongComposition_bound
theorem FormalMultilinearSeries.compAlongComposition_bound :
∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
[inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F]
[inst_4 : NormedSpace 𝕜 F] [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {n : ℕ}
(p : FormalMultilinearSeries 𝕜 E F) (c : Composition n) (f : ContinuousMultilinearMap 𝕜 (fun _i => F) G)
(v : Fin n → E),
‖(ContinuousMultilinearMap.compAlongComposition p c f) v‖ ≤
(‖f‖ * Finset.univ.prod fun i => ‖p (c.blocksFun i)‖) * Finset.univ.prod fun i => ‖v i‖
This theorem, `FormalMultilinearSeries.compAlongComposition_bound`, states that for any nontrivially normed field `𝕜`, normed add commutative groups `E`, `F`, and `G`, and normed spaces over `𝕜` of `E`, `F`, and `G`, given a formal multilinear series `p` from `𝕜` and `E` to `F`, a composition `c` of a natural number `n`, a continuous multilinear map `f` from `𝕜` and `F` to `G`, and a function `v` from the finite set of `n` to `E`, the norm of the composition of `f` along the composition `p` and `c` evaluated at `v` is less than or equal to the product of the norm of `f` and the product of norms of `p` over the blocks of `c`, all multiplied by the product of norms of `v` over all elements of the finite set of `n`. This theorem provides a bound on the norm of the composition of a continuous multilinear map and a formal multilinear series.
More concisely: For any nontrivially normed field `𝕜`, normed add commutative groups `E`, `F`, and `G`, and normed spaces over `𝕜` of `E`, `F`, and `G`, given a continuous multilinear map `f` from `𝕜` and `F` to `G`, a formal multilinear series `p` from `𝕜` and `E` to `F`, a composition `c` of a natural number `n`, and a function `v` from the finite set of `n` to `E`, the norm of `f ∘ p ∘ c (v)` is less than or equal to the product of the norm of `f`, the product of norms of `p` over the blocks of `c`, and the product of norms of `v` over all elements of the finite set `n`.
|
FormalMultilinearSeries.id_apply_ne_one
theorem FormalMultilinearSeries.id_apply_ne_one :
∀ (𝕜 : Type u_1) (E : Type u_2) [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] {n : ℕ}, n ≠ 1 → FormalMultilinearSeries.id 𝕜 E n = 0
This theorem states that for any nontrivially normed field `𝕜` and a normed additive commutative group `E` that is also a normed space over `𝕜`, the `n`-th coefficient of the identity formal multilinear series (which is a series where all coefficients are zero except for `n = 1` where it is the identity) is zero if `n` is not equal to one.
More concisely: For any nontrivially normed field `𝕜` and normed additive commutative group `E` over `𝕜` as a normed space, the identity formal multilinear series has zero `n`-th coefficient for `n > 1`.
|
FormalMultilinearSeries.compPartialSumTarget_tendsto_atTop
theorem FormalMultilinearSeries.compPartialSumTarget_tendsto_atTop :
Filter.Tendsto (fun N => FormalMultilinearSeries.compPartialSumTarget 0 N N) Filter.atTop Filter.atTop
This theorem states that the auxiliary set, which corresponds to the composition of partial sums, asymptotically contains all possible compositions. In more detail, as N goes to infinity (`Filter.atTop`), the set obtained by composing partial sums from 0 to N (`FormalMultilinearSeries.compPartialSumTarget 0 N N`) also tends to include all possible compositions (also indicated by `Filter.atTop`). In mathematical terms, this is expressing that the function mapping N to the set of compositions of partial sums from 0 to N has a limit of including all possible compositions as N approaches infinity.
More concisely: As N approaches infinity, the set of compositions obtained by composing partial sums from 0 to N includes all possible compositions.
|
AnalyticAt.comp
theorem AnalyticAt.comp :
∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
[inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F]
[inst_4 : NormedSpace 𝕜 F] [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {g : F → G} {f : E → F}
{x : E}, AnalyticAt 𝕜 g (f x) → AnalyticAt 𝕜 f x → AnalyticAt 𝕜 (g ∘ f) x
The theorem `AnalyticAt.comp` states that if we have two functions `g` and `f` which are analytic at the points `f(x)` and `x` respectively, then the composition of `g` and `f` (denoted by `g ∘ f`) is also analytic at the point `x`. Here, a function is said to be analytic at a point if it can be written as a convergent power series around that point. This theorem is defined over a non-trivially normed field `𝕜`, and the function `f` maps from a normed vector space `E` over `𝕜` to another normed vector space `F` over `𝕜`, while `g` maps from `F` to yet another normed vector space `G` over `𝕜`.
More concisely: If functions `f: E → F` and `g: F → G` are analytic at points `x` and `f(x)` respectively over a non-trivially normed field `𝕜`, then their composition `g ∘ f` is analytic at point `x`.
|