English
If x lies inside the radius-ball, then the series of p_n applied to x is summable.
Русский
Если x лежит внутри радиусной сферы, то сумма p_n(x) сходится по нормам.
LaTeX
$$$x \\in \\mathrm{EMetric.ball}(0, p.radius) \\Rightarrow \\sum_n \\|p_n(x)\\| < \\infty.$$$
Lean4
theorem comp_rightInv_aux1 {n : ℕ} (hn : 0 < n) (p : FormalMultilinearSeries 𝕜 E F) (q : FormalMultilinearSeries 𝕜 F E)
(v : Fin n → F) :
p.comp q n v =
∑ c ∈ {c : Composition n | 1 < c.length}.toFinset, p c.length (q.applyComposition c v) + p 1 fun _ => q n v :=
by
classical
have A :
(Finset.univ : Finset (Composition n)) = {c | 1 < Composition.length c}.toFinset ∪ {Composition.single n hn} :=
by
refine Subset.antisymm (fun c _ => ?_) (subset_univ _)
by_cases h : 1 < c.length
· simp [h]
· have : c.length = 1 := by refine (eq_iff_le_not_lt.2 ⟨?_, h⟩).symm; exact c.length_pos_of_pos hn
rw [← Composition.eq_single_iff_length hn] at this
simp [this]
have B : Disjoint ({c | 1 < Composition.length c} : Set (Composition n)).toFinset {Composition.single n hn} := by simp
have C :
p (Composition.single n hn).length (q.applyComposition (Composition.single n hn) v) = p 1 fun _ : Fin 1 => q n v :=
by
apply p.congr (Composition.single_length hn) fun j hj1 _ => ?_
simp [applyComposition_single]
simp [FormalMultilinearSeries.comp, A, Finset.sum_union B, C, -Set.toFinset_setOf, -add_right_inj,
-Composition.single_length, -Finset.union_singleton]
