sum_section — Mathlib

English

If two differentiable sections s and t are given, then their sum is differentiable.

Русский

Если заданы дифференцируемые секции s и t, то их сумма дифференцируема.

LaTeX

$$$ MDifferentiable I (I.prod 𝓘(𝕜, F)) (\x => TotalSpace.mk' F x (s x + t x))$$

Lean4

theorem sum_section {ι : Type*} {s : Finset ι} {t : ι → (x : B) → E x}
    (hs : ∀ 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 ∈ s, (t i x))) u x₀ := by
  classical
    induction s using Finset.induction_on with
  | empty => simpa using (contMDiffWithinAt_zeroSection 𝕜 E).mdifferentiableWithinAt le_rfl
  | insert i s hi h => simpa [Finset.sum_insert hi] using mdifferentiableWithinAt_add_section (hs i) h

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