theorem map_finsum {β : Type u_1} {α : Type u_2} {γ : Type u_3} [AddCommMonoid β] [AddCommMonoid γ] {G : Type u_4} [FunLike G β γ] [AddMonoidHomClass G β γ] (g : G) {f : α → β} (hf : (Function.support f).Finite) : g (∑ᶠ (i : α), f i) = ∑ᶠ (i : α), g (f i)

theorem finprod_eq_prod_of_mulSupport_subset_of_finite {α : Type u_1} {M : Type u_2} [CommMonoid M] (f : α → M) {s : Set α} (h : Function.mulSupport f ⊆ s) (hs : s.Finite) : ∏ᶠ (i : α), f i = ∏ i ∈ hs.toFinset, f i

theorem finsum_eq_sum_of_support_subset_of_finite {α : Type u_1} {M : Type u_2} [AddCommMonoid M] (f : α → M) {s : Set α} (h : Function.support f ⊆ s) (hs : s.Finite) : ∑ᶠ (i : α), f i = ∑ i ∈ hs.toFinset, f i

def reallyConvexHull (𝕜 : Type u_6) {E : Type u_7} [OrderedSemiring 𝕜] [AddCommMonoid E] [SMul 𝕜 E] (s : Set E) : Set E

Equations

• reallyConvexHull 𝕜 s = {e : E | ∃ (w : E → 𝕜), 0 ≤ w ∧ Function.support w ⊆ s ∧ ∑ᶠ (x : E), w x = 1 ∧ e = ∑ᶠ (x : E), w x • x}

theorem finsum.exists_ne_zero_of_sum_ne_zero {β : Type u_6} {α : Type u_7} {s : Finset α} {f : α → β} [AddCommMonoid β] : ∑ᶠ (x : α) (_ : x ∈ s), f x ≠ 0 → ∃ a ∈ s, f a ≠ 0

theorem finite_of_finprod_ne_one {M : Type u_6} {ι : Type u_7} [CommMonoid M] {f : ι → M} (h : ∏ᶠ (i : ι), f i ≠ 1) : (Function.mulSupport f).Finite

theorem finite_of_finsum_ne_zero {M : Type u_6} {ι : Type u_7} [AddCommMonoid M] {f : ι → M} (h : ∑ᶠ (i : ι), f i ≠ 0) : (Function.support f).Finite

theorem support_finite_of_finsum_eq_of_neZero {M : Type u_6} {ι : Type u_7} [AddCommMonoid M] {f : ι → M} {x : M} [NeZero x] (h : ∑ᶠ (i : ι), f i = x) : (Function.support f).Finite

theorem Subsingleton.mulSupport_eq {α : Type u_6} {β : Type u_7} [Subsingleton β] [One β] (f : α → β) : Function.mulSupport f = ∅

theorem Subsingleton.support_eq {α : Type u_6} {β : Type u_7} [Subsingleton β] [Zero β] (f : α → β) : Function.support f = ∅

theorem support_finite_of_finsum_eq_one {M : Type u_6} {ι : Type u_7} [NonAssocSemiring M] {f : ι → M} (h : ∑ᶠ (i : ι), f i = 1) : (Function.support f).Finite

theorem finsum_sum_filter {α : Type u_6} {β : Type u_7} {M : Type u_8} [AddCommMonoid M] (f : β → α) (s : Finset β) [DecidableEq α] (g : β → M) : ∑ᶠ (x : α), ∑ y ∈ {j ∈ s | f j = x}, g y = ∑ k ∈ s, g k

theorem sum_mem_reallyConvexHull {𝕜 : Type u_1} {E : Type u_3} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] {s : Set E} {ι : Type u_6} {t : Finset ι} {w : ι → 𝕜} {z : ι → E} (h₀ : ∀ i ∈ t, 0 ≤ w i) (h₁ : ∑ i ∈ t, w i = 1) (hz : ∀ i ∈ t, z i ∈ s) : ∑ i ∈ t, w i • z i ∈ reallyConvexHull 𝕜 s

theorem reallyConvexHull_mono {𝕜 : Type u_1} {E : Type u_3} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] : Monotone (reallyConvexHull 𝕜)

def ReallyConvex (𝕜 : Type u_6) {E : Type u_7} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] (s : Set E) : Prop

Generalization of Convex to semirings. We only add the s = ∅ clause if 𝕜 is trivial.

Equations

• ReallyConvex 𝕜 s = (s = ∅ ∨ ∀ (w : E → 𝕜), 0 ≤ w → Function.support w ⊆ s → ∑ᶠ (x : E), w x = 1 → ∑ᶠ (x : E), w x • x ∈ s)

@[simp]

theorem reallyConvex_empty {𝕜 : Type u_1} {E : Type u_3} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] : ReallyConvex 𝕜 ∅

@[simp]

theorem reallyConvex_univ {𝕜 : Type u_1} {E : Type u_3} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] : ReallyConvex 𝕜 Set.univ

theorem Nontrivial.reallyConvex_iff {𝕜 : Type u_1} {E : Type u_3} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] {s : Set E} [Nontrivial 𝕜] : ReallyConvex 𝕜 s ↔ ∀ (w : E → 𝕜), 0 ≤ w → Function.support w ⊆ s → ∑ᶠ (x : E), w x = 1 → ∑ᶠ (x : E), w x • x ∈ s

theorem Subsingleton.reallyConvex {𝕜 : Type u_1} {E : Type u_3} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] {s : Set E} [Subsingleton 𝕜] : ReallyConvex 𝕜 s

theorem reallyConvex_iff_hull {𝕜 : Type u_1} {E : Type u_3} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] {s : Set E} [Nontrivial 𝕜] : ReallyConvex 𝕜 s ↔ reallyConvexHull 𝕜 s ⊆ s

theorem ReallyConvex.sum_mem {𝕜 : Type u_1} {E : Type u_3} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] {s : Set E} [Nontrivial 𝕜] (hs : ReallyConvex 𝕜 s) {ι : Type u_6} {t : Finset ι} {w : ι → 𝕜} {z : ι → E} (h₀ : ∀ i ∈ t, 0 ≤ w i) (h₁ : ∑ i ∈ t, w i = 1) (hz : ∀ i ∈ t, z i ∈ s) : ∑ i ∈ t, w i • z i ∈ s

theorem ReallyConvex.finsum_mem {𝕜 : Type u_1} {E : Type u_3} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] {s : Set E} [Nontrivial 𝕜] (hs : ReallyConvex 𝕜 s) {ι : Type u_6} {w : ι → 𝕜} {z : ι → E} (h₀ : ∀ (i : ι), 0 ≤ w i) (h₁ : ∑ᶠ (i : ι), w i = 1) (hz : ∀ i ∈ Function.support w, z i ∈ s) : ∑ᶠ (i : ι), w i • z i ∈ s

theorem ReallyConvex.add_mem {𝕜 : Type u_1} {E : Type u_3} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] {s : Set E} (hs : ReallyConvex 𝕜 s) {w₁ w₂ : 𝕜} {z₁ z₂ : E} (hw₁ : 0 ≤ w₁) (hw₂ : 0 ≤ w₂) (hw : w₁ + w₂ = 1) (hz₁ : z₁ ∈ s) (hz₂ : z₂ ∈ s) : w₁ • z₁ + w₂ • z₂ ∈ s

theorem ReallyConvex.inter {𝕜 : Type u_1} {E : Type u_3} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] {s t : Set E} (hs : ReallyConvex 𝕜 s) (ht : ReallyConvex 𝕜 t) : ReallyConvex 𝕜 (s ∩ t)

theorem ReallyConvex.preimageₛₗ {𝕜 : Type u_1} {𝕜' : Type u_2} {E : Type u_3} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] {E' : Type u_5} [AddCommMonoid E'] [OrderedSemiring 𝕜'] [Module 𝕜' E'] (σ : 𝕜 →+*o 𝕜') (f : E →ₛₗ[σ.toRingHom] E') {s : Set E'} (hs : ReallyConvex 𝕜' s) : ReallyConvex 𝕜 (⇑f ⁻¹' s)

theorem ReallyConvex.preimage {𝕜 : Type u_1} {E : Type u_3} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] {E₂ : Type u_4} [AddCommMonoid E₂] [Module 𝕜 E₂] (f : E →ₗ[𝕜] E₂) {s : Set E₂} (hs : ReallyConvex 𝕜 s) : ReallyConvex 𝕜 (⇑f ⁻¹' s)

theorem reallyConvex_iff_convex (𝕜 : Type u_1) {E : Type u_2} [LinearOrderedField 𝕜] [AddCommGroup E] [Module 𝕜 E] {s : Set E} : ReallyConvex 𝕜 s ↔ Convex 𝕜 s