English
FormalMultilinearSeries.compChangeOfVariables_sum asserts the equality of sums when changing variables in the sum over compositions; it formalizes that the variable change preserves the total.
Русский
Теорема compChangeOfVariables_sum: переход к изменению переменных в сумме по композициям сохраняет общую сумму.
LaTeX
$$∀ e, f, g, h, h, equality of sums under the bijection compChangeOfVariables; sum over source equals sum over target.$$
Lean4
/-- The auxiliary set corresponding to the composition of partial sums asymptotically contains
all possible compositions. -/
theorem compPartialSumTarget_tendsto_prod_atTop :
Tendsto (fun (p : ℕ × ℕ) => compPartialSumTarget 0 p.1 p.2) atTop atTop :=
by
apply Monotone.tendsto_atTop_finset
· intro m n hmn a ha
have : ∀ i, i < m.1 → i < n.1 := fun i hi => lt_of_lt_of_le hi hmn.1
have : ∀ i, i < m.2 → i < n.2 := fun i hi => lt_of_lt_of_le hi hmn.2
simp_all
· rintro ⟨n, c⟩
simp only [mem_compPartialSumTarget_iff]
obtain ⟨n, hn⟩ : BddAbove ((Finset.univ.image fun i : Fin c.length => c.blocksFun i) : Set ℕ) := Finset.bddAbove _
refine
⟨max n c.length + 1, bot_le, lt_of_le_of_lt (le_max_right n c.length) (lt_add_one _), fun j =>
lt_of_le_of_lt (le_trans ?_ (le_max_left _ _)) (lt_add_one _)⟩
apply hn
simp only [Finset.mem_image_of_mem, Finset.mem_coe, Finset.mem_univ]
