Convex sets

In a 𝕜-vector space, we define the following property:

• Convex 𝕜 s: A set s is convex if for any two points x y ∈ s it includes segment 𝕜 x y.

We provide various equivalent versions, and prove that some specific sets are convex.

TODO

Generalize all this file to affine spaces.

Convexity of sets

def Convex (𝕜 : Type u_1) {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [SMul 𝕜 E] (s : Set E) : Prop

Convexity of sets.

Equations

• Convex 𝕜 s = ∀ ⦃x : E⦄, x ∈ s → StarConvex 𝕜 x s

theorem Convex.starConvex {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [SMul 𝕜 E] {s : Set E} {x : E} (hs : Convex 𝕜 s) (hx : x ∈ s) : StarConvex 𝕜 x s

theorem convex_iff_segment_subset {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [SMul 𝕜 E] {s : Set E} : Convex 𝕜 s ↔ ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → segment 𝕜 x y ⊆ s

theorem Convex.segment_subset {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [SMul 𝕜 E] {s : Set E} (h : Convex 𝕜 s) {x y : E} (hx : x ∈ s) (hy : y ∈ s) : segment 𝕜 x y ⊆ s

theorem Convex.openSegment_subset {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [SMul 𝕜 E] {s : Set E} (h : Convex 𝕜 s) {x y : E} (hx : x ∈ s) (hy : y ∈ s) : openSegment 𝕜 x y ⊆ s

theorem convex_iff_add_mem {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [SMul 𝕜 E] {s : Set E} : Convex 𝕜 s ↔ ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • x + b • y ∈ s

theorem convex_iff_pointwise_add_subset {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [SMul 𝕜 E] {s : Set E} : Convex 𝕜 s ↔ ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • s + b • s ⊆ s

Alternative definition of set convexity, in terms of pointwise set operations.

theorem Convex.set_combo_subset {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [SMul 𝕜 E] {s : Set E} : Convex 𝕜 s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • s + b • s ⊆ s

Alias of the forward direction of convex_iff_pointwise_add_subset.

---

Alternative definition of set convexity, in terms of pointwise set operations.

theorem convex_empty {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [SMul 𝕜 E] : Convex 𝕜 ∅

theorem convex_univ {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [SMul 𝕜 E] : Convex 𝕜 Set.univ

theorem Convex.inter {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [SMul 𝕜 E] {s t : Set E} (hs : Convex 𝕜 s) (ht : Convex 𝕜 t) : Convex 𝕜 (s ∩ t)

theorem convex_sInter {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [SMul 𝕜 E] {S : Set (Set E)} (h : ∀ s ∈ S, Convex 𝕜 s) : Convex 𝕜 (⋂₀ S)

theorem convex_iInter {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [SMul 𝕜 E] {ι : Sort u_5} {s : ι → Set E} (h : ∀ (i : ι), Convex 𝕜 (s i)) : Convex 𝕜 (⋂ (i : ι), s i)

theorem convex_iInter₂ {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [SMul 𝕜 E] {ι : Sort u_5} {κ : ι → Sort u_6} {s : (i : ι) → κ i → Set E} (h : ∀ (i : ι) (j : κ i), Convex 𝕜 (s i j)) : Convex 𝕜 (⋂ (i : ι), ⋂ (j : κ i), s i j)

theorem Convex.prod {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [AddCommMonoid F] [SMul 𝕜 E] [SMul 𝕜 F] {s : Set E} {t : Set F} (hs : Convex 𝕜 s) (ht : Convex 𝕜 t) : Convex 𝕜 (s ×ˢ t)

theorem convex_pi {𝕜 : Type u_1} [Semiring 𝕜] [PartialOrder 𝕜] {ι : Type u_5} {E : ι → Type u_6} [(i : ι) → AddCommMonoid (E i)] [(i : ι) → SMul 𝕜 (E i)] {s : Set ι} {t : (i : ι) → Set (E i)} (ht : ∀ ⦃i : ι⦄, i ∈ s → Convex 𝕜 (t i)) : Convex 𝕜 (s.pi t)

theorem Directed.convex_iUnion {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [SMul 𝕜 E] {ι : Sort u_5} {s : ι → Set E} (hdir : Directed (fun (x1 x2 : Set E) => x1 ⊆ x2) s) (hc : ∀ ⦃i : ι⦄, Convex 𝕜 (s i)) : Convex 𝕜 (⋃ (i : ι), s i)

theorem DirectedOn.convex_sUnion {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [SMul 𝕜 E] {c : Set (Set E)} (hdir : DirectedOn (fun (x1 x2 : Set E) => x1 ⊆ x2) c) (hc : ∀ ⦃A : Set E⦄, A ∈ c → Convex 𝕜 A) : Convex 𝕜 (⋃₀ c)

theorem Convex.setOf_const_imp {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [SMul 𝕜 E] {s : Set E} {P : Prop} (hs : Convex 𝕜 s) : Convex 𝕜 {x : E | P → x ∈ s}

theorem convex_iff_openSegment_subset {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] {s : Set E} [ZeroLEOneClass 𝕜] : Convex 𝕜 s ↔ ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → openSegment 𝕜 x y ⊆ s

theorem convex_iff_forall_pos {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] {s : Set E} : Convex 𝕜 s ↔ ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s

theorem convex_iff_pairwise_pos {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] {s : Set E} : Convex 𝕜 s ↔ s.Pairwise fun (x y : E) => ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s

theorem Convex.starConvex_iff {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] {s : Set E} {x : E} [ZeroLEOneClass 𝕜] (hs : Convex 𝕜 s) (h : s.Nonempty) : StarConvex 𝕜 x s ↔ x ∈ s

theorem Set.Subsingleton.convex {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] {s : Set E} (h : s.Subsingleton) : Convex 𝕜 s

@[simp]

theorem convex_singleton {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] (c : E) : Convex 𝕜 {c}

theorem convex_zero {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] : Convex 𝕜 0

theorem convex_segment {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] [IsOrderedRing 𝕜] (x y : E) : Convex 𝕜 (segment 𝕜 x y)

theorem Convex.linear_image {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [AddCommMonoid F] [Module 𝕜 E] [Module 𝕜 F] {s : Set E} (hs : Convex 𝕜 s) (f : E →ₗ[𝕜] F) : Convex 𝕜 (⇑f '' s)

See Convex.semilinear_image for a version for semilinear maps, but requiring that 𝕜 be a linear order, instead of just a partial order.

theorem Convex.is_linear_image {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [AddCommMonoid F] [Module 𝕜 E] [Module 𝕜 F] {s : Set E} (hs : Convex 𝕜 s) {f : E → F} (hf : IsLinearMap 𝕜 f) : Convex 𝕜 (f '' s)

theorem Convex.linear_preimage {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [AddCommMonoid F] [Module 𝕜 E] [Module 𝕜 F] {s : Set F} (hs : Convex 𝕜 s) (f : E →ₗ[𝕜] F) : Convex 𝕜 (⇑f ⁻¹' s)

theorem Convex.is_linear_preimage {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [AddCommMonoid F] [Module 𝕜 E] [Module 𝕜 F] {s : Set F} (hs : Convex 𝕜 s) {f : E → F} (hf : IsLinearMap 𝕜 f) : Convex 𝕜 (f ⁻¹' s)

theorem Convex.add {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] {s t : Set E} (hs : Convex 𝕜 s) (ht : Convex 𝕜 t) : Convex 𝕜 (s + t)

noncomputable def convexAddSubmonoid (𝕜 : Type u_1) (E : Type u_2) [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] : AddSubmonoid (Set E)

The convex sets form an additive submonoid under pointwise addition.

Equations

• convexAddSubmonoid 𝕜 E = { carrier := {s : Set E | Convex 𝕜 s}, add_mem' := ⋯, zero_mem' := ⋯ }

@[simp]

theorem coe_convexAddSubmonoid (𝕜 : Type u_1) (E : Type u_2) [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] : ↑(convexAddSubmonoid 𝕜 E) = {s : Set E | Convex 𝕜 s}

@[simp]

theorem mem_convexAddSubmonoid {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] {s : Set E} : s ∈ convexAddSubmonoid 𝕜 E ↔ Convex 𝕜 s

theorem convex_list_sum {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] {l : List (Set E)} (h : ∀ i ∈ l, Convex 𝕜 i) : Convex 𝕜 l.sum

theorem convex_multiset_sum {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] {s : Multiset (Set E)} (h : ∀ i ∈ s, Convex 𝕜 i) : Convex 𝕜 s.sum

theorem convex_sum {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] {ι : Type u_5} {s : Finset ι} (t : ι → Set E) (h : ∀ i ∈ s, Convex 𝕜 (t i)) : Convex 𝕜 (∑ i ∈ s, t i)

theorem Convex.vadd {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] {s : Set E} (hs : Convex 𝕜 s) (z : E) : Convex 𝕜 (z +ᵥ s)

theorem Convex.translate {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] {s : Set E} (hs : Convex 𝕜 s) (z : E) : Convex 𝕜 ((fun (x : E) => z + x) '' s)

theorem Convex.translate_preimage_right {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] {s : Set E} (hs : Convex 𝕜 s) (z : E) : Convex 𝕜 ((fun (x : E) => z + x) ⁻¹' s)

The translation of a convex set is also convex.

theorem Convex.translate_preimage_left {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] {s : Set E} (hs : Convex 𝕜 s) (z : E) : Convex 𝕜 ((fun (x : E) => x + z) ⁻¹' s)

The translation of a convex set is also convex.

theorem convex_Iic {𝕜 : Type u_1} {β : Type u_4} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid β] [PartialOrder β] [IsOrderedAddMonoid β] [Module 𝕜 β] [PosSMulMono 𝕜 β] (r : β) : Convex 𝕜 (Set.Iic r)

theorem convex_Ici {𝕜 : Type u_1} {β : Type u_4} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid β] [PartialOrder β] [IsOrderedAddMonoid β] [Module 𝕜 β] [PosSMulMono 𝕜 β] (r : β) : Convex 𝕜 (Set.Ici r)

theorem convex_Icc {𝕜 : Type u_1} {β : Type u_4} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid β] [PartialOrder β] [IsOrderedAddMonoid β] [Module 𝕜 β] [PosSMulMono 𝕜 β] (r s : β) : Convex 𝕜 (Set.Icc r s)

theorem convex_halfSpace_le {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] [AddCommMonoid β] [PartialOrder β] [IsOrderedAddMonoid β] [Module 𝕜 β] [PosSMulMono 𝕜 β] {f : E → β} (h : IsLinearMap 𝕜 f) (r : β) : Convex 𝕜 {w : E | f w ≤ r}

theorem convex_halfSpace_ge {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] [AddCommMonoid β] [PartialOrder β] [IsOrderedAddMonoid β] [Module 𝕜 β] [PosSMulMono 𝕜 β] {f : E → β} (h : IsLinearMap 𝕜 f) (r : β) : Convex 𝕜 {w : E | r ≤ f w}

theorem convex_hyperplane {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] [AddCommMonoid β] [PartialOrder β] [IsOrderedAddMonoid β] [Module 𝕜 β] [PosSMulMono 𝕜 β] {f : E → β} (h : IsLinearMap 𝕜 f) (r : β) : Convex 𝕜 {w : E | f w = r}

theorem convex_Iio {𝕜 : Type u_1} {β : Type u_4} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid β] [PartialOrder β] [IsOrderedCancelAddMonoid β] [Module 𝕜 β] [PosSMulStrictMono 𝕜 β] (r : β) : Convex 𝕜 (Set.Iio r)

theorem convex_Ioi {𝕜 : Type u_1} {β : Type u_4} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid β] [PartialOrder β] [IsOrderedCancelAddMonoid β] [Module 𝕜 β] [PosSMulStrictMono 𝕜 β] (r : β) : Convex 𝕜 (Set.Ioi r)

theorem convex_Ioo {𝕜 : Type u_1} {β : Type u_4} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid β] [PartialOrder β] [IsOrderedCancelAddMonoid β] [Module 𝕜 β] [PosSMulStrictMono 𝕜 β] (r s : β) : Convex 𝕜 (Set.Ioo r s)

theorem convex_Ico {𝕜 : Type u_1} {β : Type u_4} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid β] [PartialOrder β] [IsOrderedCancelAddMonoid β] [Module 𝕜 β] [PosSMulStrictMono 𝕜 β] (r s : β) : Convex 𝕜 (Set.Ico r s)

theorem convex_Ioc {𝕜 : Type u_1} {β : Type u_4} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid β] [PartialOrder β] [IsOrderedCancelAddMonoid β] [Module 𝕜 β] [PosSMulStrictMono 𝕜 β] (r s : β) : Convex 𝕜 (Set.Ioc r s)

theorem convex_halfSpace_lt {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] [AddCommMonoid β] [PartialOrder β] [IsOrderedCancelAddMonoid β] [Module 𝕜 β] [PosSMulStrictMono 𝕜 β] {f : E → β} (h : IsLinearMap 𝕜 f) (r : β) : Convex 𝕜 {w : E | f w < r}

theorem convex_halfSpace_gt {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] [AddCommMonoid β] [PartialOrder β] [IsOrderedCancelAddMonoid β] [Module 𝕜 β] [PosSMulStrictMono 𝕜 β] {f : E → β} (h : IsLinearMap 𝕜 f) (r : β) : Convex 𝕜 {w : E | r < f w}

theorem convex_uIcc {𝕜 : Type u_1} {β : Type u_4} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid β] [LinearOrder β] [IsOrderedAddMonoid β] [Module 𝕜 β] [PosSMulMono 𝕜 β] (r s : β) : Convex 𝕜 (Set.uIcc r s)

theorem Convex.lift {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [ZeroLEOneClass 𝕜] [Module 𝕜 E] (R : Type u_5) [Semiring R] [PartialOrder R] [Module R E] [Module R 𝕜] [IsScalarTower R 𝕜 E] [SMulPosMono R 𝕜] {s : Set E} (hs : Convex 𝕜 s) : Convex R s

Lift the convexity of a set up through a scalar tower.

theorem MonotoneOn.convex_le {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [LinearOrder E] [IsOrderedAddMonoid E] [PartialOrder β] [Module 𝕜 E] [PosSMulMono 𝕜 E] {s : Set E} {f : E → β} (hf : MonotoneOn f s) (hs : Convex 𝕜 s) (r : β) : Convex 𝕜 {x : E | x ∈ s ∧ f x ≤ r}

theorem MonotoneOn.convex_lt {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [LinearOrder E] [IsOrderedAddMonoid E] [PartialOrder β] [Module 𝕜 E] [PosSMulMono 𝕜 E] {s : Set E} {f : E → β} (hf : MonotoneOn f s) (hs : Convex 𝕜 s) (r : β) : Convex 𝕜 {x : E | x ∈ s ∧ f x < r}

theorem MonotoneOn.convex_ge {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [LinearOrder E] [IsOrderedAddMonoid E] [PartialOrder β] [Module 𝕜 E] [PosSMulMono 𝕜 E] {s : Set E} {f : E → β} (hf : MonotoneOn f s) (hs : Convex 𝕜 s) (r : β) : Convex 𝕜 {x : E | x ∈ s ∧ r ≤ f x}

theorem MonotoneOn.convex_gt {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [LinearOrder E] [IsOrderedAddMonoid E] [PartialOrder β] [Module 𝕜 E] [PosSMulMono 𝕜 E] {s : Set E} {f : E → β} (hf : MonotoneOn f s) (hs : Convex 𝕜 s) (r : β) : Convex 𝕜 {x : E | x ∈ s ∧ r < f x}

theorem AntitoneOn.convex_le {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [LinearOrder E] [IsOrderedAddMonoid E] [PartialOrder β] [Module 𝕜 E] [PosSMulMono 𝕜 E] {s : Set E} {f : E → β} (hf : AntitoneOn f s) (hs : Convex 𝕜 s) (r : β) : Convex 𝕜 {x : E | x ∈ s ∧ f x ≤ r}

theorem AntitoneOn.convex_lt {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [LinearOrder E] [IsOrderedAddMonoid E] [PartialOrder β] [Module 𝕜 E] [PosSMulMono 𝕜 E] {s : Set E} {f : E → β} (hf : AntitoneOn f s) (hs : Convex 𝕜 s) (r : β) : Convex 𝕜 {x : E | x ∈ s ∧ f x < r}

theorem AntitoneOn.convex_ge {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [LinearOrder E] [IsOrderedAddMonoid E] [PartialOrder β] [Module 𝕜 E] [PosSMulMono 𝕜 E] {s : Set E} {f : E → β} (hf : AntitoneOn f s) (hs : Convex 𝕜 s) (r : β) : Convex 𝕜 {x : E | x ∈ s ∧ r ≤ f x}

theorem AntitoneOn.convex_gt {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [LinearOrder E] [IsOrderedAddMonoid E] [PartialOrder β] [Module 𝕜 E] [PosSMulMono 𝕜 E] {s : Set E} {f : E → β} (hf : AntitoneOn f s) (hs : Convex 𝕜 s) (r : β) : Convex 𝕜 {x : E | x ∈ s ∧ r < f x}

theorem Monotone.convex_le {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [LinearOrder E] [IsOrderedAddMonoid E] [PartialOrder β] [Module 𝕜 E] [PosSMulMono 𝕜 E] {f : E → β} (hf : Monotone f) (r : β) : Convex 𝕜 {x : E | f x ≤ r}

theorem Monotone.convex_lt {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [LinearOrder E] [IsOrderedAddMonoid E] [PartialOrder β] [Module 𝕜 E] [PosSMulMono 𝕜 E] {f : E → β} (hf : Monotone f) (r : β) : Convex 𝕜 {x : E | f x ≤ r}

theorem Monotone.convex_ge {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [LinearOrder E] [IsOrderedAddMonoid E] [PartialOrder β] [Module 𝕜 E] [PosSMulMono 𝕜 E] {f : E → β} (hf : Monotone f) (r : β) : Convex 𝕜 {x : E | r ≤ f x}

theorem Monotone.convex_gt {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [LinearOrder E] [IsOrderedAddMonoid E] [PartialOrder β] [Module 𝕜 E] [PosSMulMono 𝕜 E] {f : E → β} (hf : Monotone f) (r : β) : Convex 𝕜 {x : E | f x ≤ r}

theorem Antitone.convex_le {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [LinearOrder E] [IsOrderedAddMonoid E] [PartialOrder β] [Module 𝕜 E] [PosSMulMono 𝕜 E] {f : E → β} (hf : Antitone f) (r : β) : Convex 𝕜 {x : E | f x ≤ r}

theorem Antitone.convex_lt {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [LinearOrder E] [IsOrderedAddMonoid E] [PartialOrder β] [Module 𝕜 E] [PosSMulMono 𝕜 E] {f : E → β} (hf : Antitone f) (r : β) : Convex 𝕜 {x : E | f x < r}

theorem Antitone.convex_ge {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [LinearOrder E] [IsOrderedAddMonoid E] [PartialOrder β] [Module 𝕜 E] [PosSMulMono 𝕜 E] {f : E → β} (hf : Antitone f) (r : β) : Convex 𝕜 {x : E | r ≤ f x}

theorem Antitone.convex_gt {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [LinearOrder E] [IsOrderedAddMonoid E] [PartialOrder β] [Module 𝕜 E] [PosSMulMono 𝕜 E] {f : E → β} (hf : Antitone f) (r : β) : Convex 𝕜 {x : E | r < f x}

theorem Convex.smul {𝕜 : Type u_1} {E : Type u_2} [CommSemiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] {s : Set E} (hs : Convex 𝕜 s) (c : 𝕜) : Convex 𝕜 (c • s)

theorem Convex.smul_preimage {𝕜 : Type u_1} {E : Type u_2} [CommSemiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] {s : Set E} (hs : Convex 𝕜 s) (c : 𝕜) : Convex 𝕜 ((fun (z : E) => c • z) ⁻¹' s)

theorem Convex.affinity {𝕜 : Type u_1} {E : Type u_2} [CommSemiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] {s : Set E} (hs : Convex 𝕜 s) (z : E) (c : 𝕜) : Convex 𝕜 ((fun (x : E) => z + c • x) '' s)

theorem convex_openSegment {𝕜 : Type u_1} {E : Type u_2} [CommSemiring 𝕜] [PartialOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] (a b : E) : Convex 𝕜 (openSegment 𝕜 a b)

@[simp]

theorem convex_vadd {𝕜 : Type u_1} {E : Type u_2} [Ring 𝕜] [PartialOrder 𝕜] [AddCommGroup E] [Module 𝕜 E] {s : Set E} (a : E) : Convex 𝕜 (a +ᵥ s) ↔ Convex 𝕜 s

theorem AffineSubspace.convex {𝕜 : Type u_1} {E : Type u_2} [Ring 𝕜] [PartialOrder 𝕜] [AddCommGroup E] [Module 𝕜 E] (Q : AffineSubspace 𝕜 E) : Convex 𝕜 ↑Q

Affine subspaces are convex.

theorem Convex.affine_preimage {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [Ring 𝕜] [PartialOrder 𝕜] [AddCommGroup E] [AddCommGroup F] [Module 𝕜 E] [Module 𝕜 F] (f : E →ᵃ[𝕜] F) {s : Set F} (hs : Convex 𝕜 s) : Convex 𝕜 (⇑f ⁻¹' s)

The preimage of a convex set under an affine map is convex.

theorem Convex.affine_image {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [Ring 𝕜] [PartialOrder 𝕜] [AddCommGroup E] [AddCommGroup F] [Module 𝕜 E] [Module 𝕜 F] {s : Set E} (f : E →ᵃ[𝕜] F) (hs : Convex 𝕜 s) : Convex 𝕜 (⇑f '' s)

The image of a convex set under an affine map is convex.

theorem Convex.neg {𝕜 : Type u_1} {E : Type u_2} [Ring 𝕜] [PartialOrder 𝕜] [AddCommGroup E] [Module 𝕜 E] {s : Set E} (hs : Convex 𝕜 s) : Convex 𝕜 (-s)

theorem Convex.sub {𝕜 : Type u_1} {E : Type u_2} [Ring 𝕜] [PartialOrder 𝕜] [AddCommGroup E] [Module 𝕜 E] {s t : Set E} (hs : Convex 𝕜 s) (ht : Convex 𝕜 t) : Convex 𝕜 (s - t)

theorem Convex.add_smul_mem {𝕜 : Type u_1} {E : Type u_2} [Ring 𝕜] [PartialOrder 𝕜] [AddCommGroup E] [Module 𝕜 E] {s : Set E} [AddRightMono 𝕜] (hs : Convex 𝕜 s) {x y : E} (hx : x ∈ s) (hy : x + y ∈ s) {t : 𝕜} (ht : t ∈ Set.Icc 0 1) : x + t • y ∈ s

theorem Convex.smul_mem_of_zero_mem {𝕜 : Type u_1} {E : Type u_2} [Ring 𝕜] [PartialOrder 𝕜] [AddCommGroup E] [Module 𝕜 E] {s : Set E} [AddRightMono 𝕜] (hs : Convex 𝕜 s) {x : E} (zero_mem : 0 ∈ s) (hx : x ∈ s) {t : 𝕜} (ht : t ∈ Set.Icc 0 1) : t • x ∈ s

theorem Convex.mapsTo_lineMap {𝕜 : Type u_1} {E : Type u_2} [Ring 𝕜] [PartialOrder 𝕜] [AddCommGroup E] [Module 𝕜 E] {s : Set E} [AddRightMono 𝕜] (h : Convex 𝕜 s) {x y : E} (hx : x ∈ s) (hy : y ∈ s) : Set.MapsTo (⇑(AffineMap.lineMap x y)) (Set.Icc 0 1) s

theorem Convex.lineMap_mem {𝕜 : Type u_1} {E : Type u_2} [Ring 𝕜] [PartialOrder 𝕜] [AddCommGroup E] [Module 𝕜 E] {s : Set E} [AddRightMono 𝕜] (h : Convex 𝕜 s) {x y : E} (hx : x ∈ s) (hy : y ∈ s) {t : 𝕜} (ht : t ∈ Set.Icc 0 1) : (AffineMap.lineMap x y) t ∈ s

theorem Convex.add_smul_sub_mem {𝕜 : Type u_1} {E : Type u_2} [Ring 𝕜] [PartialOrder 𝕜] [AddCommGroup E] [Module 𝕜 E] {s : Set E} [AddRightMono 𝕜] (h : Convex 𝕜 s) {x y : E} (hx : x ∈ s) (hy : y ∈ s) {t : 𝕜} (ht : t ∈ Set.Icc 0 1) : x + t • (y - x) ∈ s

theorem Convex.semilinear_image {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [AddCommMonoid E] [PartialOrder 𝕜] {𝕜' : Type u_5} [Semiring 𝕜'] [PartialOrder 𝕜'] {σ : 𝕜 →+* 𝕜'} [RingHomSurjective σ] {F' : Type u_6} [AddCommMonoid F'] [Module 𝕜' F'] [Module 𝕜 E] {s : Set E} (hs : Convex 𝕜 s) (hσ : ∀ {s t : 𝕜}, σ s ≤ σ t ↔ s ≤ t) (f : E →ₛₗ[σ] F') : Convex 𝕜' (⇑f '' s)

theorem Convex_subadditive_le {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [AddCommMonoid E] [LinearOrder 𝕜] [IsOrderedRing 𝕜] [SMul 𝕜 E] {f : E → 𝕜} (hf1 : ∀ (x y : E), f (x + y) ≤ f x + f y) (hf2 : ∀ ⦃c : 𝕜⦄ (x : E), 0 ≤ c → f (c • x) ≤ c * f x) (B : 𝕜) : Convex 𝕜 {x : E | f x ≤ B}

theorem Convex.midpoint_mem {𝕜 : Type u_1} {E : Type u_2} [Ring 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] [Invertible 2] {s : Set E} {x y : E} (h : Convex 𝕜 s) (hx : x ∈ s) (hy : y ∈ s) : midpoint 𝕜 x y ∈ s

theorem convex_iff_div {𝕜 : Type u_1} {E : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {s : Set E} : Convex 𝕜 s ↔ ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → 0 < a + b → (a / (a + b)) • x + (b / (a + b)) • y ∈ s

Alternative definition of set convexity, using division.

theorem Convex.mem_smul_of_zero_mem {𝕜 : Type u_1} {E : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {s : Set E} (h : Convex 𝕜 s) {x : E} (zero_mem : 0 ∈ s) (hx : x ∈ s) {t : 𝕜} (ht : 1 ≤ t) : x ∈ t • s

theorem Convex.exists_mem_add_smul_eq {𝕜 : Type u_1} {E : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {s : Set E} (h : Convex 𝕜 s) {x y : E} {p q : 𝕜} (hx : x ∈ s) (hy : y ∈ s) (hp : 0 ≤ p) (hq : 0 ≤ q) : ∃ z ∈ s, (p + q) • z = p • x + q • y

theorem Convex.add_smul {𝕜 : Type u_1} {E : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {s : Set E} (h_conv : Convex 𝕜 s) {p q : 𝕜} (hp : 0 ≤ p) (hq : 0 ≤ q) : (p + q) • s = p • s + q • s

Convex sets in an ordered space

Relates Convex and OrdConnected.

theorem Set.OrdConnected.convex_of_chain {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [PartialOrder E] [IsOrderedAddMonoid E] [Module 𝕜 E] [PosSMulMono 𝕜 E] {s : Set E} (hs : s.OrdConnected) (h : IsChain (fun (x1 x2 : E) => x1 ≤ x2) s) : Convex 𝕜 s

theorem Set.OrdConnected.convex {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [LinearOrder E] [IsOrderedAddMonoid E] [Module 𝕜 E] [PosSMulMono 𝕜 E] {s : Set E} (hs : s.OrdConnected) : Convex 𝕜 s

theorem convex_iff_ordConnected {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {s : Set 𝕜} : Convex 𝕜 s ↔ s.OrdConnected

theorem Convex.ordConnected {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {s : Set 𝕜} : Convex 𝕜 s → s.OrdConnected

Alias of the forward direction of convex_iff_ordConnected.

Convexity of submodules/subspaces

theorem Submodule.convex {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] (K : Submodule 𝕜 E) : Convex 𝕜 ↑K

theorem Submodule.starConvex {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] (K : Submodule 𝕜 E) : StarConvex 𝕜 0 ↑K

theorem Submodule.Convex.semilinear_range {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] {𝕜' : Type u_5} [Semiring 𝕜'] {σ : 𝕜' →+* 𝕜} [RingHomSurjective σ] {F' : Type u_6} [AddCommMonoid F'] [Module 𝕜' F'] (f : F' →ₛₗ[σ] E) : Convex 𝕜 ↑f.range

theorem convex_of_nonneg_surjective_algebraMap {R : Type u_5} [CommSemiring R] (A : Type u_6) [Semiring A] [Algebra R A] {M : Type u_7} [AddCommMonoid M] [Module A M] [Module R M] [IsScalarTower R A M] [PartialOrder R] [PartialOrder A] [FaithfulSMul R A] {s : Set M} (halg : Set.Ici 0 ⊆ ⇑(algebraMap R A) '' Set.Ici 0) (hs : Convex R s) : Convex A s