finsum_smul_mem_convex — Mathlib

English

Same as above for a different fixed i.

Русский

Аналогично предыдущему утверждению для другого фиксированного i.

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 finsum_smul_mem_convex {g : ι → M → F} {t : Set F} {x : M} (hx : x ∈ s) (hg : ∀ i, f i x ≠ 0 → g i x ∈ t)
    (ht : Convex ℝ t) : ∑ᶠ i, f i x • g i x ∈ t :=
  ht.finsum_mem (fun _ => f.nonneg _ _) (f.sum_eq_one hx) hg

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