English
If all t_i are differentiable within at x0 for i in a finite set, then the finsum over i is differentiable within at x0.
Русский
Если для каждого i в конечном наборе секции дифференцируемы внутри x0, то finsum по i дифференцируема внутри x0.
LaTeX
$$$ MDifferentiableWithinAt I (I.prod 𝓘(𝕜, F)) (\x => TotalSpace.mk' F x (\sum' i, t_i x)) u x0$$
Lean4
theorem finsum_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
apply
(MDifferentiableWithinAt.sum_section_of_locallyFinite ht ht').congr' (t := Set.univ) (fun y hy ↦ ?_) (by grind)
trivial
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⟩
rw [tsum_eq_finsum (hfin.subset this)]
