contMDiffAt_finsum — Mathlib

English

The finsum evaluated at a point x0 is ContMDiff at x0.

Русский

Значение суммы ∑ᶠ i f_i(x) в точке x0 гладко в окрестности x0.

LaTeX

$$$\text{ContMDiffAt } I \ 𝓘(\mathbb{R}, F)\, n (x \mapsto \sum^\infty_i f_i(x))\, x_0$$$

Lean4

theorem contMDiffAt_finsum {x₀ : M} {g : ι → M → F} (hφ : ∀ i, x₀ ∈ tsupport (f i) → ContMDiffAt I 𝓘(ℝ, F) n (g i) x₀) :
    ContMDiffAt I 𝓘(ℝ, F) n (fun x ↦ ∑ᶠ i, f i x • g i x) x₀ :=
  by
  refine _root_.contMDiffAt_finsum (f.locallyFinite.smul_left _) fun i ↦ ?_
  by_cases hx : x₀ ∈ tsupport (f i)
  · exact ContMDiffAt.smul ((f i).contMDiff.of_le (mod_cast le_top)).contMDiffAt (hφ i hx)
  · exact contMDiffAt_of_notMem (compl_subset_compl.mpr (tsupport_smul_subset_left (f i) (g i)) hx) n

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