finsum_smul_mem_convex — Mathlib

English

Let f be a PartitionOfUnity on X and g_i:X→E be a family with supports subordinate to the partition; then the finite sum of f_i x g_i x lies in a convex set t if t is convex.

Русский

Пусть f—разбиение единицы на X, а g_i: X→E — семейство структур, опор которых◦ подпадают под разбиение; сумма smul-образов принадлежит выпуклому множеству.

LaTeX

$$$\forall x, \sum f_i(x) g_i(x) \in t \;\text{при } t\text{ выпукло}$$$

Lean4

theorem finsum_smul_mem_convex {s : Set X} (f : PartitionOfUnity ι X s) {g : ι → X → E} {t : Set E} {x : X} (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

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