Mathlib.Analysis.Convex.Basic

Convex definition

: Prop

Full source

/-- Convexity of sets. -/
def Convex : Prop :=
  ∀ ⦃x : E⦄, x ∈ s → StarConvex 𝕜 x s

Convex set

Informal description

A set $s$ in a vector space $E$ over an ordered scalar field $\mathbb{K}$ is called *convex* if for every point $x \in s$, the set $s$ is star-convex with respect to $x$, meaning that for any $y \in s$, the line segment connecting $x$ and $y$ is entirely contained in $s$.

Convex.starConvex theorem

(hs : Convex 𝕜 s) (hx : x ∈ s) : StarConvex 𝕜 x s

Full source

theorem Convex.starConvex (hs : Convex 𝕜 s) (hx : x ∈ s) : StarConvex 𝕜 x s :=
  hs hx

Convex sets are star-convex at each of their points

Informal description

Let $s$ be a convex set in a vector space $E$ over an ordered scalar field $\mathbb{K}$, and let $x \in s$. Then $s$ is star-convex with respect to $x$, meaning that for any $y \in s$, the line segment connecting $x$ and $y$ is entirely contained in $s$.

convex_iff_segment_subset theorem

: Convex 𝕜 s ↔ ∀ ⦃x⦄, x ∈ s → ∀ ⦃y⦄, y ∈ s → [x -[𝕜] y] ⊆ s

Full source

theorem convex_iff_segment_subset : ConvexConvex 𝕜 s ↔ ∀ ⦃x⦄, x ∈ s → ∀ ⦃y⦄, y ∈ s → [x -[𝕜] y] ⊆ s :=
  forall₂_congr fun _ _ => starConvex_iff_segment_subset

Characterization of Convex Sets via Closed Segments

Informal description

A set $s$ in a vector space $E$ over an ordered scalar field $\mathbb{K}$ is convex if and only if for any two points $x, y \in s$, the closed segment $[x, y]$ connecting $x$ and $y$ is entirely contained in $s$.

Convex.segment_subset theorem

(h : Convex 𝕜 s) {x y : E} (hx : x ∈ s) (hy : y ∈ s) : [x -[𝕜] y] ⊆ s

Full source

theorem Convex.segment_subset (h : Convex 𝕜 s) {x y : E} (hx : x ∈ s) (hy : y ∈ s) :
    [x -[𝕜] y][x -[𝕜] y] ⊆ s :=
  convex_iff_segment_subset.1 h hx hy

Convexity Implies Segment Inclusion

Informal description

Let $s$ be a convex set in a vector space $E$ over an ordered scalar field $\mathbb{K}$. For any two points $x, y \in s$, the closed segment $[x, y]$ connecting $x$ and $y$ is entirely contained in $s$.

Convex.openSegment_subset theorem

(h : Convex 𝕜 s) {x y : E} (hx : x ∈ s) (hy : y ∈ s) : openSegment 𝕜 x y ⊆ s

Full source

theorem Convex.openSegment_subset (h : Convex 𝕜 s) {x y : E} (hx : x ∈ s) (hy : y ∈ s) :
    openSegmentopenSegment 𝕜 x y ⊆ s :=
  (openSegment_subset_segment 𝕜 x y).trans (h.segment_subset hx hy)

Convexity Implies Open Segment Inclusion

Informal description

Let $s$ be a convex set in a vector space $E$ over an ordered scalar field $\mathbb{K}$. For any two points $x, y \in s$, the open segment $(x, y)$ connecting $x$ and $y$ is entirely contained in $s$.

convex_iff_pointwise_add_subset theorem

: Convex 𝕜 s ↔ ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • s + b • s ⊆ s

Full source

/-- Alternative definition of set convexity, in terms of pointwise set operations. -/
theorem convex_iff_pointwise_add_subset :
    ConvexConvex 𝕜 s ↔ ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • s + b • s ⊆ s :=
  Iff.intro
    (by
      rintro hA a b ha hb hab w ⟨au, ⟨u, hu, rfl⟩, bv, ⟨v, hv, rfl⟩, rfl⟩
      exact hA hu hv ha hb hab)
    fun h _ hx _ hy _ _ ha hb hab => (h ha hb hab) (Set.add_mem_add ⟨_, hx, rfl⟩ ⟨_, hy, rfl⟩)

Characterization of Convex Sets via Minkowski Sum

Informal description

A set $s$ in a vector space $E$ over an ordered scalar field $\mathbb{K}$ is convex if and only if for any non-negative scalars $a, b \in \mathbb{K}$ with $a + b = 1$, the Minkowski sum $a \cdot s + b \cdot s$ is a subset of $s$.

convex_empty theorem

: Convex 𝕜 (∅ : Set E)

Full source

theorem convex_empty : Convex 𝕜 (∅ : Set E) := fun _ => False.elim

Empty Set is Convex

Informal description

The empty set is convex in any vector space $E$ over an ordered scalar field $\mathbb{K}$.

convex_univ theorem

: Convex 𝕜 (Set.univ : Set E)

Full source

theorem convex_univ : Convex 𝕜 (Set.univ : Set E) := fun _ _ => starConvex_univ _

Universal Set is Convex in Vector Space

Informal description

The universal set in a vector space $E$ over an ordered scalar field $\mathbb{K}$ is convex.

Convex.inter theorem

{t : Set E} (hs : Convex 𝕜 s) (ht : Convex 𝕜 t) : Convex 𝕜 (s ∩ t)

Full source

theorem Convex.inter {t : Set E} (hs : Convex 𝕜 s) (ht : Convex 𝕜 t) : Convex 𝕜 (s ∩ t) :=
  fun _ hx => (hs hx.1).inter (ht hx.2)

Intersection of Convex Sets is Convex

Informal description

Let $E$ be a vector space over an ordered scalar field $\mathbb{K}$. If two sets $s, t \subseteq E$ are convex, then their intersection $s \cap t$ is also convex.

convex_sInter theorem

{S : Set (Set E)} (h : ∀ s ∈ S, Convex 𝕜 s) : Convex 𝕜 (⋂₀ S)

Full source

theorem convex_sInter {S : Set (Set E)} (h : ∀ s ∈ S, Convex 𝕜 s) : Convex 𝕜 (⋂₀ S) := fun _ hx =>
  starConvex_sInter fun _ hs => h _ hs <| hx _ hs

Intersection of Convex Sets is Convex

Informal description

For any collection of sets $S$ in a vector space $E$ over an ordered scalar field $\mathbb{K}$, if every set $s \in S$ is convex, then the intersection $\bigcap_{s \in S} s$ is also convex.

convex_iInter theorem

{ι : Sort*} {s : ι → Set E} (h : ∀ i, Convex 𝕜 (s i)) : Convex 𝕜 (⋂ i, s i)

Full source

theorem convex_iInter {ι : Sort*} {s : ι → Set E} (h : ∀ i, Convex 𝕜 (s i)) :
    Convex 𝕜 (⋂ i, s i) :=
  sInter_range s ▸ convex_sInter <| forall_mem_range.2 h

Intersection of an Indexed Family of Convex Sets is Convex

Informal description

For any indexed family of sets $\{s_i\}_{i \in \iota}$ in a vector space $E$ over an ordered scalar field $\mathbb{K}$, if each set $s_i$ is convex, then the intersection $\bigcap_{i \in \iota} s_i$ is also convex.

convex_iInter₂ theorem

 {ι : Sort*} {κ : ι → Sort*} {s : (i : ι) → κ i → Set E} (h : ∀ i j, Convex 𝕜 (s i j)) : Convex 𝕜 (⋂ (i) (j), s i j)

Full source

theorem convex_iInter₂ {ι : Sort*} {κ : ι → Sort*} {s : (i : ι) → κ i → Set E}
    (h : ∀ i j, Convex 𝕜 (s i j)) : Convex 𝕜 (⋂ (i) (j), s i j) :=
  convex_iInter fun i => convex_iInter <| h i

Double Intersection of Convex Sets is Convex

Informal description

Let $\mathbb{K}$ be an ordered scalar field and $E$ a vector space over $\mathbb{K}$. Given an indexed family of sets $\{s_{i,j}\}_{i \in \iota, j \in \kappa(i)}$ in $E$, if each set $s_{i,j}$ is convex, then the intersection $\bigcap_{i \in \iota} \bigcap_{j \in \kappa(i)} s_{i,j}$ is also convex.

Convex.prod theorem

{s : Set E} {t : Set F} (hs : Convex 𝕜 s) (ht : Convex 𝕜 t) : Convex 𝕜 (s ×ˢ t)

Full source

theorem Convex.prod {s : Set E} {t : Set F} (hs : Convex 𝕜 s) (ht : Convex 𝕜 t) :
    Convex 𝕜 (s ×ˢ t) := fun _ hx => (hs hx.1).prod (ht hx.2)

Convexity of Cartesian Product of Convex Sets

Informal description

Let $E$ and $F$ be vector spaces over an ordered scalar field $\mathbb{K}$. If $s \subseteq E$ and $t \subseteq F$ are convex sets, then their Cartesian product $s \times t$ is convex in $E \times F$.

convex_pi theorem

 {ι : Type*} {E : ι → Type*} [∀ 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)

Full source

theorem convex_pi {ι : Type*} {E : ι → Type*} [∀ 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) :=
  fun _ hx => starConvex_pi fun _ hi => ht hi <| hx _ hi

Convexity of Product Sets in Vector Spaces

Informal description

Let $\mathbb{K}$ be an ordered scalar field, $\iota$ a type, and for each $i \in \iota$, let $E_i$ be an $\mathbb{K}$-vector space. Given a subset $s \subseteq \iota$ and a family of subsets $t_i \subseteq E_i$ for each $i \in s$, if each $t_i$ is convex in $E_i$ for $i \in s$, then the product set $\prod_{i \in s} t_i$ is convex in $\prod_{i \in \iota} E_i$.

Directed.convex_iUnion theorem

 {ι : Sort*} {s : ι → Set E} (hdir : Directed (· ⊆ ·) s) (hc : ∀ ⦃i : ι⦄, Convex 𝕜 (s i)) : Convex 𝕜 (⋃ i, s i)

Full source

theorem Directed.convex_iUnion {ι : Sort*} {s : ι → Set E} (hdir : Directed (· ⊆ ·) s)
    (hc : ∀ ⦃i : ι⦄, Convex 𝕜 (s i)) : Convex 𝕜 (⋃ i, s i) := by
  rintro x hx y hy a b ha hb hab
  rw [mem_iUnion] at hx hy ⊢
  obtain ⟨i, hx⟩ := hx
  obtain ⟨j, hy⟩ := hy
  obtain ⟨k, hik, hjk⟩ := hdir i j
  exact ⟨k, hc (hik hx) (hjk hy) ha hb hab⟩

Convexity of Directed Union of Convex Sets

Informal description

Let $\mathbb{K}$ be an ordered scalar field and $E$ a $\mathbb{K}$-vector space. Given a directed family of sets $\{s_i\}_{i \in \iota}$ in $E$ (with respect to the subset relation $\subseteq$) where each $s_i$ is convex, the union $\bigcup_{i \in \iota} s_i$ is also convex.

DirectedOn.convex_sUnion theorem

 {c : Set (Set E)} (hdir : DirectedOn (· ⊆ ·) c) (hc : ∀ ⦃A : Set E⦄, A ∈ c → Convex 𝕜 A) : Convex 𝕜 (⋃₀ c)

Full source

theorem DirectedOn.convex_sUnion {c : Set (Set E)} (hdir : DirectedOn (· ⊆ ·) c)
    (hc : ∀ ⦃A : Set E⦄, A ∈ c → Convex 𝕜 A) : Convex 𝕜 (⋃₀ c) := by
  rw [sUnion_eq_iUnion]
  exact (directedOn_iff_directed.1 hdir).convex_iUnion fun A => hc A.2

Convexity of Directed Union of Convex Sets in a Vector Space

Informal description

Let $\mathbb{K}$ be an ordered scalar field and $E$ a $\mathbb{K}$-vector space. Given a collection of sets $c$ in $E$ that is directed with respect to the subset relation $\subseteq$, and such that every set $A \in c$ is convex, then the union $\bigcup_{A \in c} A$ is also convex.

convex_iff_openSegment_subset theorem

[ZeroLEOneClass 𝕜] : Convex 𝕜 s ↔ ∀ ⦃x⦄, x ∈ s → ∀ ⦃y⦄, y ∈ s → openSegment 𝕜 x y ⊆ s

Full source

theorem convex_iff_openSegment_subset [ZeroLEOneClass 𝕜] :
    ConvexConvex 𝕜 s ↔ ∀ ⦃x⦄, x ∈ s → ∀ ⦃y⦄, y ∈ s → openSegment 𝕜 x y ⊆ s :=
  forall₂_congr fun _ => starConvex_iff_openSegment_subset

Characterization of Convex Sets via Open Segments

Informal description

A set $s$ in a vector space over an ordered scalar field $\mathbb{K}$ (where $0 \leq 1$) is convex if and only if for every pair of points $x, y \in s$, the open segment connecting $x$ and $y$ is entirely contained in $s$.

convex_iff_forall_pos theorem

 : Convex 𝕜 s ↔ ∀ ⦃x⦄, x ∈ s → ∀ ⦃y⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s

Full source

theorem convex_iff_forall_pos :
    ConvexConvex 𝕜 s ↔
      ∀ ⦃x⦄, x ∈ s → ∀ ⦃y⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s :=
  forall₂_congr fun _ => starConvex_iff_forall_pos

Characterization of Convex Sets via Positive Linear Combinations

Informal description

A set $s$ in a vector space over an ordered scalar field $\mathbb{K}$ is convex if and only if for every pair of points $x, y \in s$ and every pair of positive scalars $a, b \in \mathbb{K}$ such that $a + b = 1$, the linear combination $a \cdot x + b \cdot y$ belongs to $s$.

convex_iff_pairwise_pos theorem

 : Convex 𝕜 s ↔ s.Pairwise fun x y => ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s

Full source

theorem convex_iff_pairwise_pos : ConvexConvex 𝕜 s ↔
    s.Pairwise fun x y => ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s := by
  refine convex_iff_forall_pos.trans ⟨fun h x hx y hy _ => h hx hy, ?_⟩
  intro h x hx y hy a b ha hb hab
  obtain rfl | hxy := eq_or_ne x y
  · rwa [Convex.combo_self hab]
  · exact h hx hy hxy ha hb hab

Characterization of Convex Sets via Pairwise Positive Linear Combinations

Informal description

A set $s$ in a vector space over an ordered scalar field $\mathbb{K}$ is convex if and only if for every pair of distinct points $x, y \in s$ and every pair of positive scalars $a, b \in \mathbb{K}$ such that $a + b = 1$, the linear combination $a \cdot x + b \cdot y$ belongs to $s$.

Convex.starConvex_iff theorem

[ZeroLEOneClass 𝕜] (hs : Convex 𝕜 s) (h : s.Nonempty) : StarConvex 𝕜 x s ↔ x ∈ s

Full source

theorem Convex.starConvex_iff [ZeroLEOneClass 𝕜] (hs : Convex 𝕜 s) (h : s.Nonempty) :
    StarConvexStarConvex 𝕜 x s ↔ x ∈ s :=
  ⟨fun hxs => hxs.mem h, hs.starConvex⟩

Characterization of Star-Convexity in Nonempty Convex Sets

Informal description

Let $\mathbb{K}$ be an ordered scalar field where $0 \leq 1$, and let $s$ be a nonempty convex set in a vector space over $\mathbb{K}$. Then for any point $x$, the set $s$ is star-convex with respect to $x$ if and only if $x$ belongs to $s$.

Set.Subsingleton.convex theorem

{s : Set E} (h : s.Subsingleton) : Convex 𝕜 s

Full source

protected theorem Set.Subsingleton.convex {s : Set E} (h : s.Subsingleton) : Convex 𝕜 s :=
  convex_iff_pairwise_pos.mpr (h.pairwise _)

Convexity of Subsingleton Sets

Informal description

For any subsingleton set $s$ in a vector space $E$ over an ordered scalar field $\mathbb{K}$, the set $s$ is convex.

convex_singleton theorem

(c : E) : Convex 𝕜 ({ c } : Set E)

Full source

@[simp] theorem convex_singleton (c : E) : Convex 𝕜 ({c} : Set E) :=
  subsingleton_singleton.convex

Convexity of Singleton Sets in Vector Spaces

Informal description

For any point $c$ in a vector space $E$ over an ordered scalar field $\mathbb{K}$, the singleton set $\{c\}$ is convex.

convex_zero theorem

: Convex 𝕜 (0 : Set E)

Full source

theorem convex_zero : Convex 𝕜 (0 : Set E) :=
  convex_singleton _

Convexity of the Zero Vector in a Vector Space

Informal description

The singleton set $\{0\}$ in a vector space $E$ over an ordered scalar field $\mathbb{K}$ is convex.

convex_segment theorem

[IsOrderedRing 𝕜] (x y : E) : Convex 𝕜 [x -[𝕜] y]

Full source

theorem convex_segment [IsOrderedRing 𝕜] (x y : E) : Convex 𝕜 [x -[𝕜] y] := by
  rintro p ⟨ap, bp, hap, hbp, habp, rfl⟩ q ⟨aq, bq, haq, hbq, habq, rfl⟩ a b ha hb hab
  refine
    ⟨a * ap + b * aq, a * bp + b * bq, add_nonneg (mul_nonneg ha hap) (mul_nonneg hb haq),
      add_nonneg (mul_nonneg ha hbp) (mul_nonneg hb hbq), ?_, ?_⟩
  · rw [add_add_add_comm, ← mul_add, ← mul_add, habp, habq, mul_one, mul_one, hab]
  · match_scalars <;> noncomm_ring

Convexity of the Segment $[x, y]_{\mathbb{K}}$ in a Vector Space over an Ordered Ring

Informal description

Let $\mathbb{K}$ be an ordered ring and $E$ be a $\mathbb{K}$-vector space. For any two points $x, y \in E$, the segment $[x, y]_{\mathbb{K}}$ is convex in $E$.

Convex.linear_image theorem

(hs : Convex 𝕜 s) (f : E →ₗ[𝕜] F) : Convex 𝕜 (f '' s)

Full source

theorem Convex.linear_image (hs : Convex 𝕜 s) (f : E →ₗ[𝕜] F) : Convex 𝕜 (f '' s) := by
  rintro _ ⟨x, hx, rfl⟩ _ ⟨y, hy, rfl⟩ a b ha hb hab
  exact ⟨a • x + b • y, hs hx hy ha hb hab, by rw [f.map_add, f.map_smul, f.map_smul]⟩

Image of a Convex Set under a Linear Map is Convex

Informal description

Let $E$ and $F$ be vector spaces over an ordered scalar field $\mathbb{K}$. If $s \subseteq E$ is a convex set and $f : E \to F$ is a linear map, then the image $f(s) \subseteq F$ is also convex.

Convex.is_linear_image theorem

(hs : Convex 𝕜 s) {f : E → F} (hf : IsLinearMap 𝕜 f) : Convex 𝕜 (f '' s)

Full source

theorem Convex.is_linear_image (hs : Convex 𝕜 s) {f : E → F} (hf : IsLinearMap 𝕜 f) :
    Convex 𝕜 (f '' s) :=
  hs.linear_image <| hf.mk' f

Convexity of Linear Image of a Convex Set

Informal description

Let $E$ and $F$ be vector spaces over an ordered scalar field $\mathbb{K}$. If $s \subseteq E$ is a convex set and $f : E \to F$ is a $\mathbb{K}$-linear map, then the image $f(s) \subseteq F$ is also convex.

Convex.linear_preimage theorem

 {𝕜₁ : Type*} [Semiring 𝕜₁] [Module 𝕜₁ E] [Module 𝕜₁ F] {s : Set F} [SMul 𝕜 𝕜₁] [IsScalarTower 𝕜 𝕜₁ E]
  [IsScalarTower 𝕜 𝕜₁ F] (hs : Convex 𝕜 s) (f : E →ₗ[𝕜₁] F) : Convex 𝕜 (f ⁻¹' s)

Full source

theorem Convex.linear_preimage {𝕜₁ : Type*} [Semiring 𝕜₁] [Module 𝕜₁ E] [Module 𝕜₁ F] {s : Set F}
    [SMul 𝕜 𝕜₁] [IsScalarTower 𝕜 𝕜₁ E] [IsScalarTower 𝕜 𝕜₁ F] (hs : Convex 𝕜 s) (f : E →ₗ[𝕜₁] F) :
    Convex 𝕜 (f ⁻¹' s) := fun x hx y hy a b ha hb hab => by
  rw [mem_preimage, f.map_add, LinearMap.map_smul_of_tower, LinearMap.map_smul_of_tower]
  exact hs hx hy ha hb hab

Preimage of Convex Set under Linear Map is Convex

Informal description

Let $E$ and $F$ be vector spaces over ordered scalar fields $\mathbb{K}$ and $\mathbb{K}_1$ respectively, with $\mathbb{K}$ acting on $\mathbb{K}_1$ via scalar multiplication. Suppose $s \subseteq F$ is a convex set and $f : E \to F$ is a linear map between these vector spaces. Then the preimage $f^{-1}(s) \subseteq E$ is also convex.

Convex.is_linear_preimage theorem

 {𝕜₁ : Type*} [Semiring 𝕜₁] [Module 𝕜₁ E] [Module 𝕜₁ F] {s : Set F} [SMul 𝕜 𝕜₁] [IsScalarTower 𝕜 𝕜₁ E]
  [IsScalarTower 𝕜 𝕜₁ F] (hs : Convex 𝕜 s) {f : E → F} (hf : IsLinearMap 𝕜₁ f) : Convex 𝕜 (f ⁻¹' s)

Full source

theorem Convex.is_linear_preimage {𝕜₁ : Type*} [Semiring 𝕜₁] [Module 𝕜₁ E] [Module 𝕜₁ F] {s : Set F}
  [SMul 𝕜 𝕜₁] [IsScalarTower 𝕜 𝕜₁ E] [IsScalarTower 𝕜 𝕜₁ F] (hs : Convex 𝕜 s) {f : E → F}
  (hf : IsLinearMap 𝕜₁ f) :
    Convex 𝕜 (f ⁻¹' s) :=
  hs.linear_preimage <| hf.mk' f

Preimage of Convex Set under Linear Map is Convex

Informal description

Let $E$ and $F$ be vector spaces over ordered scalar fields $\mathbb{K}$ and $\mathbb{K}_1$ respectively, with $\mathbb{K}$ acting on $\mathbb{K}_1$ via scalar multiplication. If $s \subseteq F$ is a convex set and $f : E \to F$ is a $\mathbb{K}_1$-linear map, then the preimage $f^{-1}(s) \subseteq E$ is also convex.

Convex.add theorem

{t : Set E} (hs : Convex 𝕜 s) (ht : Convex 𝕜 t) : Convex 𝕜 (s + t)

Full source

theorem Convex.add {t : Set E} (hs : Convex 𝕜 s) (ht : Convex 𝕜 t) : Convex 𝕜 (s + t) := by
  rw [← add_image_prod]
  exact (hs.prod ht).is_linear_image IsLinearMap.isLinearMap_add

Convexity of Minkowski Sum of Convex Sets

Informal description

Let $E$ be a vector space over an ordered scalar field $\mathbb{K}$. If $s, t \subseteq E$ are convex sets, then their Minkowski sum $s + t = \{x + y \mid x \in s, y \in t\}$ is also convex.

convexAddSubmonoid definition

: AddSubmonoid (Set E)

Full source

/-- The convex sets form an additive submonoid under pointwise addition. -/
def convexAddSubmonoid : AddSubmonoid (Set E) where
  carrier := {s : Set E | Convex 𝕜 s}
  zero_mem' := convex_zero
  add_mem' := Convex.add

Additive submonoid of convex sets

Informal description

The additive submonoid of all convex subsets of a vector space $E$ over an ordered scalar field $\mathbb{K}$, where the operation is pointwise addition of sets. The carrier of this submonoid consists of all convex subsets of $E$, it contains the zero set $\{0\}$, and is closed under Minkowski addition of convex sets.

coe_convexAddSubmonoid theorem

: ↑(convexAddSubmonoid 𝕜 E) = {s : Set E | Convex 𝕜 s}

Full source

@[simp, norm_cast]
theorem coe_convexAddSubmonoid : ↑(convexAddSubmonoid 𝕜 E) = {s : Set E | Convex 𝕜 s} :=
  rfl

Characterization of Convex Sets in the Additive Submonoid

Informal description

The carrier of the additive submonoid of convex sets in a vector space $E$ over an ordered scalar field $\mathbb{K}$ is precisely the collection of all convex subsets of $E$. In other words, a set $s \subseteq E$ belongs to the submonoid if and only if $s$ is convex.

mem_convexAddSubmonoid theorem

{s : Set E} : s ∈ convexAddSubmonoid 𝕜 E ↔ Convex 𝕜 s

Full source

@[simp]
theorem mem_convexAddSubmonoid {s : Set E} : s ∈ convexAddSubmonoid 𝕜 Es ∈ convexAddSubmonoid 𝕜 E ↔ Convex 𝕜 s :=
  Iff.rfl

Membership in Convex Additive Submonoid Characterizes Convexity

Informal description

A set $s$ in a vector space $E$ over an ordered scalar field $\mathbb{K}$ belongs to the additive submonoid of convex sets if and only if $s$ is convex.

convex_list_sum theorem

{l : List (Set E)} (h : ∀ i ∈ l, Convex 𝕜 i) : Convex 𝕜 l.sum

Full source

theorem convex_list_sum {l : List (Set E)} (h : ∀ i ∈ l, Convex 𝕜 i) : Convex 𝕜 l.sum :=
  (convexAddSubmonoid 𝕜 E).list_sum_mem h

Convexity of Minkowski Sum of Convex Sets in a List

Informal description

For any list $l$ of sets in a vector space $E$ over an ordered scalar field $\mathbb{K}$, if every set in $l$ is convex, then the Minkowski sum of all sets in $l$ is also convex.

convex_multiset_sum theorem

{s : Multiset (Set E)} (h : ∀ i ∈ s, Convex 𝕜 i) : Convex 𝕜 s.sum

Full source

theorem convex_multiset_sum {s : Multiset (Set E)} (h : ∀ i ∈ s, Convex 𝕜 i) : Convex 𝕜 s.sum :=
  (convexAddSubmonoid 𝕜 E).multiset_sum_mem _ h

Convexity of Minkowski Sum of Convex Sets in a Multiset

Informal description

Let $\mathbb{K}$ be an ordered scalar field and $E$ a vector space over $\mathbb{K}$. Given a multiset $s$ of subsets of $E$, if every set in $s$ is convex, then the Minkowski sum of all sets in $s$ is also convex.

convex_sum theorem

{ι} {s : Finset ι} (t : ι → Set E) (h : ∀ i ∈ s, Convex 𝕜 (t i)) : Convex 𝕜 (∑ i ∈ s, t i)

Full source

theorem convex_sum {ι} {s : Finset ι} (t : ι → Set E) (h : ∀ i ∈ s, Convex 𝕜 (t i)) :
    Convex 𝕜 (∑ i ∈ s, t i) :=
  (convexAddSubmonoid 𝕜 E).sum_mem h

Convexity of Minkowski Sum of Convex Sets

Informal description

Let $\mathbb{K}$ be an ordered scalar field, $E$ a vector space over $\mathbb{K}$, $\iota$ an index type, and $s$ a finite subset of $\iota$. Given a family of sets $(t_i)_{i \in \iota}$ in $E$ such that each $t_i$ is convex for all $i \in s$, then the Minkowski sum $\sum_{i \in s} t_i$ is also convex.

Convex.vadd theorem

(hs : Convex 𝕜 s) (z : E) : Convex 𝕜 (z +ᵥ s)

Full source

theorem Convex.vadd (hs : Convex 𝕜 s) (z : E) : Convex 𝕜 (z +ᵥ s) := by
  simp_rw [← image_vadd, vadd_eq_add, ← singleton_add]
  exact (convex_singleton _).add hs

Convexity of Translated Sets in Vector Spaces

Informal description

Let $E$ be a vector space over an ordered scalar field $\mathbb{K}$ and $s \subseteq E$ be a convex set. For any vector $z \in E$, the set obtained by translating $s$ by $z$ (i.e., $z + s = \{z + x \mid x \in s\}$) is convex.

Convex.translate theorem

(hs : Convex 𝕜 s) (z : E) : Convex 𝕜 ((fun x => z + x) '' s)

Full source

theorem Convex.translate (hs : Convex 𝕜 s) (z : E) : Convex 𝕜 ((fun x => z + x) '' s) :=
  hs.vadd _

Convexity of Translated Image in Vector Spaces

Informal description

Let $E$ be a vector space over an ordered scalar field $\mathbb{K}$ and $s \subseteq E$ be a convex set. For any vector $z \in E$, the image of $s$ under the translation map $x \mapsto z + x$ is convex in $E$.

Convex.translate_preimage_right theorem

(hs : Convex 𝕜 s) (z : E) : Convex 𝕜 ((fun x => z + x) ⁻¹' s)

Full source

/-- The translation of a convex set is also convex. -/
theorem Convex.translate_preimage_right (hs : Convex 𝕜 s) (z : E) :
    Convex 𝕜 ((fun x => z + x) ⁻¹' s) := by
  intro x hx y hy a b ha hb hab
  have h := hs hx hy ha hb hab
  rwa [smul_add, smul_add, add_add_add_comm, ← add_smul, hab, one_smul] at h

Convexity of Translated Preimage (Right)

Informal description

Let $E$ be a vector space over an ordered scalar field $\mathbb{K}$ and $s \subseteq E$ be a convex set. For any vector $z \in E$, the preimage of $s$ under the translation map $x \mapsto z + x$ is convex in $E$.

Convex.translate_preimage_left theorem

(hs : Convex 𝕜 s) (z : E) : Convex 𝕜 ((fun x => x + z) ⁻¹' s)

Full source

/-- The translation of a convex set is also convex. -/
theorem Convex.translate_preimage_left (hs : Convex 𝕜 s) (z : E) :
    Convex 𝕜 ((fun x => x + z) ⁻¹' s) := by
  simpa only [add_comm] using hs.translate_preimage_right z

Convexity of Translated Preimage (Left)

Informal description

Let $E$ be a vector space over an ordered scalar field $\mathbb{K}$ and $s \subseteq E$ be a convex set. For any vector $z \in E$, the preimage of $s$ under the translation map $x \mapsto x + z$ is convex in $E$.

convex_Iic theorem

(r : β) : Convex 𝕜 (Iic r)

Full source

theorem convex_Iic (r : β) : Convex 𝕜 (Iic r) := fun x hx y hy a b ha hb hab =>
  calc
    a • x + b • y ≤ a • r + b • r :=
      add_le_add (smul_le_smul_of_nonneg_left hx ha) (smul_le_smul_of_nonneg_left hy hb)
    _ = r := Convex.combo_self hab _

Convexity of Left-Infinite Right-Closed Interval in Ordered Vector Space

Informal description

For any element $r$ in an ordered vector space $\beta$ over an ordered scalar field $\mathbb{K}$, the left-infinite right-closed interval $(-\infty, r]$ is a convex set.

convex_Ici theorem

(r : β) : Convex 𝕜 (Ici r)

Full source

theorem convex_Ici (r : β) : Convex 𝕜 (Ici r) :=
  convex_Iic (β := βᵒᵈ) r

Convexity of Right-Infinite Left-Closed Interval in Ordered Vector Space

Informal description

For any element $r$ in an ordered vector space $\beta$ over an ordered scalar field $\mathbb{K}$, the right-infinite left-closed interval $[r, \infty)$ is a convex set.

convex_Icc theorem

(r s : β) : Convex 𝕜 (Icc r s)

Full source

theorem convex_Icc (r s : β) : Convex 𝕜 (Icc r s) :=
  Ici_inter_Iic.subst ((convex_Ici r).inter <| convex_Iic s)

Convexity of Closed Interval in Ordered Vector Space

Informal description

For any elements $r$ and $s$ in an ordered vector space $\beta$ over an ordered scalar field $\mathbb{K}$, the closed interval $[r, s]$ is a convex set.

convex_halfSpace_le theorem

{f : E → β} (h : IsLinearMap 𝕜 f) (r : β) : Convex 𝕜 {w | f w ≤ r}

Full source

theorem convex_halfSpace_le {f : E → β} (h : IsLinearMap 𝕜 f) (r : β) : Convex 𝕜 { w | f w ≤ r } :=
  (convex_Iic r).is_linear_preimage h

Convexity of Half-Space Defined by Linear Inequality

Informal description

Let $E$ be a vector space over an ordered scalar field $\mathbb{K}$, and let $\beta$ be an ordered vector space over $\mathbb{K}$. For any $\mathbb{K}$-linear map $f : E \to \beta$ and any $r \in \beta$, the half-space $\{w \in E \mid f(w) \leq r\}$ is convex.

convex_halfSpace_ge theorem

{f : E → β} (h : IsLinearMap 𝕜 f) (r : β) : Convex 𝕜 {w | r ≤ f w}

Full source

theorem convex_halfSpace_ge {f : E → β} (h : IsLinearMap 𝕜 f) (r : β) : Convex 𝕜 { w | r ≤ f w } :=
  (convex_Ici r).is_linear_preimage h

Convexity of Upper Half-Space Defined by Linear Inequality

Informal description

Let $E$ be a vector space over an ordered scalar field $\mathbb{K}$, and let $\beta$ be an ordered vector space over $\mathbb{K}$. For any $\mathbb{K}$-linear map $f : E \to \beta$ and any $r \in \beta$, the upper half-space $\{w \in E \mid r \leq f(w)\}$ is convex.

convex_hyperplane theorem

{f : E → β} (h : IsLinearMap 𝕜 f) (r : β) : Convex 𝕜 {w | f w = r}

Full source

theorem convex_hyperplane {f : E → β} (h : IsLinearMap 𝕜 f) (r : β) : Convex 𝕜 { w | f w = r } := by
  simp_rw [le_antisymm_iff]
  exact (convex_halfSpace_le h r).inter (convex_halfSpace_ge h r)

Convexity of Hyperplane Defined by Linear Equation

Informal description

Let $E$ be a vector space over an ordered scalar field $\mathbb{K}$, and let $\beta$ be an ordered vector space over $\mathbb{K}$. For any $\mathbb{K}$-linear map $f : E \to \beta$ and any $r \in \beta$, the hyperplane $\{w \in E \mid f(w) = r\}$ is convex.

convex_Iio theorem

(r : β) : Convex 𝕜 (Iio r)

Full source

theorem convex_Iio (r : β) : Convex 𝕜 (Iio r) := by
  intro x hx y hy a b ha hb hab
  obtain rfl | ha' := ha.eq_or_lt
  · rw [zero_add] at hab
    rwa [zero_smul, zero_add, hab, one_smul]
  rw [mem_Iio] at hx hy
  calc
    a • x + b • y < a • r + b • r := add_lt_add_of_lt_of_le
        (smul_lt_smul_of_pos_left hx ha') (smul_le_smul_of_nonneg_left hy.le hb)
    _ = r := Convex.combo_self hab _

Convexity of Left-Infinite Right-Open Interval $(-\infty, r)$

Informal description

For any ordered vector space $E$ over an ordered scalar field $\mathbb{K}$ and any element $r \in E$, the left-infinite right-open interval $(-\infty, r) = \{x \in E \mid x < r\}$ is convex.

convex_Ioi theorem

(r : β) : Convex 𝕜 (Ioi r)

Full source

theorem convex_Ioi (r : β) : Convex 𝕜 (Ioi r) :=
  convex_Iio (β := βᵒᵈ) r

Convexity of Right-Infinite Left-Open Interval $(r, \infty)$

Informal description

For any ordered vector space $E$ over an ordered scalar field $\mathbb{K}$ and any element $r \in E$, the right-infinite left-open interval $(r, \infty) = \{x \in E \mid x > r\}$ is convex.

convex_Ioo theorem

(r s : β) : Convex 𝕜 (Ioo r s)

Full source

theorem convex_Ioo (r s : β) : Convex 𝕜 (Ioo r s) :=
  Ioi_inter_Iio.subst ((convex_Ioi r).inter <| convex_Iio s)

Convexity of Open Interval $(r, s)$ in Ordered Vector Spaces

Informal description

For any ordered vector space $E$ over an ordered scalar field $\mathbb{K}$ and any two elements $r, s \in E$, the open interval $(r, s) = \{x \in E \mid r < x < s\}$ is convex.

convex_Ico theorem

(r s : β) : Convex 𝕜 (Ico r s)

Full source

theorem convex_Ico (r s : β) : Convex 𝕜 (Ico r s) :=
  Ici_inter_Iio.subst ((convex_Ici r).inter <| convex_Iio s)

Convexity of Left-Closed Right-Open Interval $[r, s)$

Informal description

For any ordered vector space $E$ over an ordered scalar field $\mathbb{K}$ and any elements $r, s \in E$, the left-closed right-open interval $[r, s) = \{x \in E \mid r \leq x < s\}$ is convex.

convex_Ioc theorem

(r s : β) : Convex 𝕜 (Ioc r s)

Full source

theorem convex_Ioc (r s : β) : Convex 𝕜 (Ioc r s) :=
  Ioi_inter_Iic.subst ((convex_Ioi r).inter <| convex_Iic s)

Convexity of Left-Open Right-Closed Interval $(r, s]$

Informal description

For any elements $r$ and $s$ in an ordered vector space $\beta$ over an ordered scalar field $\mathbb{K}$, the left-open right-closed interval $(r, s]$ is convex.

convex_halfSpace_lt theorem

{f : E → β} (h : IsLinearMap 𝕜 f) (r : β) : Convex 𝕜 {w | f w < r}

Full source

theorem convex_halfSpace_lt {f : E → β} (h : IsLinearMap 𝕜 f) (r : β) : Convex 𝕜 { w | f w < r } :=
  (convex_Iio r).is_linear_preimage h

Convexity of Half-Space Defined by Linear Inequality $f(w) < r$

Informal description

Let $E$ be a vector space over an ordered scalar field $\mathbb{K}$, and let $\beta$ be another ordered vector space over $\mathbb{K}$. Given a $\mathbb{K}$-linear map $f \colon E \to \beta$ and an element $r \in \beta$, the half-space $\{w \in E \mid f(w) < r\}$ is convex.

convex_halfSpace_gt theorem

{f : E → β} (h : IsLinearMap 𝕜 f) (r : β) : Convex 𝕜 {w | r < f w}

Full source

theorem convex_halfSpace_gt {f : E → β} (h : IsLinearMap 𝕜 f) (r : β) : Convex 𝕜 { w | r < f w } :=
  (convex_Ioi r).is_linear_preimage h

Convexity of Upper Half-Space Defined by Linear Functional

Informal description

Let $E$ be a vector space over an ordered scalar field $\mathbb{K}$, $\beta$ be an ordered vector space over $\mathbb{K}$, and $f \colon E \to \beta$ be a $\mathbb{K}$-linear map. For any $r \in \beta$, the set $\{w \in E \mid r < f(w)\}$ is convex.

convex_uIcc theorem

(r s : β) : Convex 𝕜 (uIcc r s)

Full source

theorem convex_uIcc (r s : β) : Convex 𝕜 (uIcc r s) :=
  convex_Icc _ _

Convexity of Unordered Closed Interval in Ordered Vector Space

Informal description

For any two elements $r$ and $s$ in an ordered vector space $\beta$ over an ordered scalar field $\mathbb{K}$, the unordered closed interval $\text{uIcc}(r, s) = [r \sqcap s, r \sqcup s]$ is a convex set.

MonotoneOn.convex_le theorem

(hf : MonotoneOn f s) (hs : Convex 𝕜 s) (r : β) : Convex 𝕜 ({x ∈ s | f x ≤ r})

Full source

theorem MonotoneOn.convex_le (hf : MonotoneOn f s) (hs : Convex 𝕜 s) (r : β) :
    Convex 𝕜 ({ x ∈ s | f x ≤ r }) := fun x hx y hy _ _ ha hb hab =>
  ⟨hs hx.1 hy.1 ha hb hab,
    (hf (hs hx.1 hy.1 ha hb hab) (max_rec' s hx.1 hy.1) (Convex.combo_le_max x y ha hb hab)).trans
      (max_rec' { x | f x ≤ r } hx.2 hy.2)⟩

Convexity of Sublevel Sets under Monotone Functions

Informal description

Let $E$ be a vector space over an ordered scalar field $\mathbb{K}$, $s \subseteq E$ a convex set, and $f \colon E \to \beta$ a function that is monotone on $s$. Then for any $r \in \beta$, the sublevel set $\{x \in s \mid f(x) \leq r\}$ is convex.

MonotoneOn.convex_lt theorem

(hf : MonotoneOn f s) (hs : Convex 𝕜 s) (r : β) : Convex 𝕜 ({x ∈ s | f x < r})

Full source

theorem MonotoneOn.convex_lt (hf : MonotoneOn f s) (hs : Convex 𝕜 s) (r : β) :
    Convex 𝕜 ({ x ∈ s | f x < r }) := fun x hx y hy _ _ ha hb hab =>
  ⟨hs hx.1 hy.1 ha hb hab,
    (hf (hs hx.1 hy.1 ha hb hab) (max_rec' s hx.1 hy.1)
          (Convex.combo_le_max x y ha hb hab)).trans_lt
      (max_rec' { x | f x < r } hx.2 hy.2)⟩

Convexity of Strict Sublevel Sets of Monotone Functions on Convex Sets

Informal description

Let $E$ be a vector space over an ordered scalar field $\mathbb{K}$, $s$ a convex subset of $E$, and $f : E \to \beta$ a function that is monotone on $s$. Then for any $r \in \beta$, the sublevel set $\{x \in s \mid f(x) < r\}$ is convex.

MonotoneOn.convex_ge theorem

(hf : MonotoneOn f s) (hs : Convex 𝕜 s) (r : β) : Convex 𝕜 ({x ∈ s | r ≤ f x})

Full source

theorem MonotoneOn.convex_ge (hf : MonotoneOn f s) (hs : Convex 𝕜 s) (r : β) :
    Convex 𝕜 ({ x ∈ s | r ≤ f x }) :=
  MonotoneOn.convex_le (E := Eᵒᵈ) (β := βᵒᵈ) hf.dual hs r

Convexity of Superlevel Sets under Monotone Functions

Informal description

Let $E$ be a vector space over an ordered scalar field $\mathbb{K}$, $s \subseteq E$ a convex set, and $f \colon E \to \beta$ a function that is monotone on $s$. Then for any $r \in \beta$, the superlevel set $\{x \in s \mid r \leq f(x)\}$ is convex.

MonotoneOn.convex_gt theorem

(hf : MonotoneOn f s) (hs : Convex 𝕜 s) (r : β) : Convex 𝕜 ({x ∈ s | r < f x})

Full source

theorem MonotoneOn.convex_gt (hf : MonotoneOn f s) (hs : Convex 𝕜 s) (r : β) :
    Convex 𝕜 ({ x ∈ s | r < f x }) :=
  MonotoneOn.convex_lt (E := Eᵒᵈ) (β := βᵒᵈ) hf.dual hs r

Convexity of Strict Superlevel Sets of Monotone Functions on Convex Sets

Informal description

Let $E$ be a vector space over an ordered scalar field $\mathbb{K}$, $s$ a convex subset of $E$, and $f : E \to \beta$ a function that is monotone on $s$. Then for any $r \in \beta$, the superlevel set $\{x \in s \mid r < f(x)\}$ is convex.

AntitoneOn.convex_le theorem

(hf : AntitoneOn f s) (hs : Convex 𝕜 s) (r : β) : Convex 𝕜 ({x ∈ s | f x ≤ r})

Full source

theorem AntitoneOn.convex_le (hf : AntitoneOn f s) (hs : Convex 𝕜 s) (r : β) :
    Convex 𝕜 ({ x ∈ s | f x ≤ r }) :=
  MonotoneOn.convex_ge (β := βᵒᵈ) hf hs r

Convexity of Sublevel Sets under Antitone Functions

Informal description

Let $E$ be a vector space over an ordered scalar field $\mathbb{K}$, $s \subseteq E$ a convex set, and $f \colon E \to \beta$ a function that is antitone on $s$. Then for any $r \in \beta$, the sublevel set $\{x \in s \mid f(x) \leq r\}$ is convex.

AntitoneOn.convex_lt theorem

(hf : AntitoneOn f s) (hs : Convex 𝕜 s) (r : β) : Convex 𝕜 ({x ∈ s | f x < r})

Full source

theorem AntitoneOn.convex_lt (hf : AntitoneOn f s) (hs : Convex 𝕜 s) (r : β) :
    Convex 𝕜 ({ x ∈ s | f x < r }) :=
  MonotoneOn.convex_gt (β := βᵒᵈ) hf hs r

Convexity of Strict Sublevel Sets under Antitone Functions

Informal description

Let $E$ be a vector space over an ordered scalar field $\mathbb{K}$, $s \subseteq E$ a convex set, and $f \colon E \to \beta$ a function that is antitone on $s$. Then for any $r \in \beta$, the sublevel set $\{x \in s \mid f(x) < r\}$ is convex.

AntitoneOn.convex_ge theorem

(hf : AntitoneOn f s) (hs : Convex 𝕜 s) (r : β) : Convex 𝕜 ({x ∈ s | r ≤ f x})

Full source

theorem AntitoneOn.convex_ge (hf : AntitoneOn f s) (hs : Convex 𝕜 s) (r : β) :
    Convex 𝕜 ({ x ∈ s | r ≤ f x }) :=
  MonotoneOn.convex_le (β := βᵒᵈ) hf hs r

Convexity of Superlevel Sets under Antitone Functions

Informal description

Let $E$ be a vector space over an ordered scalar field $\mathbb{K}$, $s \subseteq E$ a convex set, and $f \colon E \to \beta$ a function that is antitone on $s$. Then for any $r \in \beta$, the superlevel set $\{x \in s \mid r \leq f(x)\}$ is convex.

AntitoneOn.convex_gt theorem

(hf : AntitoneOn f s) (hs : Convex 𝕜 s) (r : β) : Convex 𝕜 ({x ∈ s | r < f x})

Full source

theorem AntitoneOn.convex_gt (hf : AntitoneOn f s) (hs : Convex 𝕜 s) (r : β) :
    Convex 𝕜 ({ x ∈ s | r < f x }) :=
  MonotoneOn.convex_lt (β := βᵒᵈ)  hf hs r

Convexity of Strict Superlevel Sets of Antitone Functions on Convex Sets

Informal description

Let $E$ be a vector space over an ordered scalar field $\mathbb{K}$, $s$ a convex subset of $E$, and $f : E \to \beta$ a function that is antitone on $s$. Then for any $r \in \beta$, the superlevel set $\{x \in s \mid r < f(x)\}$ is convex.

Monotone.convex_le theorem

(hf : Monotone f) (r : β) : Convex 𝕜 {x | f x ≤ r}

Full source

theorem Monotone.convex_le (hf : Monotone f) (r : β) : Convex 𝕜 { x | f x ≤ r } :=
  Set.sep_univ.subst ((hf.monotoneOn univ).convex_le convex_univ r)

Convexity of Sublevel Sets of Monotone Functions

Informal description

Let $E$ be a vector space over an ordered scalar field $\mathbb{K}$ and $f \colon E \to \beta$ be a monotone function. Then for any $r \in \beta$, the sublevel set $\{x \in E \mid f(x) \leq r\}$ is convex.

Monotone.convex_lt theorem

(hf : Monotone f) (r : β) : Convex 𝕜 {x | f x ≤ r}

Full source

theorem Monotone.convex_lt (hf : Monotone f) (r : β) : Convex 𝕜 { x | f x ≤ r } :=
  Set.sep_univ.subst ((hf.monotoneOn univ).convex_le convex_univ r)

Convexity of Sublevel Sets under Monotone Functions

Informal description

Let $E$ be a vector space over an ordered scalar field $\mathbb{K}$ and $f : E \to \beta$ be a monotone function. Then for any $r \in \beta$, the sublevel set $\{x \mid f(x) \leq r\}$ is convex in $E$.

Monotone.convex_ge theorem

(hf : Monotone f) (r : β) : Convex 𝕜 {x | r ≤ f x}

Full source

theorem Monotone.convex_ge (hf : Monotone f) (r : β) : Convex 𝕜 { x | r ≤ f x } :=
  Set.sep_univ.subst ((hf.monotoneOn univ).convex_ge convex_univ r)

Convexity of Superlevel Sets for Monotone Functions

Informal description

Let $E$ be a vector space over an ordered scalar field $\mathbb{K}$ and $f \colon E \to \beta$ be a monotone function. Then for any $r \in \beta$, the superlevel set $\{x \in E \mid r \leq f(x)\}$ is convex.

Monotone.convex_gt theorem

(hf : Monotone f) (r : β) : Convex 𝕜 {x | f x ≤ r}

Full source

theorem Monotone.convex_gt (hf : Monotone f) (r : β) : Convex 𝕜 { x | f x ≤ r } :=
  Set.sep_univ.subst ((hf.monotoneOn univ).convex_le convex_univ r)

Convexity of Sublevel Sets for Monotone Functions

Informal description

Let $E$ be a vector space over an ordered scalar field $\mathbb{K}$ and $f \colon E \to \beta$ be a monotone function. Then for any $r \in \beta$, the sublevel set $\{x \in E \mid f(x) \leq r\}$ is convex.

Antitone.convex_le theorem

(hf : Antitone f) (r : β) : Convex 𝕜 {x | f x ≤ r}

Full source

theorem Antitone.convex_le (hf : Antitone f) (r : β) : Convex 𝕜 { x | f x ≤ r } :=
  Set.sep_univ.subst ((hf.antitoneOn univ).convex_le convex_univ r)

Convexity of Sublevel Sets for Antitone Functions

Informal description

Let $E$ be a vector space over an ordered scalar field $\mathbb{K}$ and $f \colon E \to \beta$ be an antitone function. Then for any $r \in \beta$, the sublevel set $\{x \in E \mid f(x) \leq r\}$ is convex.

Antitone.convex_lt theorem

(hf : Antitone f) (r : β) : Convex 𝕜 {x | f x < r}

Full source

theorem Antitone.convex_lt (hf : Antitone f) (r : β) : Convex 𝕜 { x | f x < r } :=
  Set.sep_univ.subst ((hf.antitoneOn univ).convex_lt convex_univ r)

Convexity of Strict Sublevel Sets for Antitone Functions

Informal description

Let $E$ be a vector space over an ordered scalar field $\mathbb{K}$, and let $f \colon E \to \beta$ be an antitone function. Then for any $r \in \beta$, the strict sublevel set $\{x \in E \mid f(x) < r\}$ is convex in $E$.

Antitone.convex_ge theorem

(hf : Antitone f) (r : β) : Convex 𝕜 {x | r ≤ f x}

Full source

theorem Antitone.convex_ge (hf : Antitone f) (r : β) : Convex 𝕜 { x | r ≤ f x } :=
  Set.sep_univ.subst ((hf.antitoneOn univ).convex_ge convex_univ r)

Convexity of Superlevel Sets under Antitone Functions

Informal description

Let $E$ be a vector space over an ordered scalar field $\mathbb{K}$ and $f \colon E \to \beta$ be an antitone function. Then for any $r \in \beta$, the superlevel set $\{x \in E \mid r \leq f(x)\}$ is convex.

Antitone.convex_gt theorem

(hf : Antitone f) (r : β) : Convex 𝕜 {x | r < f x}

Full source

theorem Antitone.convex_gt (hf : Antitone f) (r : β) : Convex 𝕜 { x | r < f x } :=
  Set.sep_univ.subst ((hf.antitoneOn univ).convex_gt convex_univ r)

Convexity of Strict Superlevel Sets of Antitone Functions

Informal description

Let $E$ be a vector space over an ordered scalar field $\mathbb{K}$ and let $f : E \to \beta$ be an antitone function. For any $r \in \beta$, the superlevel set $\{x \in E \mid r < f(x)\}$ is convex.

Convex.smul theorem

(hs : Convex 𝕜 s) (c : 𝕜) : Convex 𝕜 (c • s)

Full source

theorem Convex.smul (hs : Convex 𝕜 s) (c : 𝕜) : Convex 𝕜 (c • s) :=
  hs.linear_image (LinearMap.lsmul _ _ c)

Convexity is preserved under scalar multiplication

Informal description

Let $E$ be a vector space over an ordered scalar field $\mathbb{K}$ and let $s \subseteq E$ be a convex set. For any scalar $c \in \mathbb{K}$, the scaled set $c \cdot s = \{c \cdot x \mid x \in s\}$ is convex.

Convex.smul_preimage theorem

(hs : Convex 𝕜 s) (c : 𝕜) : Convex 𝕜 ((fun z => c • z) ⁻¹' s)

Full source

theorem Convex.smul_preimage (hs : Convex 𝕜 s) (c : 𝕜) : Convex 𝕜 ((fun z => c • z) ⁻¹' s) :=
  hs.linear_preimage (LinearMap.lsmul _ _ c)

Convexity of Scaling Preimage

Informal description

Let $E$ be a vector space over an ordered scalar field $\mathbb{K}$ and let $s \subseteq E$ be a convex set. For any scalar $c \in \mathbb{K}$, the preimage of $s$ under the scaling operation $z \mapsto c \cdot z$ is convex. In other words, the set $\{x \in E \mid c \cdot x \in s\}$ is convex.

Convex.affinity theorem

(hs : Convex 𝕜 s) (z : E) (c : 𝕜) : Convex 𝕜 ((fun x => z + c • x) '' s)

Full source

theorem Convex.affinity (hs : Convex 𝕜 s) (z : E) (c : 𝕜) :
    Convex 𝕜 ((fun x => z + c • x) '' s) := by
  simpa only [← image_smul, ← image_vadd, image_image] using (hs.smul c).vadd z

Convexity is preserved under affine transformations

Informal description

Let $E$ be a vector space over an ordered scalar field $\mathbb{K}$ and let $s \subseteq E$ be a convex set. For any vector $z \in E$ and scalar $c \in \mathbb{K}$, the image of $s$ under the affine transformation $x \mapsto z + c \cdot x$ is convex. In other words, the set $\{z + c \cdot x \mid x \in s\}$ is convex.

convex_openSegment theorem

(a b : E) : Convex 𝕜 (openSegment 𝕜 a b)

Full source

theorem convex_openSegment (a b : E) : Convex 𝕜 (openSegment 𝕜 a b) := by
  rw [convex_iff_openSegment_subset]
  rintro p ⟨ap, bp, hap, hbp, habp, rfl⟩ q ⟨aq, bq, haq, hbq, habq, rfl⟩ z ⟨a, b, ha, hb, hab, rfl⟩
  refine ⟨a * ap + b * aq, a * bp + b * bq, by positivity, by positivity, ?_, ?_⟩
  · linear_combination (norm := noncomm_ring) a * habp + b * habq + hab
  · module

Convexity of Open Segment in Vector Space

Informal description

For any two points $a$ and $b$ in a vector space $E$ over an ordered scalar field $\mathbb{K}$, the open segment connecting $a$ and $b$ is a convex set. That is, the set $\{\lambda a + (1-\lambda)b \mid \lambda \in \mathbb{K}, 0 < \lambda < 1\}$ is convex.

convex_vadd theorem

(a : E) : Convex 𝕜 (a +ᵥ s) ↔ Convex 𝕜 s

Full source

@[simp]
theorem convex_vadd (a : E) : ConvexConvex 𝕜 (a +ᵥ s) ↔ Convex 𝕜 s :=
  ⟨fun h ↦ by simpa using h.vadd (-a), fun h ↦ h.vadd _⟩

Convexity is Preserved under Translation: $a + s$ is convex $\iff$ $s$ is convex

Informal description

For any vector $a$ in a vector space $E$ over an ordered scalar field $\mathbb{K}$, the translated set $a + s$ is convex if and only if the original set $s$ is convex.

AffineSubspace.convex theorem

(Q : AffineSubspace 𝕜 E) : Convex 𝕜 (Q : Set E)

Full source

/-- Affine subspaces are convex. -/
theorem AffineSubspace.convex (Q : AffineSubspace 𝕜 E) : Convex 𝕜 (Q : Set E) :=
  fun x hx y hy a b _ _ hab ↦ by simpa [Convex.combo_eq_smul_sub_add hab] using Q.2 _ hy hx hx

Convexity of Affine Subspaces

Informal description

For any affine subspace $Q$ of a vector space $E$ over an ordered scalar field $\mathbb{K}$, the underlying set of $Q$ is convex.

Convex.affine_preimage theorem

(f : E →ᵃ[𝕜] F) {s : Set F} (hs : Convex 𝕜 s) : Convex 𝕜 (f ⁻¹' s)

Full source

/-- The preimage of a convex set under an affine map is convex. -/
theorem Convex.affine_preimage (f : E →ᵃ[𝕜] F) {s : Set F} (hs : Convex 𝕜 s) : Convex 𝕜 (f ⁻¹' s) :=
  fun _ hx => (hs hx).affine_preimage _

Preimage of a Convex Set under an Affine Map is Convex

Informal description

Let $E$ and $F$ be vector spaces over an ordered scalar field $\mathbb{K}$, and let $s \subseteq F$ be a convex set. For any affine map $f : E \to F$, the preimage $f^{-1}(s)$ is convex in $E$.

Convex.affine_image theorem

(f : E →ᵃ[𝕜] F) (hs : Convex 𝕜 s) : Convex 𝕜 (f '' s)

Full source

/-- The image of a convex set under an affine map is convex. -/
theorem Convex.affine_image (f : E →ᵃ[𝕜] F) (hs : Convex 𝕜 s) : Convex 𝕜 (f '' s) := by
  rintro _ ⟨x, hx, rfl⟩
  exact (hs hx).affine_image _

Convexity is preserved under affine images

Informal description

Let $E$ and $F$ be vector spaces over an ordered scalar field $\mathbb{K}$, and let $s \subseteq E$ be a convex set. For any affine map $f : E \to F$, the image $f(s)$ is convex in $F$.

Convex.neg theorem

(hs : Convex 𝕜 s) : Convex 𝕜 (-s)

Full source

theorem Convex.neg (hs : Convex 𝕜 s) : Convex 𝕜 (-s) :=
  hs.is_linear_preimage IsLinearMap.isLinearMap_neg (𝕜₁ := 𝕜)

Negation preserves convexity

Informal description

If a set $s$ in a vector space $E$ over an ordered scalar field $\mathbb{K}$ is convex, then its negation $-s = \{-x \mid x \in s\}$ is also convex.

Convex.sub theorem

(hs : Convex 𝕜 s) (ht : Convex 𝕜 t) : Convex 𝕜 (s - t)

Full source

theorem Convex.sub (hs : Convex 𝕜 s) (ht : Convex 𝕜 t) : Convex 𝕜 (s - t) := by
  rw [sub_eq_add_neg]
  exact hs.add ht.neg

Convexity of Minkowski Difference of Convex Sets

Informal description

Let $E$ be a vector space over an ordered scalar field $\mathbb{K}$. If $s, t \subseteq E$ are convex sets, then their Minkowski difference $s - t = \{x - y \mid x \in s, y \in t\}$ is also convex.

Convex.add_smul_mem theorem

 (hs : Convex 𝕜 s) {x y : E} (hx : x ∈ s) (hy : x + y ∈ s) {t : 𝕜} (ht : t ∈ Icc (0 : 𝕜) 1) : x + t • y ∈ s

Full source

theorem Convex.add_smul_mem (hs : Convex 𝕜 s) {x y : E} (hx : x ∈ s) (hy : x + y ∈ s) {t : 𝕜}
    (ht : t ∈ Icc (0 : 𝕜) 1) : x + t • y ∈ s := by
  have h : x + t • y = (1 - t) • x + t • (x + y) := by match_scalars <;> noncomm_ring
  rw [h]
  exact hs hx hy (sub_nonneg_of_le ht.2) ht.1 (sub_add_cancel _ _)

Convexity under linear combination: $x + t y \in s$ for $t \in [0,1]$

Informal description

Let $E$ be a vector space over an ordered scalar field $\mathbb{K}$ and $s$ be a convex subset of $E$. For any points $x \in s$ and $y \in E$ such that $x + y \in s$, and for any scalar $t \in [0,1]$, the point $x + t y$ belongs to $s$.

Convex.smul_mem_of_zero_mem theorem

 (hs : Convex 𝕜 s) {x : E} (zero_mem : (0 : E) ∈ s) (hx : x ∈ s) {t : 𝕜} (ht : t ∈ Icc (0 : 𝕜) 1) : t • x ∈ s

Full source

theorem Convex.smul_mem_of_zero_mem (hs : Convex 𝕜 s) {x : E} (zero_mem : (0 : E) ∈ s) (hx : x ∈ s)
    {t : 𝕜} (ht : t ∈ Icc (0 : 𝕜) 1) : t • x ∈ s := by
  simpa using hs.add_smul_mem zero_mem (by simpa using hx) ht

Convexity under scaling: $t \cdot x \in s$ for $t \in [0,1]$ when $0 \in s$

Informal description

Let $E$ be a vector space over an ordered scalar field $\mathbb{K}$ and $s$ be a convex subset of $E$ containing the zero vector. For any point $x \in s$ and scalar $t \in [0,1]$, the scaled vector $t \cdot x$ belongs to $s$.

Convex.mapsTo_lineMap theorem

(h : Convex 𝕜 s) {x y : E} (hx : x ∈ s) (hy : y ∈ s) : MapsTo (AffineMap.lineMap x y) (Icc (0 : 𝕜) 1) s

Full source

theorem Convex.mapsTo_lineMap (h : Convex 𝕜 s) {x y : E} (hx : x ∈ s) (hy : y ∈ s) :
    MapsTo (AffineMap.lineMap x y) (Icc (0 : 𝕜) 1) s := by
  simpa only [mapsTo', segment_eq_image_lineMap] using h.segment_subset hx hy

Convexity implies line segment maps into set

Informal description

Let $E$ be a vector space over an ordered scalar field $\mathbb{K}$ and $s$ be a convex subset of $E$. For any two points $x, y \in s$, the affine map $\text{lineMap}(x, y)$ maps the closed interval $[0,1] \subseteq \mathbb{K}$ into $s$. That is, for every $t \in [0,1]$, the point $\text{lineMap}(x, y)(t) = x + t(y - x)$ belongs to $s$.

Convex.lineMap_mem theorem

 (h : Convex 𝕜 s) {x y : E} (hx : x ∈ s) (hy : y ∈ s) {t : 𝕜} (ht : t ∈ Icc 0 1) : AffineMap.lineMap x y t ∈ s

Full source

theorem Convex.lineMap_mem (h : Convex 𝕜 s) {x y : E} (hx : x ∈ s) (hy : y ∈ s) {t : 𝕜}
    (ht : t ∈ Icc 0 1) : AffineMap.lineMapAffineMap.lineMap x y t ∈ s :=
  h.mapsTo_lineMap hx hy ht

Convexity implies line segment containment: $(1-t)x + t y \in s$ for $t \in [0,1]$

Informal description

Let $E$ be a vector space over an ordered scalar field $\mathbb{K}$ and $s \subseteq E$ be a convex set. For any two points $x, y \in s$ and any parameter $t \in [0,1]$, the point $(1-t)x + t y$ lies in $s$.

Convex.add_smul_sub_mem theorem

 (h : Convex 𝕜 s) {x y : E} (hx : x ∈ s) (hy : y ∈ s) {t : 𝕜} (ht : t ∈ Icc (0 : 𝕜) 1) : x + t • (y - x) ∈ s

Full source

theorem Convex.add_smul_sub_mem (h : Convex 𝕜 s) {x y : E} (hx : x ∈ s) (hy : y ∈ s) {t : 𝕜}
    (ht : t ∈ Icc (0 : 𝕜) 1) : x + t • (y - x) ∈ s := by
  rw [add_comm]
  exact h.lineMap_mem hx hy ht

Convex combination of two points remains in the set

Informal description

Let $E$ be a vector space over an ordered scalar field $\mathbb{K}$ and $s \subseteq E$ be a convex set. For any two points $x, y \in s$ and any parameter $t \in [0,1]$, the point $x + t(y - x)$ lies in $s$.

Convex_subadditive_le theorem

 [SMul 𝕜 E] {f : E → 𝕜} (hf1 : ∀ x y, f (x + y) ≤ (f x) + (f y)) (hf2 : ∀ ⦃c⦄ x, 0 ≤ c → f (c • x) ≤ c * f x) (B : 𝕜) :
  Convex 𝕜 {x | f x ≤ B}

Full source

theorem Convex_subadditive_le [SMul 𝕜 E] {f : E → 𝕜} (hf1 : ∀ x y, f (x + y) ≤ (f x) + (f y))
    (hf2 : ∀ ⦃c⦄ x, 0 ≤ c → f (c • x) ≤ c * f x) (B : 𝕜) :
    Convex 𝕜 { x | f x ≤ B } := by
  rw [convex_iff_segment_subset]
  rintro x hx y hy z ⟨a, b, ha, hb, hs, rfl⟩
  calc
    _ ≤ a • (f x) + b • (f y) := le_trans (hf1 _ _) (add_le_add (hf2 x ha) (hf2 y hb))
    _ ≤ a • B + b • B := by gcongr <;> assumption
    _ ≤ B := by rw [← add_smul, hs, one_smul]

Convexity of Sublevel Sets of Subadditive, Nonnegatively Homogeneous Functions

Informal description

Let $E$ be a vector space over an ordered scalar field $\mathbb{K}$ and let $f : E \to \mathbb{K}$ be a function satisfying: 1. Subadditivity: $f(x + y) \leq f(x) + f(y)$ for all $x, y \in E$ 2. Nonnegative homogeneity: $f(c \cdot x) \leq c \cdot f(x)$ for all $x \in E$ and $c \in \mathbb{K}$ with $0 \leq c$ Then for any $B \in \mathbb{K}$, the sublevel set $\{x \in E \mid f(x) \leq B\}$ is convex in $E$.

Convex.midpoint_mem theorem

 [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

Full source

theorem Convex.midpoint_mem [Ring 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
    [AddCommGroup E] [Module 𝕜 E] [Invertible (2 : 𝕜)] {s : Set E} {x y : E}
    (h : Convex 𝕜 s) (hx : x ∈ s) (hy : y ∈ s) : midpointmidpoint 𝕜 x y ∈ s :=
  h.segment_subset hx hy <| midpoint_mem_segment x y

Midpoint of Two Points in a Convex Set Belongs to the Set

Informal description

Let $\mathbb{K}$ be a linearly ordered ring with a strict order and let $E$ be a $\mathbb{K}$-module where $2$ is invertible in $\mathbb{K}$. For any convex set $s \subseteq E$ and any two points $x, y \in s$, the midpoint of $x$ and $y$ lies in $s$.

convex_iff_div theorem

 :
  Convex 𝕜 s ↔
    ∀ ⦃x⦄, x ∈ s → ∀ ⦃y⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → 0 < a + b → (a / (a + b)) • x + (b / (a + b)) • y ∈ s

Full source

/-- Alternative definition of set convexity, using division. -/
theorem convex_iff_div :
    ConvexConvex 𝕜 s ↔ ∀ ⦃x⦄, x ∈ s → ∀ ⦃y⦄, y ∈ s →
      ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → 0 < a + b → (a / (a + b)) • x + (b / (a + b)) • y ∈ s :=
  forall₂_congr fun _ _ => starConvex_iff_div

Characterization of Convex Sets via Division

Informal description

A set $s$ in a vector space over an ordered scalar field $\mathbb{K}$ is convex if and only if for any two points $x, y \in s$ and any non-negative scalars $a, b \in \mathbb{K}$ with $a + b > 0$, the point $\left(\frac{a}{a+b}\right) \cdot x + \left(\frac{b}{a+b}\right) \cdot y$ belongs to $s$.

Convex.mem_smul_of_zero_mem theorem

(h : Convex 𝕜 s) {x : E} (zero_mem : (0 : E) ∈ s) (hx : x ∈ s) {t : 𝕜} (ht : 1 ≤ t) : x ∈ t • s

Full source

theorem Convex.mem_smul_of_zero_mem (h : Convex 𝕜 s) {x : E} (zero_mem : (0 : E) ∈ s) (hx : x ∈ s)
    {t : 𝕜} (ht : 1 ≤ t) : x ∈ t • s := by
  rw [mem_smul_set_iff_inv_smul_mem₀ (zero_lt_one.trans_le ht).ne']
  exact h.smul_mem_of_zero_mem zero_mem hx
    ⟨inv_nonneg.2 (zero_le_one.trans ht), inv_le_one_of_one_le₀ ht⟩

Inclusion of Point in Scaled Convex Set for $t \geq 1$ When Zero is in the Set

Informal description

Let $E$ be a vector space over an ordered scalar field $\mathbb{K}$ and $s$ be a convex subset of $E$ containing the zero vector. For any point $x \in s$ and scalar $t \geq 1$, the vector $x$ belongs to the scaled set $t \cdot s$.

Convex.exists_mem_add_smul_eq theorem

 (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

Full source

theorem Convex.exists_mem_add_smul_eq (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 := by
  rcases _root_.em (p = 0 ∧ q = 0) with (⟨rfl, rfl⟩ | hpq)
  · use x, hx
    simp
  · replace hpq : 0 < p + q :=
      (add_nonneg hp hq).lt_of_ne' (mt (add_eq_zero_iff_of_nonneg hp hq).1 hpq)
    refine ⟨_, convex_iff_div.1 h hx hy hp hq hpq, ?_⟩
    match_scalars <;> field_simp

Existence of Convex Combination in Convex Sets

Informal description

Let $s$ be a convex set in a vector space $E$ over an ordered scalar field $\mathbb{K}$. For any two points $x, y \in s$ and non-negative scalars $p, q \in \mathbb{K}$, there exists a point $z \in s$ such that $(p + q) \cdot z = p \cdot x + q \cdot y$.

Convex.add_smul theorem

(h_conv : Convex 𝕜 s) {p q : 𝕜} (hp : 0 ≤ p) (hq : 0 ≤ q) : (p + q) • s = p • s + q • s

Full source

theorem Convex.add_smul (h_conv : Convex 𝕜 s) {p q : 𝕜} (hp : 0 ≤ p) (hq : 0 ≤ q) :
    (p + q) • s = p • s + q • s := (add_smul_subset _ _ _).antisymm <| by
  rintro _ ⟨_, ⟨v₁, h₁, rfl⟩, _, ⟨v₂, h₂, rfl⟩, rfl⟩
  exact h_conv.exists_mem_add_smul_eq h₁ h₂ hp hq

Minkowski Sum of Scaled Convex Sets: $(p + q) \cdot s = p \cdot s + q \cdot s$

Informal description

Let $s$ be a convex set in a vector space $E$ over an ordered scalar field $\mathbb{K}$. For any non-negative scalars $p, q \in \mathbb{K}$, the Minkowski sum of the scaled sets satisfies $(p + q) \cdot s = p \cdot s + q \cdot s$.

Set.OrdConnected.convex_of_chain theorem

 [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [PartialOrder E] [IsOrderedAddMonoid E] [Module 𝕜 E] [OrderedSMul 𝕜 E]
  {s : Set E} (hs : s.OrdConnected) (h : IsChain (· ≤ ·) s) : Convex 𝕜 s

Full source

theorem Set.OrdConnected.convex_of_chain [Semiring 𝕜] [PartialOrder 𝕜]
    [AddCommMonoid E] [PartialOrder E] [IsOrderedAddMonoid E] [Module 𝕜 E]
    [OrderedSMul 𝕜 E] {s : Set E} (hs : s.OrdConnected) (h : IsChain (· ≤ ·) s) : Convex 𝕜 s := by
  refine convex_iff_segment_subset.mpr fun x hx y hy => ?_
  obtain hxy | hyx := h.total hx hy
  · exact (segment_subset_Icc hxy).trans (hs.out hx hy)
  · rw [segment_symm]
    exact (segment_subset_Icc hyx).trans (hs.out hy hx)

Convexity of Order-Connected Chains in Ordered Modules

Informal description

Let $\mathbb{K}$ be a partially ordered semiring, and let $E$ be a partially ordered additive commutative monoid with a module structure over $\mathbb{K}$ and an ordered scalar multiplication. For any subset $s \subseteq E$, if $s$ is order-connected and forms a chain with respect to the partial order $\leq$ on $E$, then $s$ is convex in $E$.

Set.OrdConnected.convex theorem

 [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [LinearOrder E] [IsOrderedAddMonoid E] [Module 𝕜 E] [OrderedSMul 𝕜 E]
  {s : Set E} (hs : s.OrdConnected) : Convex 𝕜 s

Full source

theorem Set.OrdConnected.convex [Semiring 𝕜] [PartialOrder 𝕜]
    [AddCommMonoid E] [LinearOrder E] [IsOrderedAddMonoid E] [Module 𝕜 E]
    [OrderedSMul 𝕜 E] {s : Set E} (hs : s.OrdConnected) : Convex 𝕜 s :=
  hs.convex_of_chain <| isChain_of_trichotomous s

Convexity of Order-Connected Sets in Linearly Ordered Modules

Informal description

Let $\mathbb{K}$ be a partially ordered semiring, and let $E$ be a linearly ordered additive commutative monoid with a module structure over $\mathbb{K}$ and an ordered scalar multiplication. For any subset $s \subseteq E$, if $s$ is order-connected (i.e., for any $x, y \in s$, the closed interval $[x, y]$ is contained in $s$), then $s$ is convex in $E$.

convex_iff_ordConnected theorem

[Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {s : Set 𝕜} : Convex 𝕜 s ↔ s.OrdConnected

Full source

theorem convex_iff_ordConnected [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {s : Set 𝕜} :
    ConvexConvex 𝕜 s ↔ s.OrdConnected := by
  simp_rw [convex_iff_segment_subset, segment_eq_uIcc, ordConnected_iff_uIcc_subset]

Convexity Equivalence for Order-Connected Sets in Ordered Fields

Informal description

For any field $\mathbb{K}$ with a linear order and a strict ordered ring structure, and for any subset $s \subseteq \mathbb{K}$, the set $s$ is convex if and only if it is order connected (i.e., for any two points $x, y \in s$, the closed interval $[x, y]$ is entirely contained in $s$).

Submodule.convex theorem

(K : Submodule 𝕜 E) : Convex 𝕜 (↑K : Set E)

Full source

protected theorem convex (K : Submodule 𝕜 E) : Convex 𝕜 (↑K : Set E) := by
  repeat' intro
  refine add_mem (smul_mem _ _ ?_) (smul_mem _ _ ?_) <;> assumption

Convexity of Submodules

Informal description

For any submodule $K$ of a vector space $E$ over an ordered scalar field $\mathbb{K}$, the underlying set of $K$ is convex.

Submodule.starConvex theorem

(K : Submodule 𝕜 E) : StarConvex 𝕜 (0 : E) K

Full source

protected theorem starConvex (K : Submodule 𝕜 E) : StarConvex 𝕜 (0 : E) K :=
  K.convex K.zero_mem

Star-Convexity of Submodules with Respect to Origin

Informal description

For any submodule $K$ of a vector space $E$ over an ordered scalar field $\mathbb{K}$, the set $K$ is star-convex with respect to the origin (i.e., for any $x \in K$, the line segment from $0$ to $x$ is contained in $K$).

stdSimplex definition

: Set (ι → 𝕜)

Full source

/-- 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. -/
def stdSimplex : Set (ι → 𝕜) :=
  { f | (∀ x, 0 ≤ f x) ∧ ∑ x, f x = 1 }

Standard simplex in function space

Informal description

The standard simplex in the space of functions $\iota \to \mathbb{k}$ is the set of vectors with non-negative coordinates that sum to 1, defined as $\{ f \colon \iota \to \mathbb{k} \mid (\forall x, 0 \leq f x) \land \sum_x f x = 1 \}$.

stdSimplex_eq_inter theorem

: stdSimplex 𝕜 ι = (⋂ x, {f | 0 ≤ f x}) ∩ {f | ∑ x, f x = 1}

Full source

theorem stdSimplex_eq_inter : stdSimplex 𝕜 ι = (⋂ x, { f | 0 ≤ f x }) ∩ { f | ∑ x, f x = 1 } := by
  ext f
  simp only [stdSimplex, Set.mem_inter_iff, Set.mem_iInter, Set.mem_setOf_eq]

Standard simplex as intersection of non-negativity and unit-sum conditions

Informal description

The standard simplex in the function space $\iota \to \mathbb{k}$ is equal to the intersection of all sets $\{f \mid 0 \leq f x\}$ for $x \in \iota$ with the set $\{f \mid \sum_{x} f x = 1\}$. In other words, it consists of all functions $f \colon \iota \to \mathbb{k}$ that are non-negative at every point and whose values sum to 1.

convex_stdSimplex theorem

[IsOrderedRing 𝕜] : Convex 𝕜 (stdSimplex 𝕜 ι)

Full source

theorem convex_stdSimplex [IsOrderedRing 𝕜] : Convex 𝕜 (stdSimplex 𝕜 ι) := by
  refine fun f hf g hg a b ha hb hab => ⟨fun x => ?_, ?_⟩
  · apply_rules [add_nonneg, mul_nonneg, hf.1, hg.1]
  · simp_rw [Pi.add_apply, Pi.smul_apply]
    rwa [Finset.sum_add_distrib, ← Finset.smul_sum, ← Finset.smul_sum, hf.2, hg.2, smul_eq_mul,
      smul_eq_mul, mul_one, mul_one]

Convexity of the Standard Simplex in Ordered Semirings

Informal description

For any ordered semiring $\mathbb{K}$, the standard simplex in the function space $\iota \to \mathbb{K}$ is convex. That is, for any two functions $f, g$ in the standard simplex and any $t \in [0,1]$, the convex combination $(1-t)f + t g$ also lies in the standard simplex.

stdSimplex_of_subsingleton theorem

[Subsingleton 𝕜] : stdSimplex 𝕜 ι = univ

Full source

@[nontriviality] lemma stdSimplex_of_subsingleton [Subsingleton 𝕜] : stdSimplex 𝕜 ι = univ :=
  eq_univ_of_forall fun _ ↦ ⟨fun _ ↦ (Subsingleton.elim _ _).le, Subsingleton.elim _ _⟩

Standard simplex equals universal set for subsingleton scalar field

Informal description

When the scalar field $\mathbb{k}$ is a subsingleton (i.e., has at most one element), the standard simplex in the function space $\iota \to \mathbb{k}$ is equal to the universal set (the set of all functions from $\iota$ to $\mathbb{k}$).

stdSimplex_of_isEmpty_index theorem

[IsEmpty ι] [Nontrivial 𝕜] : stdSimplex 𝕜 ι = ∅

Full source

/-- The standard simplex in the zero-dimensional space is empty. -/
lemma stdSimplex_of_isEmpty_index [IsEmpty ι] [Nontrivial 𝕜] : stdSimplex 𝕜 ι = ∅ :=
  eq_empty_of_forall_not_mem <| by rintro f ⟨-, hf⟩; simp at hf

Empty Index Type Yields Empty Standard Simplex

Informal description

For a nontrivial scalar field $\mathbb{k}$ and an empty index type $\iota$, the standard simplex in the function space $\iota \to \mathbb{k}$ is the empty set, i.e., $\text{stdSimplex}\,\mathbb{k}\,\iota = \emptyset$.

stdSimplex_unique theorem

[ZeroLEOneClass 𝕜] [Nonempty ι] [Subsingleton ι] : stdSimplex 𝕜 ι = {fun _ ↦ 1}

Full source

lemma stdSimplex_unique [ZeroLEOneClass 𝕜] [Nonempty ι] [Subsingleton ι] :
    stdSimplex 𝕜 ι = {fun _ ↦ 1} := by
  cases nonempty_unique ι
  refine eq_singleton_iff_unique_mem.2 ⟨⟨fun _ ↦ zero_le_one, Fintype.sum_unique _⟩, ?_⟩
  rintro f ⟨-, hf⟩
  rw [Fintype.sum_unique] at hf
  exact funext (Unique.forall_iff.2 hf)

Standard Simplex for Unique Index Type is Singleton of Constant One Function

Informal description

For a scalar field $\mathbb{k}$ where $0 \leq 1$, a nonempty index type $\iota$ that is a subsingleton (has at most one element), the standard simplex in $\iota \to \mathbb{k}$ consists of exactly one function: the constant function that maps every element of $\iota$ to $1$. That is, $\text{stdSimplex}\,\mathbb{k}\,\iota = \{\lambda \_. 1\}$.

single_mem_stdSimplex theorem

(i : ι) : Pi.single i 1 ∈ stdSimplex 𝕜 ι

Full source

theorem single_mem_stdSimplex (i : ι) : Pi.singlePi.single i 1 ∈ stdSimplex 𝕜 ι :=
  ⟨le_update_iff.2 ⟨zero_le_one, fun _ _ ↦ le_rfl⟩, by simp⟩

Indicator Function at Index $i$ Belongs to the Standard Simplex

Informal description

For any index $i$ in the type $\iota$, the function $\mathrm{single}_i(1)$ belongs to the standard simplex in $\iota \to \mathbb{k}$, where $\mathrm{single}_i(1)$ is the function that takes the value $1$ at $i$ and $0$ elsewhere.

ite_eq_mem_stdSimplex theorem

(i : ι) : (if i = · then (1 : 𝕜) else 0) ∈ stdSimplex 𝕜 ι

Full source

theorem ite_eq_mem_stdSimplex (i : ι) : (if i = · then (1 : 𝕜) else 0) ∈ stdSimplex 𝕜 ι := by
  simpa only [@eq_comm _ i, ← Pi.single_apply] using single_mem_stdSimplex 𝕜 i

Indicator Function $\mathbf{1}_i$ Belongs to the Standard Simplex

Informal description

For any index $i$ in the type $\iota$, the indicator function $\mathbf{1}_i$ defined by $\mathbf{1}_i(j) = 1$ if $j = i$ and $0$ otherwise belongs to the standard simplex in $\iota \to \mathbb{k}$. That is, $\mathbf{1}_i \in \text{stdSimplex}\,\mathbb{k}\,\iota$.

segment_single_subset_stdSimplex theorem

(i j : ι) : ([Pi.single i 1 -[𝕜] Pi.single j 1] : Set (ι → 𝕜)) ⊆ stdSimplex 𝕜 ι

Full source

/-- The edges are contained in the simplex. -/
lemma segment_single_subset_stdSimplex (i j : ι) :
    ([Pi.single i 1 -[𝕜] Pi.single j 1] : Set (ι → 𝕜)) ⊆ stdSimplex 𝕜 ι :=
  (convex_stdSimplex 𝕜 ι).segment_subset (single_mem_stdSimplex _ _) (single_mem_stdSimplex _ _)

Segment between Indicator Functions Lies in Standard Simplex

Informal description

For any indices $i, j$ in $\iota$, the segment connecting the indicator functions $\mathrm{single}_i(1)$ and $\mathrm{single}_j(1)$ in the function space $\iota \to \mathbb{k}$ is contained in the standard simplex. That is, for any $t \in [0,1]$, the convex combination $(1-t) \cdot \mathrm{single}_i(1) + t \cdot \mathrm{single}_j(1)$ belongs to the standard simplex.

stdSimplex_fin_two theorem

: stdSimplex 𝕜 (Fin 2) = ([Pi.single 0 1 -[𝕜] Pi.single 1 1] : Set (Fin 2 → 𝕜))

Full source

lemma stdSimplex_fin_two :
    stdSimplex 𝕜 (Fin 2) = ([Pi.single 0 1 -[𝕜] Pi.single 1 1] : Set (Fin 2 → 𝕜)) := by
  refine Subset.antisymm ?_ (segment_single_subset_stdSimplex 𝕜 (0 : Fin 2) 1)
  rintro f ⟨hf₀, hf₁⟩
  rw [Fin.sum_univ_two] at hf₁
  refine ⟨f 0, f 1, hf₀ 0, hf₀ 1, hf₁, funext <| Fin.forall_fin_two.2 ?_⟩
  simp

Standard 1-Simplex as Segment between Basis Vectors

Informal description

The standard simplex in the function space $\text{Fin}\, 2 \to \mathbb{k}$ is equal to the segment connecting the two indicator functions $\mathrm{single}_0(1)$ and $\mathrm{single}_1(1)$. That is, \[ \text{stdSimplex}\,\mathbb{k}\,(\text{Fin}\,2) = \left\{ (1-t) \cdot \mathrm{single}_0(1) + t \cdot \mathrm{single}_1(1) \mid t \in [0,1] \right\}. \]

stdSimplexEquivIcc definition

: stdSimplex 𝕜 (Fin 2) ≃ Icc (0 : 𝕜) 1

Full source

/-- The standard one-dimensional simplex in `Fin 2 → 𝕜` is equivalent to the unit interval. -/
@[simps -fullyApplied]
def stdSimplexEquivIcc : stdSimplexstdSimplex 𝕜 (Fin 2) ≃ Icc (0 : 𝕜) 1 where
  toFun f := ⟨f.1 0, f.2.1 _, f.2.2 ▸
    Finset.single_le_sum (fun i _ ↦ f.2.1 i) (Finset.mem_univ _)⟩
  invFun x := ⟨![x, 1 - x], Fin.forall_fin_two.2 ⟨x.2.1, sub_nonneg.2 x.2.2⟩,
    calc
      ∑ i : Fin 2, ![(x : 𝕜), 1 - x] i = x + (1 - x) := Fin.sum_univ_two _
      _ = 1 := add_sub_cancel _ _⟩
  left_inv f := Subtype.eq <| funext <| Fin.forall_fin_two.2 <| .intro rfl <|
      calc
        (1 : 𝕜) - f.1 0 = f.1 0 + f.1 1 - f.1 0 := by rw [← Fin.sum_univ_two f.1, f.2.2]
        _ = f.1 1 := add_sub_cancel_left _ _
  right_inv _ := Subtype.eq rfl

Equivalence between standard 1-simplex and unit interval

Informal description

The standard one-dimensional simplex in the space of functions $\text{Fin}\, 2 \to \mathbb{k}$ is equivalent to the closed interval $[0,1]$ in $\mathbb{k}$. More precisely, there exists a bijection between: 1. The set of functions $f \colon \text{Fin}\, 2 \to \mathbb{k}$ with non-negative values that sum to 1 (the standard simplex) 2. The closed interval $[0,1] \subseteq \mathbb{k}$ The bijection is given by: - Forward direction: $f \mapsto f(0)$ (the first component) - Backward direction: $x \mapsto (x, 1-x)$ (the pair of components summing to 1)

TODO