English
If the operator norms of p_n grow no faster than some geometric progression with ratio less than radius, the radius is positive and bounded away from zero.
Русский
Если нормы операторов p_n растут не быстрее геометрической прогрессии с коэффициентом меньше радиуса, радиус положителен и далёк от нуля.
LaTeX
$$$\\exists C>0, \\exists r>0:\\; \\|p_n\\| \\le C r^n \\quad(\\forall n).$$$
Lean4
/-- First 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 a general abstract setup. -/
theorem radius_right_inv_pos_of_radius_pos_aux1 (n : ℕ) (p : ℕ → ℝ) (hp : ∀ k, 0 ≤ p k) {r a : ℝ} (hr : 0 ≤ r)
(ha : 0 ≤ a) :
∑ k ∈ Ico 2 (n + 1),
a ^ k *
∑ c ∈ ({c | 1 < Composition.length c}.toFinset : Finset (Composition k)),
r ^ c.length * ∏ j, p (c.blocksFun j) ≤
∑ j ∈ Ico 2 (n + 1), r ^ j * (∑ k ∈ Ico 1 n, a ^ k * p k) ^ j :=
calc
∑ k ∈ Ico 2 (n + 1),
a ^ k *
∑ c ∈ ({c | 1 < Composition.length c}.toFinset : Finset (Composition k)),
r ^ c.length * ∏ j, p (c.blocksFun j) =
∑ k ∈ Ico 2 (n + 1),
∑ c ∈ ({c | 1 < Composition.length c}.toFinset : Finset (Composition k)),
∏ j, r * (a ^ c.blocksFun j * p (c.blocksFun j)) :=
by
simp_rw [mul_sum]
congr! with k _ c
rw [prod_mul_distrib, prod_mul_distrib, prod_pow_eq_pow_sum, Composition.sum_blocksFun, prod_const, card_fin]
ring
_ ≤ ∑ d ∈ compPartialSumTarget 2 (n + 1) n, ∏ j : Fin d.2.length, r * (a ^ d.2.blocksFun j * p (d.2.blocksFun j)) :=
by
rw [sum_sigma']
gcongr
· intro x _ _
exact prod_nonneg fun j _ => mul_nonneg hr (mul_nonneg (pow_nonneg ha _) (hp _))
rintro ⟨k, c⟩ hd
simp only [Set.mem_toFinset (s := {c | 1 < Composition.length c}), mem_Ico, mem_sigma, Set.mem_setOf_eq] at hd
simp only [mem_compPartialSumTarget_iff]
refine ⟨hd.2, c.length_le.trans_lt hd.1.2, fun j => ?_⟩
have : c ≠ Composition.single k (zero_lt_two.trans_le hd.1.1) := by
simp [Composition.eq_single_iff_length, ne_of_gt hd.2]
rw [Composition.ne_single_iff] at this
exact (this j).trans_le (Nat.lt_succ_iff.mp hd.1.2)
_ = ∑ e ∈ compPartialSumSource 2 (n + 1) n, ∏ j : Fin e.1, r * (a ^ e.2 j * p (e.2 j)) :=
by
symm
apply compChangeOfVariables_sum
rintro ⟨k, blocksFun⟩ H
have K : (compChangeOfVariables 2 (n + 1) n ⟨k, blocksFun⟩ H).snd.length = k := by simp
congr 2 <;> try rw [K]
rw [Fin.heq_fun_iff K.symm]
intro j
rw [compChangeOfVariables_blocksFun]
_ = ∑ j ∈ Ico 2 (n + 1), r ^ j * (∑ k ∈ Ico 1 n, a ^ k * p k) ^ j :=
by
rw [compPartialSumSource, ←
sum_sigma' (Ico 2 (n + 1)) (fun k : ℕ => (Fintype.piFinset fun _ : Fin k => Ico 1 n : Finset (Fin k → ℕ)))
(fun n e => ∏ j : Fin n, r * (a ^ e j * p (e j)))]
congr! with j
simp only [← @MultilinearMap.mkPiAlgebra_apply ℝ (Fin j) _ ℝ]
simp only [←
MultilinearMap.map_sum_finset (MultilinearMap.mkPiAlgebra ℝ (Fin j) ℝ) fun _ (m : ℕ) => r * (a ^ m * p m)]
simp only [MultilinearMap.mkPiAlgebra_apply]
simp [prod_const, ← mul_sum, mul_pow]
