English
If ht is LocallyFinite and ht' assigns ContMDiffWithinAt to each t_i on u at x0, then the tsum ∑' 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 (tsum fun i => t i x)) u x0$$
Lean4
/-- The sum of a locally finite collection of sections is `C^k` iff each section is.
Version at a point within a set. -/
theorem sum_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
obtain ⟨u', hu', hfin⟩ := ht x₀
let s := {i | ((fun i ↦ {x | t i x ≠ 0}) i ∩ u').Nonempty}
have := hfin.fintype
have : ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) n (fun x ↦ TotalSpace.mk' F x (∑ i ∈ s, (t i x))) (u ∩ u') x₀ :=
ContMDiffWithinAt.sum_section fun i hi ↦ ((ht' i).mono Set.inter_subset_left)
apply (contMDiffWithinAt_inter hu').mp
apply this.congr fun y hy ↦ ?_
· rw [TotalSpace.mk_inj, tsum_eq_sum']
refine support_subset_iff'.mpr fun i hi ↦ ?_
by_contra! h
have : i ∈ s.toFinset := by
refine Set.mem_toFinset.mpr ?_
simp only [s, ne_eq, Set.mem_setOf_eq]
use x₀
simpa using ⟨h, mem_of_mem_nhds hu'⟩
exact hi this
rw [TotalSpace.mk_inj, tsum_eq_sum']
refine support_subset_iff'.mpr fun i hi ↦ ?_
by_contra! h
have : i ∈ s.toFinset := by
refine Set.mem_toFinset.mpr ?_
simp only [s, ne_eq, Set.mem_setOf_eq]
use y
simpa using ⟨h, Set.mem_of_mem_inter_right hy⟩
exact hi this
