sum_nonneg — Mathlib

English

If g is C^n on tsupport(f_i), then x ↦ f_i(x) g(x) is C^n.

Русский

Если g гладко дифференцируема до порядка n на поддержке tsupport(f_i), то произведение f_i(x) g(x) гладко дифференцируемо до порядка n.

LaTeX

$$$\forall i,\ (\forall x\in tsupport(f_i),\ ContMDiffAt(I, 𝓘(\mathbb{R}, F), n, g, x))\Rightarrow\ ContMDiffAt(I, 𝓘(\mathbb{R}, F), n, (x \mapsto f_i(x) g(x)), x)$$$

Lean4

theorem sum_nonneg (x : M) : 0 ≤ ∑ᶠ i, f i x :=
  f.toPartitionOfUnity.sum_nonneg x

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