English
If ht is LocallyFinite and ht' gives ContMDiffWithinAt for each t_i on u at x0, then the sum ∑ t_i is ContMDiffWithinAt on u at x0.
Русский
Если ht локально локально скользит и ht' задаёт гладкость каждой t_i на u в x0, то сумма ∑ t_i гладкая на u в x0.
LaTeX
$$ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) n (fun x ↦ TotalSpace.mk' F x (∑' i, t i x)) u x0$$
Lean4
theorem sum_section {s : Finset ι}
(hs : ∀ i ∈ s, ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) n (fun x ↦ TotalSpace.mk' F x (t i x)) u x₀) :
ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) n (fun x ↦ TotalSpace.mk' F x (∑ i ∈ s, (t i x))) u x₀ := by
classical
induction s using Finset.induction_on with
| empty => simpa only [Finset.sum_empty] using contMDiffWithinAt_zeroSection ..
| insert i s hi h =>
simp only [Finset.sum_insert hi]
apply (hs _ (s.mem_insert_self i)).add_section
exact h fun i a ↦ hs _ (s.mem_insert_of_mem a)
