English
Second technical lemma bounds the growth of the inverse coefficients; the radius bound follows.
Русский
Вторая техническая лемма ограничивает рост коэффициентов обратной серии; вытекает ограничение радиуса.
LaTeX
$$$\\text{(radius inequalities for inverse series and p.radius)}$$$
Lean4
/-- Second technical lemma to control the growth of coefficients of the inverse. Bound the explicit
expression for `∑_{k<n+1} aᵏ Qₖ` in terms of a sum of powers of the same sum one step before,
in the specific setup we are interesting in, by reducing to the general bound in
`radius_rightInv_pos_of_radius_pos_aux1`. -/
theorem radius_rightInv_pos_of_radius_pos_aux2 {x : E} {n : ℕ} (hn : 2 ≤ n + 1) (p : FormalMultilinearSeries 𝕜 E F)
(i : E ≃L[𝕜] F) {r a C : ℝ} (hr : 0 ≤ r) (ha : 0 ≤ a) (hC : 0 ≤ C) (hp : ∀ n, ‖p n‖ ≤ C * r ^ n) :
∑ k ∈ Ico 1 (n + 1), a ^ k * ‖p.rightInv i x k‖ ≤
‖(i.symm : F →L[𝕜] E)‖ * a +
‖(i.symm : F →L[𝕜] E)‖ * C * ∑ k ∈ Ico 2 (n + 1), (r * ∑ j ∈ Ico 1 n, a ^ j * ‖p.rightInv i x j‖) ^ k :=
let I := ‖(i.symm : F →L[𝕜] E)‖
calc
∑ k ∈ Ico 1 (n + 1), a ^ k * ‖p.rightInv i x k‖ = a * I + ∑ k ∈ Ico 2 (n + 1), a ^ k * ‖p.rightInv i x k‖ := by
simp only [I, LinearIsometryEquiv.norm_map, pow_one, rightInv_coeff_one,
show Ico (1 : ℕ) 2 = { 1 } from Nat.Ico_succ_singleton 1, sum_singleton, ← sum_Ico_consecutive _ one_le_two hn]
_ =
a * I +
∑ k ∈ Ico 2 (n + 1),
a ^ k *
‖(i.symm : F →L[𝕜] E).compContinuousMultilinearMap
(∑ c ∈ ({c | 1 < Composition.length c}.toFinset : Finset (Composition k)),
p.compAlongComposition (p.rightInv i x) c)‖ :=
by
congr! 2 with j hj
rw [rightInv_coeff _ _ _ _ (mem_Ico.1 hj).1, norm_neg]
_ ≤
a * ‖(i.symm : F →L[𝕜] E)‖ +
∑ k ∈ Ico 2 (n + 1),
a ^ k *
(I *
∑ c ∈ ({c | 1 < Composition.length c}.toFinset : Finset (Composition k)),
C * r ^ c.length * ∏ j, ‖p.rightInv i x (c.blocksFun j)‖) :=
by
gcongr with j
apply (ContinuousLinearMap.norm_compContinuousMultilinearMap_le _ _).trans
gcongr
apply (norm_sum_le _ _).trans
gcongr
apply (compAlongComposition_norm _ _ _).trans
gcongr
apply hp
_ =
I * a +
I * C *
∑ k ∈ Ico 2 (n + 1),
a ^ k *
∑ c ∈ ({c | 1 < Composition.length c}.toFinset : Finset (Composition k)),
r ^ c.length * ∏ j, ‖p.rightInv i x (c.blocksFun j)‖ :=
by
simp_rw [I, mul_assoc C, ← mul_sum, ← mul_assoc, mul_comm _ ‖(i.symm : F →L[𝕜] E)‖, mul_assoc, ← mul_sum, ←
mul_assoc, mul_comm _ C, mul_assoc, ← mul_sum]
ring
_ ≤ I * a + I * C * ∑ k ∈ Ico 2 (n + 1), (r * ∑ j ∈ Ico 1 n, a ^ j * ‖p.rightInv i x j‖) ^ k :=
by
gcongr _ + _ * _ * ?_
simp_rw [mul_pow]
apply radius_right_inv_pos_of_radius_pos_aux1 n (fun k => ‖p.rightInv i x k‖) (fun k => norm_nonneg _) hr ha
