English
For any p, sums of origin-changed terms are summable with a bound derived from the origin-change construction.
Русский
Для любого p суммы членов после переноса начала образуют сходящуюся последовательность со специализированной ограничающей оценкой.
LaTeX
$$$\\text{changeOriginSeries_summable_aux₂}: \\; (hr) \\Rightarrow \\; \\Sum_S \\dots < \\infty$$$
Lean4
theorem changeOriginSeries_summable_aux₁ {r r' : ℝ≥0} (hr : (r + r' : ℝ≥0∞) < p.radius) :
Summable fun s : Σ k l : ℕ, { s : Finset (Fin (k + l)) // s.card = l } =>
‖p (s.1 + s.2.1)‖₊ * r ^ s.2.1 * r' ^ s.1 :=
by
rw [← changeOriginIndexEquiv.symm.summable_iff]
dsimp only [Function.comp_def, changeOriginIndexEquiv_symm_apply_fst, changeOriginIndexEquiv_symm_apply_snd_fst]
have :
∀ n : ℕ,
HasSum (fun s : Finset (Fin n) => ‖p (n - s.card + s.card)‖₊ * r ^ s.card * r' ^ (n - s.card))
(‖p n‖₊ * (r + r') ^ n) :=
by
intro n
convert_to HasSum (fun s : Finset (Fin n) => ‖p n‖₊ * (r ^ s.card * r' ^ (n - s.card))) _
· ext1 s
rw [tsub_add_cancel_of_le (card_finset_fin_le _), mul_assoc]
rw [← Fin.sum_pow_mul_eq_add_pow]
exact (hasSum_fintype _).mul_left _
refine NNReal.summable_sigma.2 ⟨fun n => (this n).summable, ?_⟩
simp only [(this _).tsum_eq]
exact p.summable_nnnorm_mul_pow hr
