contMDiff_smul — Mathlib

English

If each g_i is C^n on tsupport(f_i), then x ↦ ∑ᶠ i, f_i(x) g_i(x) is ContMDiff.

Русский

Если каждый g_i гладок до порядка n на tsupport(f_i), то сумма ∑ᶠ i f_i(x) g_i(x) гладко дифференцируема до порядка n.

LaTeX

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

Lean4

theorem contMDiff_smul {g : M → F} {i} (hg : ∀ x ∈ tsupport (f i), ContMDiffAt I 𝓘(ℝ, F) n g x) :
    ContMDiff I 𝓘(ℝ, F) n fun x => f i x • g x :=
  contMDiff_of_tsupport fun x hx =>
    ((f i).contMDiff.contMDiffAt.of_le (mod_cast le_top)).smul <| hg x <| tsupport_smul_subset_left _ _ hx

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