sum_section_of_locallyFinite — Mathlib

English

If a collection of differentiable sections indexed by Finset sums to a differentiable section, then the sum is differentiable on the domain.

Русский

Если сумма секций по Finset даёт дифференцируемую секцию, то сумма дифференцируема на области определения.

LaTeX

$$$ MDifferentiableOn I (I.prod (modelWithCornersSelf 𝕜 F)) (\x => TotalSpace.mk' F x (s.sum (λ i, t i x))) u$$

Lean4

/-- The sum of a locally finite collection of sections is differentiable on a set `u`
if each section is. -/
theorem sum_section_of_locallyFinite (ht : LocallyFinite fun i ↦ {x : B | t i x ≠ 0})
    (ht' : ∀ i, MDifferentiableOn I (I.prod 𝓘(𝕜, F)) (fun x ↦ TotalSpace.mk' F x (t i x)) u) :
    MDifferentiableOn I (I.prod 𝓘(𝕜, F)) (fun x ↦ TotalSpace.mk' F x (∑' i, (t i x))) u := fun x hx ↦
  .sum_section_of_locallyFinite ht (ht' · x hx)

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