English
A variant of summability ensuring geometric bounds: there exists r>0 such that Σ_i ‖q.compAlongComposition p i‖ ⋅ r^{i1} is summable in NNReal sense.
Русский
Вариант суммируемости с геометрическим ограничением: существует r>0 such, что Σ_i ‖q.compAlongComposition p i‖ ⋅ r^{i1} суммируемо в NNReal.
LaTeX
$$$\\exists r>0,\\; Summable\\; (i \\mapsto ‖q.compAlongComposition p i.2‖_{+} \\cdot r^{i.1})$.$$
Lean4
/-- Change of variables appearing to compute the composition of partial sums of formal
power series -/
def compChangeOfVariables (m M N : ℕ) (i : Σ n, Fin n → ℕ) (hi : i ∈ compPartialSumSource m M N) : Σ n, Composition n :=
by
rcases i with ⟨n, f⟩
rw [mem_compPartialSumSource_iff] at hi
refine ⟨∑ j, f j, ofFn fun a => f a, fun {i} hi' => ?_, by simp [sum_ofFn]⟩
obtain ⟨j, rfl⟩ : ∃ j : Fin n, f j = i := by rwa [mem_ofFn', Set.mem_range] at hi'
exact (hi.2 j).1
