contDiffAt_finsum — Mathlib

English

If t is a convex set and g_i are in t, then the finsum of f_i x • g_i x lies in t.

Русский

Если t выпукто и элементы g_i(x) ∈ t, то сумма f_i(x) g_i(x) лежит в t.

LaTeX

$$Given convex set t ⊂ F, if all g_i(x) ∈ t whenever f_i(x) ≠ 0, then finsum f_i x • g_i x ∈ t.$$

Lean4

theorem contDiffAt_finsum {s : Set E} (f : SmoothPartitionOfUnity ι 𝓘(ℝ, E) E s) {x₀ : E} {g : ι → E → F}
    (hφ : ∀ i, x₀ ∈ tsupport (f i) → ContDiffAt ℝ n (g i) x₀) : ContDiffAt ℝ n (fun x ↦ ∑ᶠ i, f i x • g i x) x₀ :=
  by
  simp only [← contMDiffAt_iff_contDiffAt] at *
  exact f.contMDiffAt_finsum hφ

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