Documentation

Mathlib.Analysis.Convex.Basic

Convex sets and functions in vector spaces #

In a π•œ-vector space, we define the following objects and properties.

We also provide various equivalent versions of the definitions above, 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} [OrderedSemiring π•œ] [AddCommMonoid E] [SMul π•œ E] (s : Set E) :

Convexity of sets.

Equations
Instances For
    theorem Convex.starConvex {π•œ : Type u_1} {E : Type u_2} [OrderedSemiring π•œ] [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} [OrderedSemiring π•œ] [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} [OrderedSemiring π•œ] [AddCommMonoid E] [SMul π•œ E] {s : Set E} (h : Convex π•œ s) {x : E} {y : E} (hx : x ∈ s) (hy : y ∈ s) :
    segment π•œ x y βŠ† s
    theorem Convex.openSegment_subset {π•œ : Type u_1} {E : Type u_2} [OrderedSemiring π•œ] [AddCommMonoid E] [SMul π•œ E] {s : Set E} (h : Convex π•œ s) {x : E} {y : E} (hx : x ∈ s) (hy : y ∈ s) :
    openSegment π•œ x y βŠ† s
    theorem convex_iff_pointwise_add_subset {π•œ : Type u_1} {E : Type u_2} [OrderedSemiring π•œ] [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} [OrderedSemiring π•œ] [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} [OrderedSemiring π•œ] [AddCommMonoid E] [SMul π•œ E] :
    Convex π•œ βˆ…
    theorem convex_univ {π•œ : Type u_1} {E : Type u_2} [OrderedSemiring π•œ] [AddCommMonoid E] [SMul π•œ E] :
    Convex π•œ Set.univ
    theorem Convex.inter {π•œ : Type u_1} {E : Type u_2} [OrderedSemiring π•œ] [AddCommMonoid E] [SMul π•œ E] {s : Set E} {t : Set E} (hs : Convex π•œ s) (ht : Convex π•œ t) :
    Convex π•œ (s ∩ t)
    theorem convex_sInter {π•œ : Type u_1} {E : Type u_2} [OrderedSemiring π•œ] [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} [OrderedSemiring π•œ] [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} [OrderedSemiring π•œ] [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} [OrderedSemiring π•œ] [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} [OrderedSemiring π•œ] {ΞΉ : 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} [OrderedSemiring π•œ] [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} [OrderedSemiring π•œ] [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_iff_openSegment_subset {π•œ : Type u_1} {E : Type u_2} [OrderedSemiring π•œ] [AddCommMonoid E] [Module π•œ E] {s : Set E} :
    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} [OrderedSemiring π•œ] [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} [OrderedSemiring π•œ] [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} [OrderedSemiring π•œ] [AddCommMonoid E] [Module π•œ E] {s : Set E} {x : E} (hs : Convex π•œ s) (h : s.Nonempty) :
    StarConvex π•œ x s ↔ x ∈ s
    theorem Set.Subsingleton.convex {π•œ : Type u_1} {E : Type u_2} [OrderedSemiring π•œ] [AddCommMonoid E] [Module π•œ E] {s : Set E} (h : s.Subsingleton) :
    Convex π•œ s
    theorem convex_singleton {π•œ : Type u_1} {E : Type u_2} [OrderedSemiring π•œ] [AddCommMonoid E] [Module π•œ E] (c : E) :
    Convex π•œ {c}
    theorem convex_zero {π•œ : Type u_1} {E : Type u_2} [OrderedSemiring π•œ] [AddCommMonoid E] [Module π•œ E] :
    Convex π•œ 0
    theorem convex_segment {π•œ : Type u_1} {E : Type u_2} [OrderedSemiring π•œ] [AddCommMonoid E] [Module π•œ E] (x : E) (y : E) :
    Convex π•œ (segment π•œ x y)
    theorem Convex.linear_image {π•œ : Type u_1} {E : Type u_2} {F : Type u_3} [OrderedSemiring π•œ] [AddCommMonoid E] [AddCommMonoid F] [Module π•œ E] [Module π•œ F] {s : Set E} (hs : Convex π•œ s) (f : E β†’β‚—[π•œ] F) :
    Convex π•œ (⇑f '' s)
    theorem Convex.is_linear_image {π•œ : Type u_1} {E : Type u_2} {F : Type u_3} [OrderedSemiring π•œ] [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} [OrderedSemiring π•œ] [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} [OrderedSemiring π•œ] [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} [OrderedSemiring π•œ] [AddCommMonoid E] [Module π•œ E] {s : Set E} {t : Set E} (hs : Convex π•œ s) (ht : Convex π•œ t) :
    Convex π•œ (s + t)
    def convexAddSubmonoid (π•œ : Type u_1) (E : Type u_2) [OrderedSemiring π•œ] [AddCommMonoid E] [Module π•œ E] :

    The convex sets form an additive submonoid under pointwise addition.

    Equations
    Instances For
      @[simp]
      theorem coe_convexAddSubmonoid (π•œ : Type u_1) (E : Type u_2) [OrderedSemiring π•œ] [AddCommMonoid E] [Module π•œ E] :
      ↑(convexAddSubmonoid π•œ E) = {s : Set E | Convex π•œ s}
      @[simp]
      theorem mem_convexAddSubmonoid {π•œ : Type u_1} {E : Type u_2} [OrderedSemiring π•œ] [AddCommMonoid E] [Module π•œ E] {s : Set E} :
      s ∈ convexAddSubmonoid π•œ E ↔ Convex π•œ s
      theorem convex_list_sum {π•œ : Type u_1} {E : Type u_2} [OrderedSemiring π•œ] [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} [OrderedSemiring π•œ] [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} [OrderedSemiring π•œ] [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} [OrderedSemiring π•œ] [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} [OrderedSemiring π•œ] [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} [OrderedSemiring π•œ] [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} [OrderedSemiring π•œ] [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} [OrderedSemiring π•œ] [OrderedAddCommMonoid Ξ²] [Module π•œ Ξ²] [OrderedSMul π•œ Ξ²] (r : Ξ²) :
      Convex π•œ (Set.Iic r)
      theorem convex_Ici {π•œ : Type u_1} {Ξ² : Type u_4} [OrderedSemiring π•œ] [OrderedAddCommMonoid Ξ²] [Module π•œ Ξ²] [OrderedSMul π•œ Ξ²] (r : Ξ²) :
      Convex π•œ (Set.Ici r)
      theorem convex_Icc {π•œ : Type u_1} {Ξ² : Type u_4} [OrderedSemiring π•œ] [OrderedAddCommMonoid Ξ²] [Module π•œ Ξ²] [OrderedSMul π•œ Ξ²] (r : Ξ²) (s : Ξ²) :
      Convex π•œ (Set.Icc r s)
      theorem convex_halfspace_le {π•œ : Type u_1} {E : Type u_2} {Ξ² : Type u_4} [OrderedSemiring π•œ] [AddCommMonoid E] [Module π•œ E] [OrderedAddCommMonoid Ξ²] [Module π•œ Ξ²] [OrderedSMul π•œ Ξ²] {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} [OrderedSemiring π•œ] [AddCommMonoid E] [Module π•œ E] [OrderedAddCommMonoid Ξ²] [Module π•œ Ξ²] [OrderedSMul π•œ Ξ²] {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} [OrderedSemiring π•œ] [AddCommMonoid E] [Module π•œ E] [OrderedAddCommMonoid Ξ²] [Module π•œ Ξ²] [OrderedSMul π•œ Ξ²] {f : E β†’ Ξ²} (h : IsLinearMap π•œ f) (r : Ξ²) :
      Convex π•œ {w : E | f w = r}
      theorem convex_Iio {π•œ : Type u_1} {Ξ² : Type u_4} [OrderedSemiring π•œ] [OrderedCancelAddCommMonoid Ξ²] [Module π•œ Ξ²] [OrderedSMul π•œ Ξ²] (r : Ξ²) :
      Convex π•œ (Set.Iio r)
      theorem convex_Ioi {π•œ : Type u_1} {Ξ² : Type u_4} [OrderedSemiring π•œ] [OrderedCancelAddCommMonoid Ξ²] [Module π•œ Ξ²] [OrderedSMul π•œ Ξ²] (r : Ξ²) :
      Convex π•œ (Set.Ioi r)
      theorem convex_Ioo {π•œ : Type u_1} {Ξ² : Type u_4} [OrderedSemiring π•œ] [OrderedCancelAddCommMonoid Ξ²] [Module π•œ Ξ²] [OrderedSMul π•œ Ξ²] (r : Ξ²) (s : Ξ²) :
      Convex π•œ (Set.Ioo r s)
      theorem convex_Ico {π•œ : Type u_1} {Ξ² : Type u_4} [OrderedSemiring π•œ] [OrderedCancelAddCommMonoid Ξ²] [Module π•œ Ξ²] [OrderedSMul π•œ Ξ²] (r : Ξ²) (s : Ξ²) :
      Convex π•œ (Set.Ico r s)
      theorem convex_Ioc {π•œ : Type u_1} {Ξ² : Type u_4} [OrderedSemiring π•œ] [OrderedCancelAddCommMonoid Ξ²] [Module π•œ Ξ²] [OrderedSMul π•œ Ξ²] (r : Ξ²) (s : Ξ²) :
      Convex π•œ (Set.Ioc r s)
      theorem convex_halfspace_lt {π•œ : Type u_1} {E : Type u_2} {Ξ² : Type u_4} [OrderedSemiring π•œ] [AddCommMonoid E] [Module π•œ E] [OrderedCancelAddCommMonoid Ξ²] [Module π•œ Ξ²] [OrderedSMul π•œ Ξ²] {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} [OrderedSemiring π•œ] [AddCommMonoid E] [Module π•œ E] [OrderedCancelAddCommMonoid Ξ²] [Module π•œ Ξ²] [OrderedSMul π•œ Ξ²] {f : E β†’ Ξ²} (h : IsLinearMap π•œ f) (r : Ξ²) :
      Convex π•œ {w : E | r < f w}
      theorem convex_uIcc {π•œ : Type u_1} {Ξ² : Type u_4} [OrderedSemiring π•œ] [LinearOrderedAddCommMonoid Ξ²] [Module π•œ Ξ²] [OrderedSMul π•œ Ξ²] (r : Ξ²) (s : Ξ²) :
      Convex π•œ (Set.uIcc r s)
      theorem MonotoneOn.convex_le {π•œ : Type u_1} {E : Type u_2} {Ξ² : Type u_4} [OrderedSemiring π•œ] [LinearOrderedAddCommMonoid E] [OrderedAddCommMonoid Ξ²] [Module π•œ E] [OrderedSMul π•œ 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} [OrderedSemiring π•œ] [LinearOrderedAddCommMonoid E] [OrderedAddCommMonoid Ξ²] [Module π•œ E] [OrderedSMul π•œ 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} [OrderedSemiring π•œ] [LinearOrderedAddCommMonoid E] [OrderedAddCommMonoid Ξ²] [Module π•œ E] [OrderedSMul π•œ 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} [OrderedSemiring π•œ] [LinearOrderedAddCommMonoid E] [OrderedAddCommMonoid Ξ²] [Module π•œ E] [OrderedSMul π•œ 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} [OrderedSemiring π•œ] [LinearOrderedAddCommMonoid E] [OrderedAddCommMonoid Ξ²] [Module π•œ E] [OrderedSMul π•œ 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} [OrderedSemiring π•œ] [LinearOrderedAddCommMonoid E] [OrderedAddCommMonoid Ξ²] [Module π•œ E] [OrderedSMul π•œ 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} [OrderedSemiring π•œ] [LinearOrderedAddCommMonoid E] [OrderedAddCommMonoid Ξ²] [Module π•œ E] [OrderedSMul π•œ 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} [OrderedSemiring π•œ] [LinearOrderedAddCommMonoid E] [OrderedAddCommMonoid Ξ²] [Module π•œ E] [OrderedSMul π•œ 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} [OrderedSemiring π•œ] [LinearOrderedAddCommMonoid E] [OrderedAddCommMonoid Ξ²] [Module π•œ E] [OrderedSMul π•œ 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} [OrderedSemiring π•œ] [LinearOrderedAddCommMonoid E] [OrderedAddCommMonoid Ξ²] [Module π•œ E] [OrderedSMul π•œ 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} [OrderedSemiring π•œ] [LinearOrderedAddCommMonoid E] [OrderedAddCommMonoid Ξ²] [Module π•œ E] [OrderedSMul π•œ 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} [OrderedSemiring π•œ] [LinearOrderedAddCommMonoid E] [OrderedAddCommMonoid Ξ²] [Module π•œ E] [OrderedSMul π•œ 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} [OrderedSemiring π•œ] [LinearOrderedAddCommMonoid E] [OrderedAddCommMonoid Ξ²] [Module π•œ E] [OrderedSMul π•œ 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} [OrderedSemiring π•œ] [LinearOrderedAddCommMonoid E] [OrderedAddCommMonoid Ξ²] [Module π•œ E] [OrderedSMul π•œ 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} [OrderedSemiring π•œ] [LinearOrderedAddCommMonoid E] [OrderedAddCommMonoid Ξ²] [Module π•œ E] [OrderedSMul π•œ 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} [OrderedSemiring π•œ] [LinearOrderedAddCommMonoid E] [OrderedAddCommMonoid Ξ²] [Module π•œ E] [OrderedSMul π•œ E] {f : E β†’ Ξ²} (hf : Antitone f) (r : Ξ²) :
      Convex π•œ {x : E | r < f x}
      theorem Convex.smul {π•œ : Type u_1} {E : Type u_2} [OrderedCommSemiring π•œ] [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} [OrderedCommSemiring π•œ] [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} [OrderedCommSemiring π•œ] [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} [StrictOrderedCommSemiring π•œ] [AddCommGroup E] [Module π•œ E] (a : E) (b : E) :
      Convex π•œ (openSegment π•œ a b)
      @[simp]
      theorem convex_vadd {π•œ : Type u_1} {E : Type u_2} [OrderedRing π•œ] [AddCommGroup E] [Module π•œ E] {s : Set E} (a : E) :
      Convex π•œ (a +α΅₯ s) ↔ Convex π•œ s
      theorem Convex.add_smul_mem {π•œ : Type u_1} {E : Type u_2} [OrderedRing π•œ] [AddCommGroup E] [Module π•œ E] {s : Set E} (hs : Convex π•œ s) {x : E} {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} [OrderedRing π•œ] [AddCommGroup E] [Module π•œ E] {s : Set E} (hs : Convex π•œ s) {x : E} (zero_mem : 0 ∈ s) (hx : x ∈ s) {t : π•œ} (ht : t ∈ Set.Icc 0 1) :
      theorem Convex.mapsTo_lineMap {π•œ : Type u_1} {E : Type u_2} [OrderedRing π•œ] [AddCommGroup E] [Module π•œ E] {s : Set E} (h : Convex π•œ s) {x : E} {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} [OrderedRing π•œ] [AddCommGroup E] [Module π•œ E] {s : Set E} (h : Convex π•œ s) {x : E} {y : E} (hx : x ∈ s) (hy : y ∈ s) {t : π•œ} (ht : t ∈ Set.Icc 0 1) :
      theorem Convex.add_smul_sub_mem {π•œ : Type u_1} {E : Type u_2} [OrderedRing π•œ] [AddCommGroup E] [Module π•œ E] {s : Set E} (h : Convex π•œ s) {x : E} {y : E} (hx : x ∈ s) (hy : y ∈ s) {t : π•œ} (ht : t ∈ Set.Icc 0 1) :
      x + t β€’ (y - x) ∈ s
      theorem AffineSubspace.convex {π•œ : Type u_1} {E : Type u_2} [OrderedRing π•œ] [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} [OrderedRing π•œ] [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} [OrderedRing π•œ] [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} [OrderedRing π•œ] [AddCommGroup E] [Module π•œ E] {s : Set E} (hs : Convex π•œ s) :
      Convex π•œ (-s)
      theorem Convex.sub {π•œ : Type u_1} {E : Type u_2} [OrderedRing π•œ] [AddCommGroup E] [Module π•œ E] {s : Set E} {t : Set E} (hs : Convex π•œ s) (ht : Convex π•œ t) :
      Convex π•œ (s - t)
      theorem Convex_subadditive_le {π•œ : Type u_1} {E : Type u_2} [LinearOrderedRing π•œ] [AddCommMonoid E] [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_iff_div {π•œ : Type u_1} {E : Type u_2} [LinearOrderedField π•œ] [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} [LinearOrderedField π•œ] [AddCommGroup E] [Module π•œ E] {s : Set E} (h : Convex π•œ s) {x : E} (zero_mem : 0 ∈ s) (hx : x ∈ s) {t : π•œ} (ht : 1 ≀ t) :
      theorem Convex.exists_mem_add_smul_eq {π•œ : Type u_1} {E : Type u_2} [LinearOrderedField π•œ] [AddCommGroup E] [Module π•œ E] {s : Set E} (h : Convex π•œ s) {x : E} {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} [LinearOrderedField π•œ] [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} [OrderedSemiring π•œ] [OrderedAddCommMonoid E] [Module π•œ E] [OrderedSMul π•œ 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} [OrderedSemiring π•œ] [LinearOrderedAddCommMonoid E] [Module π•œ E] [OrderedSMul π•œ E] {s : Set E} (hs : s.OrdConnected) :
      Convex π•œ s
      theorem convex_iff_ordConnected {π•œ : Type u_1} [LinearOrderedField π•œ] {s : Set π•œ} :
      Convex π•œ s ↔ s.OrdConnected
      theorem Convex.ordConnected {π•œ : Type u_1} [LinearOrderedField π•œ] {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} [OrderedSemiring π•œ] [AddCommMonoid E] [Module π•œ E] (K : Submodule π•œ E) :
      Convex π•œ ↑K
      theorem Submodule.starConvex {π•œ : Type u_1} {E : Type u_2} [OrderedSemiring π•œ] [AddCommMonoid E] [Module π•œ E] (K : Submodule π•œ E) :
      StarConvex π•œ 0 ↑K

      Simplex #

      def stdSimplex (π•œ : Type u_1) (ΞΉ : Type u_5) [OrderedSemiring π•œ] [Fintype ΞΉ] :
      Set (ΞΉ β†’ π•œ)

      The standard simplex in the space of functions ΞΉ β†’ π•œ is the set of vectors with non-negative coordinates with total sum 1. This is the free object in the category of convex spaces.

      Equations
      Instances For
        theorem stdSimplex_eq_inter (π•œ : Type u_1) (ΞΉ : Type u_5) [OrderedSemiring π•œ] [Fintype ΞΉ] :
        stdSimplex π•œ ΞΉ = (β‹‚ (x : ΞΉ), {f : ΞΉ β†’ π•œ | 0 ≀ f x}) ∩ {f : ΞΉ β†’ π•œ | βˆ‘ x : ΞΉ, f x = 1}
        theorem convex_stdSimplex (π•œ : Type u_1) (ΞΉ : Type u_5) [OrderedSemiring π•œ] [Fintype ΞΉ] :
        Convex π•œ (stdSimplex π•œ ΞΉ)
        theorem stdSimplex_of_subsingleton (π•œ : Type u_1) (ΞΉ : Type u_5) [OrderedSemiring π•œ] [Fintype ΞΉ] [Subsingleton π•œ] :
        stdSimplex π•œ ΞΉ = Set.univ
        theorem stdSimplex_of_isEmpty_index (π•œ : Type u_1) (ΞΉ : Type u_5) [OrderedSemiring π•œ] [Fintype ΞΉ] [IsEmpty ΞΉ] [Nontrivial π•œ] :
        stdSimplex π•œ ΞΉ = βˆ…

        The standard simplex in the zero-dimensional space is empty.

        theorem stdSimplex_unique (π•œ : Type u_1) (ΞΉ : Type u_5) [OrderedSemiring π•œ] [Fintype ΞΉ] [Nonempty ΞΉ] [Subsingleton ΞΉ] :
        stdSimplex π•œ ΞΉ = {fun (x : ΞΉ) => 1}
        theorem single_mem_stdSimplex (π•œ : Type u_1) {ΞΉ : Type u_5} [OrderedSemiring π•œ] [Fintype ΞΉ] [DecidableEq ΞΉ] (i : ΞΉ) :
        Pi.single i 1 ∈ stdSimplex π•œ ΞΉ
        theorem ite_eq_mem_stdSimplex (π•œ : Type u_1) {ΞΉ : Type u_5} [OrderedSemiring π•œ] [Fintype ΞΉ] [DecidableEq ΞΉ] (i : ΞΉ) :
        (fun (x : ΞΉ) => if i = x then 1 else 0) ∈ stdSimplex π•œ ΞΉ
        theorem segment_single_subset_stdSimplex (π•œ : Type u_1) {ΞΉ : Type u_5} [OrderedSemiring π•œ] [Fintype ΞΉ] [DecidableEq ΞΉ] (i : ΞΉ) (j : ΞΉ) :
        segment π•œ (Pi.single i 1) (Pi.single j 1) βŠ† stdSimplex π•œ ΞΉ

        The edges are contained in the simplex.

        theorem stdSimplex_fin_two (π•œ : Type u_1) [OrderedSemiring π•œ] :
        stdSimplex π•œ (Fin 2) = segment π•œ (Pi.single 0 1) (Pi.single 1 1)
        @[simp]
        theorem stdSimplexEquivIcc_apply_coe (π•œ : Type u_1) [OrderedRing π•œ] (f : ↑(stdSimplex π•œ (Fin 2))) :
        ↑((stdSimplexEquivIcc π•œ) f) = ↑f 0
        @[simp]
        theorem stdSimplexEquivIcc_symm_apply_coe (π•œ : Type u_1) [OrderedRing π•œ] (x : ↑(Set.Icc 0 1)) :
        ↑((stdSimplexEquivIcc π•œ).symm x) = ![↑x, 1 - ↑x]
        def stdSimplexEquivIcc (π•œ : Type u_1) [OrderedRing π•œ] :
        ↑(stdSimplex π•œ (Fin 2)) ≃ ↑(Set.Icc 0 1)

        The standard one-dimensional simplex in Fin 2 β†’ π•œ is equivalent to the unit interval.

        Equations
        • stdSimplexEquivIcc π•œ = { toFun := fun (f : ↑(stdSimplex π•œ (Fin 2))) => βŸ¨β†‘f 0, β‹―βŸ©, invFun := fun (x : ↑(Set.Icc 0 1)) => ⟨![↑x, 1 - ↑x], β‹―βŸ©, left_inv := β‹―, right_inv := β‹― }
        Instances For