English
Under appropriate assumptions, the finsum of differentiable sections is differentiable within at x0.
Русский
При надлежащих предположениях бесконечная сумма дифференцируемых секций дифференцируема внутри x0.
LaTeX
$$$ MDifferentiableWithinAt I (I.prod 𝓘(𝕜, F)) (\x => TotalSpace.mk' F x (\sum' i, t_i x)) u x0$$
Lean4
/-- The sum of a locally finite collection of sections is differentiable if each section is.
Version at a point within a set. -/
theorem sum_section_of_locallyFinite (ht : LocallyFinite fun i ↦ {x : B | t i x ≠ 0})
(ht' : ∀ i, MDifferentiableWithinAt I (I.prod 𝓘(𝕜, F)) (fun x ↦ TotalSpace.mk' F x (t i x)) u x₀) :
MDifferentiableWithinAt I (I.prod 𝓘(𝕜, F)) (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 : MDifferentiableWithinAt I (I.prod 𝓘(𝕜, F)) (fun x ↦ TotalSpace.mk' F x (∑ i ∈ s, (t i x))) (u ∩ u') x₀ :=
MDifferentiableWithinAt.sum_section fun i ↦ ((ht' i).mono inter_subset_left)
apply (mdifferentiableWithinAt_inter hu').mp
apply this.congr' (fun y hy ↦ ?_) inter_subset_right (mem_of_mem_nhds hu')
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
simp [h, hy]
exact hi this
