English
If q and p have positive radii of convergence, then the terms that appear in the definition of their composition are summable when weighted by a suitable geometric factor; i.e., there exists r>0 such that Σ_i ‖q.compAlongComposition p i‖ r^{i1} converges.
Русский
Если q и p имеют положительные радиусы сходимости, то члены, входящие в определение композиции, суммируемы при взвешивании подходящим геометрическим коэффициентом; то есть существует r>0 such that Σ_i ‖q.compAlongComposition p i‖ r^{i1} сходится.
LaTeX
$$$\\exists r>0:\\ SUM_{i:\\Sigma n, Composition n} \\|q.compAlongComposition p i.2\\|_ + \\; r^{i.1} \\text{ суммируемо.}$$$
Lean4
/-- If two formal multilinear series have positive radius of convergence, then the terms appearing
in the definition of their composition are also summable (when multiplied by a suitable positive
geometric term). -/
theorem comp_summable_nnreal (q : FormalMultilinearSeries 𝕜 F G) (p : FormalMultilinearSeries 𝕜 E F) (hq : 0 < q.radius)
(hp : 0 < p.radius) :
∃ r > (0 : ℝ≥0), Summable fun i : Σ n, Composition n => ‖q.compAlongComposition p i.2‖₊ * r ^ i.1 := by
/- This follows from the fact that the growth rate of `‖qₙ‖` and `‖pₙ‖` is at most geometric,
giving a geometric bound on each `‖q.compAlongComposition p op‖`, together with the
fact that there are `2^(n-1)` compositions of `n`, giving at most a geometric loss. -/
rcases ENNReal.lt_iff_exists_nnreal_btwn.1 (lt_min zero_lt_one hq) with ⟨rq, rq_pos, hrq⟩
rcases ENNReal.lt_iff_exists_nnreal_btwn.1 (lt_min zero_lt_one hp) with ⟨rp, rp_pos, hrp⟩
simp only [lt_min_iff, ENNReal.coe_lt_one_iff, ENNReal.coe_pos] at hrp hrq rp_pos rq_pos
obtain ⟨Cq, _hCq0, hCq⟩ : ∃ Cq > 0, ∀ n, ‖q n‖₊ * rq ^ n ≤ Cq := q.nnnorm_mul_pow_le_of_lt_radius hrq.2
obtain ⟨Cp, hCp1, hCp⟩ : ∃ Cp ≥ 1, ∀ n, ‖p n‖₊ * rp ^ n ≤ Cp :=
by
rcases p.nnnorm_mul_pow_le_of_lt_radius hrp.2 with ⟨Cp, -, hCp⟩
exact ⟨max Cp 1, le_max_right _ _, fun n => (hCp n).trans (le_max_left _ _)⟩
let r0 : ℝ≥0 := (4 * Cp)⁻¹
have r0_pos : 0 < r0 := inv_pos.2 (mul_pos zero_lt_four (zero_lt_one.trans_le hCp1))
set r : ℝ≥0 := rp * rq * r0
have r_pos : 0 < r := mul_pos (mul_pos rp_pos rq_pos) r0_pos
have I : ∀ i : Σ n : ℕ, Composition n, ‖q.compAlongComposition p i.2‖₊ * r ^ i.1 ≤ Cq / 4 ^ i.1 :=
by
rintro ⟨n, c⟩
have A :=
calc
‖q c.length‖₊ * rq ^ n ≤ ‖q c.length‖₊ * rq ^ c.length :=
mul_le_mul' le_rfl (pow_le_pow_of_le_one rq.2 hrq.1.le c.length_le)
_ ≤ Cq := hCq _
have B :=
calc
(∏ i, ‖p (c.blocksFun i)‖₊) * rp ^ n = ∏ i, ‖p (c.blocksFun i)‖₊ * rp ^ c.blocksFun i := by
simp only [Finset.prod_mul_distrib, Finset.prod_pow_eq_pow_sum, c.sum_blocksFun]
_ ≤ ∏ _i : Fin c.length, Cp := (Finset.prod_le_prod' fun i _ => hCp _)
_ = Cp ^ c.length := by simp
_ ≤ Cp ^ n := pow_right_mono₀ hCp1 c.length_le
calc
‖q.compAlongComposition p c‖₊ * r ^ n ≤ (‖q c.length‖₊ * ∏ i, ‖p (c.blocksFun i)‖₊) * r ^ n := by
grw [q.compAlongComposition_nnnorm p c]
_ = ‖q c.length‖₊ * rq ^ n * ((∏ i, ‖p (c.blocksFun i)‖₊) * rp ^ n) * r0 ^ n := by ring
_ ≤ Cq * Cp ^ n * r0 ^ n := (mul_le_mul' (mul_le_mul' A B) le_rfl)
_ = Cq / 4 ^ n := by
simp only [r0]
simp [field, mul_pow]
refine ⟨r, r_pos, NNReal.summable_of_le I ?_⟩
simp_rw [div_eq_mul_inv]
refine Summable.mul_left _ ?_
have : ∀ n : ℕ, HasSum (fun c : Composition n => (4 ^ n : ℝ≥0)⁻¹) (2 ^ (n - 1) / 4 ^ n) :=
by
intro n
convert hasSum_fintype fun c : Composition n => (4 ^ n : ℝ≥0)⁻¹
simp [Finset.card_univ, composition_card, div_eq_mul_inv]
refine NNReal.summable_sigma.2 ⟨fun n => (this n).summable, (NNReal.summable_nat_add_iff 1).1 ?_⟩
convert (NNReal.summable_geometric (NNReal.div_lt_one_of_lt one_lt_two)).mul_left (1 / 4) using 1
ext1 n
rw [(this _).tsum_eq, add_tsub_cancel_right]
simp [field, pow_succ, mul_pow, show (4 : ℝ≥0) = 2 * 2 by norm_num]
