def reallyConvexHull (𝕜 : Type u_6) {E : Type u_7} [Semiring 𝕜] [PartialOrder 𝕜] [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 sum_mem_reallyConvexHull {𝕜 : Type u_1} {E : Type u_3} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] [IsOrderedRing 𝕜] {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} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] : Monotone (reallyConvexHull 𝕜)

def ReallyConvex (𝕜 : Type u_6) {E : Type u_7} [Semiring 𝕜] [PartialOrder 𝕜] [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} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] : ReallyConvex 𝕜 ∅

@[simp]

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

theorem Nontrivial.reallyConvex_iff {𝕜 : Type u_1} {E : Type u_3} [Semiring 𝕜] [PartialOrder 𝕜] [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} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] {s : Set E} [Subsingleton 𝕜] : ReallyConvex 𝕜 s

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

theorem ReallyConvex.sum_mem {𝕜 : Type u_1} {E : Type u_3} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] {s : Set E} [Nontrivial 𝕜] [IsOrderedRing 𝕜] (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} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] {s : Set E} [Nontrivial 𝕜] [IsOrderedRing 𝕜] (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} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] {s : Set E} [IsOrderedRing 𝕜] (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} [Semiring 𝕜] [PartialOrder 𝕜] [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} {E' : Type u_5} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] [AddCommMonoid E'] [Semiring 𝕜'] [PartialOrder 𝕜'] [IsOrderedRing 𝕜'] [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} {E₂ : Type u_4} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] [AddCommMonoid E₂] [Module 𝕜 E₂] [IsOrderedRing 𝕜] (f : E →ₗ[𝕜] E₂) {s : Set E₂} (hs : ReallyConvex 𝕜 s) : ReallyConvex 𝕜 (⇑f ⁻¹' s)

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