English
Let ht express local finiteness of the family {t_i} of sections as in ContMDiffWithinAt. If each i yields a C^k-map x ↦ TotalSpace.mk' F x (t_i(x)) within a neighborhood u of x0, then the finsum x ↦ TotalSpace.mk' F x (∑' i, t_i(x)) is C^k on that neighborhood.
Русский
Пусть {t_i} образуют локально конечную совокупность секций; если для каждого i отображение x ↦ TotalSpace.mk' F x (t_i(x)) определено как C^k внутри окрестности u вокруг x0, то сумма finsum тоже гладкая внутри этой окрестности.
LaTeX
$$$\operatorname{LocallyFinite}\,\bigl(i \mapsto \{x \in M \mid t_i(x) \neq 0\}\bigr) \land \forall i,\ ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) n (x \mapsto TotalSpace.mk' F x (t_i(x))) u x_0 \Rightarrow \ ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) n (x \mapsto TotalSpace.mk' F x (\sum' i, t_i(x))) u x_0$$$
Lean4
theorem finsum_section_of_locallyFinite (ht : LocallyFinite fun i ↦ {x : M | t i x ≠ 0})
(ht' : ∀ i, 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, t i x)) u x₀ :=
by
apply
(ContMDiffWithinAt.sum_section_of_locallyFinite ht ht').congr' (t := Set.univ) (fun y hy ↦ ?_) (by grind) trivial
rw [← tsum_eq_finsum (L := SummationFilter.unconditional ι)]
choose U hu hfin using ht y
have : {x | t x y ≠ 0} ⊆ {i | ((fun i ↦ {x | t i x ≠ 0}) i ∩ U).Nonempty} :=
by
intro x hx
rw [Set.mem_setOf] at hx ⊢
use y
simpa using ⟨hx, mem_of_mem_nhds hu⟩
exact Set.Finite.subset hfin this
