finsum_section_of_locallyFinite — Mathlib

English

If ht is locally finite and each t_i is differentiable at x0, then the finsum over i is differentiable at x0.

Русский

Если ht локально конечна и каждая t_i дифференцируема в x0, то finsum по i дифференцируема в x0.

LaTeX

$$$ MDifferentiableAt I (I.prod 𝓘(𝕜, F)) (\x => TotalSpace.mk' F x (\sumᶠ i, t_i x)) x0$$

Lean4

theorem finsum_section_of_locallyFinite (ht : LocallyFinite fun i ↦ {x : B | t i x ≠ 0})
    (ht' : ∀ i, MDifferentiableAt I (I.prod 𝓘(𝕜, F)) (fun x ↦ TotalSpace.mk' F x (t i x)) x₀) :
    MDifferentiableAt I (I.prod 𝓘(𝕜, F)) (fun x ↦ TotalSpace.mk' F x (∑ᶠ i, t i x)) x₀ :=
  by
  simp_rw [← mdifferentiableWithinAt_univ] at ht' ⊢
  exact .finsum_section_of_locallyFinite ht ht'

Похожие утверждения