contMDiff_finsum_smul — Mathlib

English

The finsum x ↦ ∑ᶠ i, f_i(x) is ContMDiff.

Русский

Функция x ↦ ∑ᶠ i f_i(x) гладко дифференцируема.

LaTeX

$$$\text{ContMDiff } I\, 𝓘(\mathbb{R})\, \infty\ (x \mapsto \sum^\infty_i f_i(x))$$$

Lean4

/-- If `f` is a smooth partition of unity on a set `s : Set M` and `g : ι → M → F` is a family of
functions such that `g i` is $C^n$ smooth at every point of the topological support of `f i`, then
the sum `fun x ↦ ∑ᶠ i, f i x • g i x` is smooth on the whole manifold. -/
theorem contMDiff_finsum_smul {g : ι → M → F} (hg : ∀ (i), ∀ x ∈ tsupport (f i), ContMDiffAt I 𝓘(ℝ, F) n (g i) x) :
    ContMDiff I 𝓘(ℝ, F) n fun x => ∑ᶠ i, f i x • g i x :=
  (contMDiff_finsum fun i => f.contMDiff_smul (hg i)) <| f.locallyFinite.subset fun _ => support_smul_subset_left _ _

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