English
The finsum (infinite sum) of differentiable sections, under suitable local finiteness, is differentiable on the same set.
Русский
При условии локальной конечности бесконечная сумма дифференцируемых секций равномерно дифференцируема на том же множестве.
LaTeX
$$$ MDifferentiableOn I (I.prod 𝓘(𝕜, F)) (\x => TotalSpace.mk' F x (\sum' i, t_i x)) u$$
Lean4
/-- The scalar product `ψ • s` of a differentiable function `ψ : M → 𝕜` and a section `s` of a
vector bundle `V → M` is differentiable once `s` is differentiable on an open set containing
`tsupport ψ`.
See `ContMDiffOn.smul_section_of_tsupport` for the analogous result about `C^n` sections. -/
theorem smul_section_of_tsupport {s : Π (x : B), E x} {ψ : B → 𝕜} (hψ : MDifferentiableOn I 𝓘(𝕜) ψ u) (ht : IsOpen u)
(ht' : tsupport ψ ⊆ u) (hs : MDifferentiableOn I (I.prod 𝓘(𝕜, F)) (fun x ↦ TotalSpace.mk' F x (s x)) u) :
MDifferentiable I (I.prod 𝓘(𝕜, F)) (fun x ↦ TotalSpace.mk' F x (ψ x • s x)) :=
by
apply
mdifferentiable_of_mdifferentiableOn_union_of_isOpen (hψ.smul_section hs) ?_ ?_ ht
(isOpen_compl_iff.mpr <| isClosed_tsupport ψ)
· apply ((mdifferentiable_zeroSection _ _).mdifferentiableOn (s := (tsupport ψ)ᶜ)).congr
intro y hy
simp [image_eq_zero_of_notMem_tsupport hy, zeroSection]
· exact Set.compl_subset_iff_union.mp <| Set.compl_subset_compl.mpr ht'
