English
In the inverse construction, the radius is bounded below by the growth bound of the right inverse.
Русский
При построении обратной величины радиус ограничен снизу по границе роста правой обратной карты.
LaTeX
$$$\\text{radius bounds for rightInv under growth control}$$$
Lean4
theorem rightInv_coeff (p : FormalMultilinearSeries 𝕜 E F) (i : E ≃L[𝕜] F) (x : E) (n : ℕ) (hn : 2 ≤ n) :
p.rightInv i x n =
-(i.symm : F →L[𝕜] E).compContinuousMultilinearMap
(∑ c ∈ ({c | 1 < Composition.length c}.toFinset : Finset (Composition n)),
p.compAlongComposition (p.rightInv i x) c) :=
by
match n with
| 0 => exact False.elim (zero_lt_two.not_ge hn)
| 1 => exact False.elim (one_lt_two.not_ge hn)
| n + 2 =>
simp only [rightInv, neg_inj]
congr (config := { closePost := false }) 1
ext v
have N : 0 < n + 2 := by simp
have : ((p 1) fun _ : Fin 1 => 0) = 0 := ContinuousMultilinearMap.map_zero _
simp [comp_rightInv_aux1 N, this, comp_rightInv_aux2, -Set.toFinset_setOf]
