Mathlib.Analysis.Convex.Strict

StrictConvex definition

 (𝕜 : Type*) {E : Type*} [Semiring 𝕜] [PartialOrder 𝕜] [TopologicalSpace E] [AddCommMonoid E] [SMul 𝕜 E] (s : Set E) :
  Prop

Full source

/-- A set is strictly convex if the open segment between any two distinct points lies is in its
interior. This basically means "convex and not flat on the boundary". -/
def StrictConvex (𝕜 : Type*) {E : Type*} [Semiring 𝕜] [PartialOrder 𝕜] [TopologicalSpace E]
    [AddCommMonoid E] [SMul 𝕜 E] (s : Set E) : Prop :=
  s.Pairwise fun x y => ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ interior s

Strictly convex set

Informal description

A set $s$ in a topological space $E$ over a partially ordered semiring $\mathbb{K}$ is called *strictly convex* if for any two distinct points $x, y \in s$, the open segment connecting $x$ and $y$ (i.e., all points of the form $a x + b y$ where $a, b > 0$ and $a + b = 1$) lies entirely in the interior of $s$.

strictConvex_iff_openSegment_subset theorem

: StrictConvex 𝕜 s ↔ s.Pairwise fun x y => openSegment 𝕜 x y ⊆ interior s

Full source

theorem strictConvex_iff_openSegment_subset :
    StrictConvexStrictConvex 𝕜 s ↔ s.Pairwise fun x y => openSegment 𝕜 x y ⊆ interior s :=
  forall₅_congr fun _ _ _ _ _ => (openSegment_subset_iff 𝕜).symm

Characterization of Strictly Convex Sets via Open Segments

Informal description

A set $s$ in a topological space $E$ over a partially ordered semiring $\mathbb{K}$ is strictly convex if and only if for every pair of distinct points $x, y \in s$, the open segment connecting $x$ and $y$ is contained in the interior of $s$. That is, $s$ is strictly convex $\iff$ $\forall x, y \in s, x \neq y \implies \text{openSegment}_{\mathbb{K}}(x,y) \subseteq \text{interior}(s)$.

StrictConvex.openSegment_subset theorem

(hs : StrictConvex 𝕜 s) (hx : x ∈ s) (hy : y ∈ s) (h : x ≠ y) : openSegment 𝕜 x y ⊆ interior s

Full source

theorem StrictConvex.openSegment_subset (hs : StrictConvex 𝕜 s) (hx : x ∈ s) (hy : y ∈ s)
    (h : x ≠ y) : openSegmentopenSegment 𝕜 x y ⊆ interior s :=
  strictConvex_iff_openSegment_subset.1 hs hx hy h

Open Segment in Interior of Strictly Convex Set

Informal description

Let $s$ be a strictly convex set in a topological space $E$ over a partially ordered semiring $\mathbb{K}$. For any two distinct points $x, y \in s$, the open segment connecting $x$ and $y$ is contained in the interior of $s$, i.e., $\text{openSegment}_{\mathbb{K}}(x,y) \subseteq \text{interior}(s)$.

strictConvex_empty theorem

: StrictConvex 𝕜 (∅ : Set E)

Full source

theorem strictConvex_empty : StrictConvex 𝕜 (∅ : Set E) :=
  pairwise_empty _

Empty Set is Strictly Convex

Informal description

The empty set is strictly convex in any topological space $E$ over a partially ordered semiring $\mathbb{K}$.

strictConvex_univ theorem

: StrictConvex 𝕜 (univ : Set E)

Full source

theorem strictConvex_univ : StrictConvex 𝕜 (univ : Set E) := by
  intro x _ y _ _ a b _ _ _
  rw [interior_univ]
  exact mem_univ _

Universal Set is Strictly Convex

Informal description

The universal set in a topological space $E$ over a partially ordered semiring $\mathbb{K}$ is strictly convex. That is, for any two distinct points $x, y \in E$, the open segment connecting $x$ and $y$ lies entirely in the interior of $E$.

StrictConvex.eq theorem

 (hs : StrictConvex 𝕜 s) (hx : x ∈ s) (hy : y ∈ s) (ha : 0 < a) (hb : 0 < b) (hab : a + b = 1)
  (h : a • x + b • y ∉ interior s) : x = y

Full source

protected nonrec theorem StrictConvex.eq (hs : StrictConvex 𝕜 s) (hx : x ∈ s) (hy : y ∈ s)
    (ha : 0 < a) (hb : 0 < b) (hab : a + b = 1) (h : a • x + b • y ∉ interior s) : x = y :=
  hs.eq hx hy fun H => h <| H ha hb hab

Equality Condition for Points in a Strictly Convex Set

Informal description

Let $s$ be a strictly convex set in a topological space $E$ over a partially ordered semiring $\mathbb{K}$. For any two points $x, y \in s$ and positive scalars $a, b > 0$ with $a + b = 1$, if the point $a x + b y$ does not lie in the interior of $s$, then $x = y$.

StrictConvex.inter theorem

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

Full source

protected theorem StrictConvex.inter {t : Set E} (hs : StrictConvex 𝕜 s) (ht : StrictConvex 𝕜 t) :
    StrictConvex 𝕜 (s ∩ t) := by
  intro x hx y hy hxy a b ha hb hab
  rw [interior_inter]
  exact ⟨hs hx.1 hy.1 hxy ha hb hab, ht hx.2 hy.2 hxy ha hb hab⟩

Intersection of Strictly Convex Sets is Strictly Convex

Informal description

Let $s$ and $t$ be strictly convex sets in a topological space $E$ over a partially ordered semiring $\mathbb{K}$. Then their intersection $s \cap t$ is also strictly convex.

Directed.strictConvex_iUnion theorem

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

Full source

theorem Directed.strictConvex_iUnion {ι : Sort*} {s : ι → Set E} (hdir : Directed (· ⊆ ·) s)
    (hs : ∀ ⦃i : ι⦄, StrictConvex 𝕜 (s i)) : StrictConvex 𝕜 (⋃ i, s i) := by
  rintro x hx y hy hxy 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 interior_mono (subset_iUnion s k) (hs (hik hx) (hjk hy) hxy ha hb hab)

Union of Directed Family of Strictly Convex Sets is Strictly Convex

Informal description

Let $\{s_i\}_{i \in \iota}$ be a directed family of subsets of a topological space $E$ over a partially ordered semiring $\mathbb{K}$ with respect to the subset relation $\subseteq$. If each $s_i$ is strictly convex, then the union $\bigcup_{i \in \iota} s_i$ is also strictly convex.

DirectedOn.strictConvex_sUnion theorem

 {S : Set (Set E)} (hdir : DirectedOn (· ⊆ ·) S) (hS : ∀ s ∈ S, StrictConvex 𝕜 s) : StrictConvex 𝕜 (⋃₀ S)

Full source

theorem DirectedOn.strictConvex_sUnion {S : Set (Set E)} (hdir : DirectedOn (· ⊆ ·) S)
    (hS : ∀ s ∈ S, StrictConvex 𝕜 s) : StrictConvex 𝕜 (⋃₀ S) := by
  rw [sUnion_eq_iUnion]
  exact (directedOn_iff_directed.1 hdir).strictConvex_iUnion fun s => hS _ s.2

Union of Directed Family of Strictly Convex Sets is Strictly Convex

Informal description

Let $S$ be a collection of subsets of a topological space $E$ over a partially ordered semiring $\mathbb{K}$. If $S$ is directed with respect to the subset relation $\subseteq$ and every set in $S$ is strictly convex, then the union $\bigcup_{s \in S} s$ is strictly convex.

StrictConvex.convex theorem

(hs : StrictConvex 𝕜 s) : Convex 𝕜 s

Full source

protected theorem StrictConvex.convex (hs : StrictConvex 𝕜 s) : Convex 𝕜 s :=
  convex_iff_pairwise_pos.2 fun _ hx _ hy hxy _ _ ha hb hab =>
    interior_subset <| hs hx hy hxy ha hb hab

Strictly convex sets are convex

Informal description

If a set $s$ in a topological space $E$ over a partially ordered semiring $\mathbb{K}$ is strictly convex, then it is convex.

Convex.strictConvex_of_isOpen theorem

(h : IsOpen s) (hs : Convex 𝕜 s) : StrictConvex 𝕜 s

Full source

/-- An open convex set is strictly convex. -/
protected theorem Convex.strictConvex_of_isOpen (h : IsOpen s) (hs : Convex 𝕜 s) :
    StrictConvex 𝕜 s :=
  fun _ hx _ hy _ _ _ ha hb hab => h.interior_eq.symm ▸ hs hx hy ha.le hb.le hab

Open Convex Sets are Strictly Convex

Informal description

Let $E$ be a topological space over a partially ordered semiring $\mathbb{K}$. If a set $s \subseteq E$ is both open and convex, then it is strictly convex.

IsOpen.strictConvex_iff theorem

(h : IsOpen s) : StrictConvex 𝕜 s ↔ Convex 𝕜 s

Full source

theorem IsOpen.strictConvex_iff (h : IsOpen s) : StrictConvexStrictConvex 𝕜 s ↔ Convex 𝕜 s :=
  ⟨StrictConvex.convex, Convex.strictConvex_of_isOpen h⟩

Open Sets are Strictly Convex if and only if They are Convex

Informal description

For an open set $s$ in a topological space $E$ over a partially ordered semiring $\mathbb{K}$, the set $s$ is strictly convex if and only if it is convex.

strictConvex_singleton theorem

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

Full source

theorem strictConvex_singleton (c : E) : StrictConvex 𝕜 ({c} : Set E) :=
  pairwise_singleton _ _

Singleton Sets are Strictly Convex

Informal description

For any point $c$ in a topological space $E$ over a partially ordered semiring $\mathbb{K}$, the singleton set $\{c\}$ is strictly convex.

Set.Subsingleton.strictConvex theorem

(hs : s.Subsingleton) : StrictConvex 𝕜 s

Full source

theorem Set.Subsingleton.strictConvex (hs : s.Subsingleton) : StrictConvex 𝕜 s :=
  hs.pairwise _

Subsingleton Sets are Strictly Convex

Informal description

For any set $s$ in a topological space $E$ over a partially ordered semiring $\mathbb{K}$, if $s$ is a subsingleton (i.e., contains at most one point), then $s$ is strictly convex.

StrictConvex.linear_image theorem

 [Semiring 𝕝] [Module 𝕝 E] [Module 𝕝 F] [LinearMap.CompatibleSMul E F 𝕜 𝕝] (hs : StrictConvex 𝕜 s) (f : E →ₗ[𝕝] F)
  (hf : IsOpenMap f) : StrictConvex 𝕜 (f '' s)

Full source

theorem StrictConvex.linear_image [Semiring 𝕝] [Module 𝕝 E] [Module 𝕝 F]
    [LinearMap.CompatibleSMul E F 𝕜 𝕝] (hs : StrictConvex 𝕜 s) (f : E →ₗ[𝕝] F) (hf : IsOpenMap f) :
    StrictConvex 𝕜 (f '' s) := by
  rintro _ ⟨x, hx, rfl⟩ _ ⟨y, hy, rfl⟩ hxy a b ha hb hab
  refine hf.image_interior_subset _ ⟨a • x + b • y, hs hx hy (ne_of_apply_ne _ hxy) ha hb hab, ?_⟩
  rw [map_add, f.map_smul_of_tower a, f.map_smul_of_tower b]

Strict convexity is preserved under open linear maps

Informal description

Let $\mathbb{K}$ and $\mathbb{L}$ be semirings, and let $E$ and $F$ be modules over $\mathbb{L}$ with compatible scalar actions by $\mathbb{K}$. Suppose $s \subseteq E$ is a strictly convex set and $f \colon E \to F$ is a $\mathbb{L}$-linear map that is also an open map. Then the image $f(s)$ is strictly convex in $F$.

StrictConvex.is_linear_image theorem

(hs : StrictConvex 𝕜 s) {f : E → F} (h : IsLinearMap 𝕜 f) (hf : IsOpenMap f) : StrictConvex 𝕜 (f '' s)

Full source

theorem StrictConvex.is_linear_image (hs : StrictConvex 𝕜 s) {f : E → F} (h : IsLinearMap 𝕜 f)
    (hf : IsOpenMap f) : StrictConvex 𝕜 (f '' s) :=
  hs.linear_image (h.mk' f) hf

Strict convexity is preserved under open linear maps

Informal description

Let $\mathbb{K}$ be a partially ordered semiring, and let $E$ and $F$ be topological spaces equipped with a $\mathbb{K}$-module structure. If $s \subseteq E$ is a strictly convex set and $f \colon E \to F$ is a $\mathbb{K}$-linear map that is also an open map, then the image $f(s)$ is strictly convex in $F$.

StrictConvex.linear_preimage theorem

 {s : Set F} (hs : StrictConvex 𝕜 s) (f : E →ₗ[𝕜] F) (hf : Continuous f) (hfinj : Injective f) :
  StrictConvex 𝕜 (s.preimage f)

Full source

theorem StrictConvex.linear_preimage {s : Set F} (hs : StrictConvex 𝕜 s) (f : E →ₗ[𝕜] F)
    (hf : Continuous f) (hfinj : Injective f) : StrictConvex 𝕜 (s.preimage f) := by
  intro x hx y hy hxy a b ha hb hab
  refine preimage_interior_subset_interior_preimage hf ?_
  rw [mem_preimage, f.map_add, f.map_smul, f.map_smul]
  exact hs hx hy (hfinj.ne hxy) ha hb hab

Preimage of Strictly Convex Set under Injective Continuous Linear Map is Strictly Convex

Informal description

Let $\mathbb{K}$ be a partially ordered semiring, and let $E$ and $F$ be topological vector spaces over $\mathbb{K}$. Suppose $s \subseteq F$ is a strictly convex set, and $f \colon E \to F$ is an injective continuous linear map. Then the preimage $f^{-1}(s)$ is strictly convex in $E$.

StrictConvex.is_linear_preimage theorem

 {s : Set F} (hs : StrictConvex 𝕜 s) {f : E → F} (h : IsLinearMap 𝕜 f) (hf : Continuous f) (hfinj : Injective f) :
  StrictConvex 𝕜 (s.preimage f)

Full source

theorem StrictConvex.is_linear_preimage {s : Set F} (hs : StrictConvex 𝕜 s) {f : E → F}
    (h : IsLinearMap 𝕜 f) (hf : Continuous f) (hfinj : Injective f) :
    StrictConvex 𝕜 (s.preimage f) :=
  hs.linear_preimage (h.mk' f) hf hfinj

Preimage of Strictly Convex Set under Injective Continuous Linear Map is Strictly Convex

Informal description

Let $\mathbb{K}$ be a partially ordered semiring, and let $E$ and $F$ be topological vector spaces over $\mathbb{K}$. Suppose $s \subseteq F$ is a strictly convex set, and $f \colon E \to F$ is an injective continuous linear map. Then the preimage $f^{-1}(s)$ is strictly convex in $E$.

Set.OrdConnected.strictConvex theorem

{s : Set β} (hs : OrdConnected s) : StrictConvex 𝕜 s

Full source

protected theorem Set.OrdConnected.strictConvex {s : Set β} (hs : OrdConnected s) :
    StrictConvex 𝕜 s := by
  refine strictConvex_iff_openSegment_subset.2 fun x hx y hy hxy => ?_
  rcases hxy.lt_or_lt with hlt | hlt <;> [skip; rw [openSegment_symm]] <;>
    exact
      (openSegment_subset_Ioo hlt).trans
        (isOpen_Ioo.subset_interior_iff.2 <| Ioo_subset_Icc_self.trans <| hs.out ‹_› ‹_›)

Order-Connected Sets are Strictly Convex

Informal description

For any order-connected set $s$ in a topological space $\beta$ over a partially ordered semiring $\mathbb{K}$, the set $s$ is strictly convex. That is, if for any two points $x, y \in s$ the closed interval $[x, y]$ is contained in $s$, then for any two distinct points $x, y \in s$, the open segment connecting $x$ and $y$ lies entirely in the interior of $s$.

strictConvex_Iic theorem

(r : β) : StrictConvex 𝕜 (Iic r)

Full source

theorem strictConvex_Iic (r : β) : StrictConvex 𝕜 (Iic r) :=
  ordConnected_Iic.strictConvex

Strict Convexity of Left-Infinite Right-Closed Interval $(-\infty, r]$

Informal description

For any element $r$ in a topological space $\beta$ over a partially ordered semiring $\mathbb{K}$, the left-infinite right-closed interval $(-\infty, r]$ is strictly convex. That is, for any two distinct points $x, y \in (-\infty, r]$, the open segment connecting $x$ and $y$ lies entirely in the interior of $(-\infty, r]$.

strictConvex_Ici theorem

(r : β) : StrictConvex 𝕜 (Ici r)

Full source

theorem strictConvex_Ici (r : β) : StrictConvex 𝕜 (Ici r) :=
  ordConnected_Ici.strictConvex

Strict convexity of the interval $[r, \infty)$

Informal description

For any element $r$ in a topological space $\beta$ over a partially ordered semiring $\mathbb{K}$, the left-closed right-infinite interval $[r, \infty)$ is strictly convex. That is, for any two distinct points $x, y \in [r, \infty)$, the open segment connecting $x$ and $y$ lies entirely in the interior of $[r, \infty)$.

strictConvex_Iio theorem

(r : β) : StrictConvex 𝕜 (Iio r)

Full source

theorem strictConvex_Iio (r : β) : StrictConvex 𝕜 (Iio r) :=
  ordConnected_Iio.strictConvex

Strict convexity of the open interval $(-\infty, r)$

Informal description

For any element $r$ in a topological space $\beta$ over a partially ordered semiring $\mathbb{K}$, the open interval $(-\infty, r)$ is strictly convex. That is, for any two distinct points $x, y \in (-\infty, r)$, the open segment connecting $x$ and $y$ lies entirely in the interior of $(-\infty, r)$.

strictConvex_Ioi theorem

(r : β) : StrictConvex 𝕜 (Ioi r)

Full source

theorem strictConvex_Ioi (r : β) : StrictConvex 𝕜 (Ioi r) :=
  ordConnected_Ioi.strictConvex

Open upper interval $(r, \infty)$ is strictly convex

Informal description

For any element $r$ in a topological space $\beta$ over a partially ordered semiring $\mathbb{K}$, the open interval $(r, \infty)$ is strictly convex. That is, for any two distinct points $x, y \in (r, \infty)$, the open segment connecting $x$ and $y$ lies entirely in the interior of $(r, \infty)$.

strictConvex_Icc theorem

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

Full source

theorem strictConvex_Icc (r s : β) : StrictConvex 𝕜 (Icc r s) :=
  ordConnected_Icc.strictConvex

Closed Intervals are Strictly Convex

Informal description

For any elements $r$ and $s$ in a topological space $\beta$ over a partially ordered semiring $\mathbb{K}$, the closed interval $[r, s] = \{x \in \beta \mid r \leq x \leq s\}$ is strictly convex. That is, for any two distinct points $x, y \in [r, s]$, the open segment connecting $x$ and $y$ lies entirely in the interior of $[r, s]$.

strictConvex_Ioo theorem

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

Full source

theorem strictConvex_Ioo (r s : β) : StrictConvex 𝕜 (Ioo r s) :=
  ordConnected_Ioo.strictConvex

Open intervals are strictly convex

Informal description

For any elements $r$ and $s$ in a topological space $\beta$ over a partially ordered semiring $\mathbb{K}$, the open interval $(r, s) = \{x \in \beta \mid r < x < s\}$ is strictly convex. That is, for any two distinct points $x, y \in (r, s)$, the open segment connecting $x$ and $y$ lies entirely in the interior of $(r, s)$.

strictConvex_Ico theorem

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

Full source

theorem strictConvex_Ico (r s : β) : StrictConvex 𝕜 (Ico r s) :=
  ordConnected_Ico.strictConvex

Strict convexity of the interval $[r, s)$

Informal description

For any two elements $r$ and $s$ in a topological space $\beta$ over a partially ordered semiring $\mathbb{K}$, the left-closed right-open interval $[r, s)$ is strictly convex. That is, for any two distinct points $x, y \in [r, s)$, the open segment connecting $x$ and $y$ lies entirely in the interior of $[r, s)$.

strictConvex_Ioc theorem

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

Full source

theorem strictConvex_Ioc (r s : β) : StrictConvex 𝕜 (Ioc r s) :=
  ordConnected_Ioc.strictConvex

Strict convexity of the interval $(r, s]$

Informal description

For any two elements $r$ and $s$ in a topological space $\beta$ over a partially ordered semiring $\mathbb{K}$, the left-open right-closed interval $(r, s] = \{x \in \beta \mid r < x \leq s\}$ is strictly convex. That is, for any two distinct points $x, y \in (r, s]$, the open segment connecting $x$ and $y$ lies entirely in the interior of $(r, s]$.

strictConvex_uIcc theorem

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

Full source

theorem strictConvex_uIcc (r s : β) : StrictConvex 𝕜 (uIcc r s) :=
  strictConvex_Icc _ _

Strict Convexity of Unordered Closed Intervals

Informal description

For any two elements $r$ and $s$ in a topological space $\beta$ over a partially ordered semiring $\mathbb{K}$, the unordered closed interval $\text{uIcc}(r, s) = [r \sqcap s, r \sqcup s]$ is strictly convex. That is, for any two distinct points $x, y \in \text{uIcc}(r, s)$, the open segment connecting $x$ and $y$ lies entirely in the interior of $\text{uIcc}(r, s)$.

strictConvex_uIoc theorem

(r s : β) : StrictConvex 𝕜 (uIoc r s)

Full source

theorem strictConvex_uIoc (r s : β) : StrictConvex 𝕜 (uIoc r s) :=
  strictConvex_Ioc _ _

Strict convexity of the unordered open-closed interval $\text{uIoc}(r, s)$

Informal description

For any two elements $r$ and $s$ in a topological space $\beta$ over a partially ordered semiring $\mathbb{K}$, the unordered open-closed interval $\text{uIoc}(r, s) = \{x \in \beta \mid \min(r, s) < x \leq \max(r, s)\}$ is strictly convex. That is, for any two distinct points $x, y \in \text{uIoc}(r, s)$, the open segment connecting $x$ and $y$ lies entirely in the interior of $\text{uIoc}(r, s)$.

StrictConvex.preimage_add_right theorem

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

Full source

/-- The translation of a strictly convex set is also strictly convex. -/
theorem StrictConvex.preimage_add_right (hs : StrictConvex 𝕜 s) (z : E) :
    StrictConvex 𝕜 ((fun x => z + x) ⁻¹' s) := by
  intro x hx y hy hxy a b ha hb hab
  refine preimage_interior_subset_interior_preimage (continuous_add_left _) ?_
  have h := hs hx hy ((add_right_injective _).ne hxy) ha hb hab
  rwa [smul_add, smul_add, add_add_add_comm, ← _root_.add_smul, hab, one_smul] at h

Strict convexity is preserved under right translation preimages

Informal description

Let $E$ be a topological space with an additive commutative monoid structure and a scalar multiplication by a partially ordered semiring $\mathbb{K}$. If $s \subseteq E$ is a strictly convex set, then for any $z \in E$, the preimage of $s$ under the function $x \mapsto z + x$ is also strictly convex.

StrictConvex.preimage_add_left theorem

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

Full source

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

Strict convexity is preserved under left translation preimages

Informal description

Let $E$ be a topological space with an additive commutative monoid structure and a scalar multiplication by a partially ordered semiring $\mathbb{K}$. If $s \subseteq E$ is a strictly convex set, then for any $z \in E$, the preimage of $s$ under the function $x \mapsto x + z$ is also strictly convex.

StrictConvex.add theorem

(hs : StrictConvex 𝕜 s) (ht : StrictConvex 𝕜 t) : StrictConvex 𝕜 (s + t)

Full source

theorem StrictConvex.add (hs : StrictConvex 𝕜 s) (ht : StrictConvex 𝕜 t) :
    StrictConvex 𝕜 (s + t) := by
  rintro _ ⟨v, hv, w, hw, rfl⟩ _ ⟨x, hx, y, hy, rfl⟩ h a b ha hb hab
  rw [smul_add, smul_add, add_add_add_comm]
  obtain rfl | hvx := eq_or_ne v x
  · refine interior_mono (add_subset_add (singleton_subset_iff.2 hv) Subset.rfl) ?_
    rw [Convex.combo_self hab, singleton_add]
    exact
      (isOpenMap_add_left _).image_interior_subset _
        (mem_image_of_mem _ <| ht hw hy (ne_of_apply_ne _ h) ha hb hab)
  exact
    subset_interior_add_left
      (add_mem_add (hs hv hx hvx ha hb hab) <| ht.convex hw hy ha.le hb.le hab)

Minkowski Sum of Strictly Convex Sets is Strictly Convex

Informal description

Let $E$ be a topological space with an additive commutative monoid structure and a scalar multiplication by a partially ordered semiring $\mathbb{K}$. If $s, t \subseteq E$ are strictly convex sets, then their Minkowski sum $s + t = \{x + y \mid x \in s, y \in t\}$ is also strictly convex.

StrictConvex.add_left theorem

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

Full source

theorem StrictConvex.add_left (hs : StrictConvex 𝕜 s) (z : E) :
    StrictConvex 𝕜 ((fun x => z + x) '' s) := by
  simpa only [singleton_add] using (strictConvex_singleton z).add hs

Strict convexity is preserved under left translation images

Informal description

Let $E$ be a topological space with an additive commutative monoid structure and a scalar multiplication by a partially ordered semiring $\mathbb{K}$. If $s \subseteq E$ is a strictly convex set, then for any $z \in E$, the image of $s$ under the function $x \mapsto z + x$ is also strictly convex.

StrictConvex.add_right theorem

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

Full source

theorem StrictConvex.add_right (hs : StrictConvex 𝕜 s) (z : E) :
    StrictConvex 𝕜 ((fun x => x + z) '' s) := by simpa only [add_comm] using hs.add_left z

Strict convexity is preserved under right translation images

Informal description

Let $E$ be a topological space with an additive commutative monoid structure and a scalar multiplication by a partially ordered semiring $\mathbb{K}$. If $s \subseteq E$ is a strictly convex set, then for any $z \in E$, the image of $s$ under the function $x \mapsto x + z$ is also strictly convex.

StrictConvex.vadd theorem

(hs : StrictConvex 𝕜 s) (x : E) : StrictConvex 𝕜 (x +ᵥ s)

Full source

/-- The translation of a strictly convex set is also strictly convex. -/
theorem StrictConvex.vadd (hs : StrictConvex 𝕜 s) (x : E) : StrictConvex 𝕜 (x +ᵥ s) :=
  hs.add_left x

Strict convexity is preserved under vector addition translation

Informal description

Let $E$ be a topological space with an additive commutative monoid structure and a scalar multiplication by a partially ordered semiring $\mathbb{K}$. If $s \subseteq E$ is a strictly convex set, then for any $x \in E$, the set $x +ᵥ s$ (the translation of $s$ by $x$) is also strictly convex.

StrictConvex.smul theorem

(hs : StrictConvex 𝕜 s) (c : 𝕝) : StrictConvex 𝕜 (c • s)

Full source

theorem StrictConvex.smul (hs : StrictConvex 𝕜 s) (c : 𝕝) : StrictConvex 𝕜 (c • s) := by
  obtain rfl | hc := eq_or_ne c 0
  · exact (subsingleton_zero_smul_set _).strictConvex
  · exact hs.linear_image (LinearMap.lsmul _ _ c) (isOpenMap_smul₀ hc)

Strict convexity is preserved under scalar multiplication

Informal description

Let $E$ be a topological space with an additive commutative monoid structure and a scalar multiplication action by a semiring $\mathbb{K}$. If $s \subseteq E$ is a strictly convex set and $c$ is an element of a semiring $\mathbb{L}$ acting on $E$, then the scaled set $c \cdot s$ is also strictly convex.

StrictConvex.affinity theorem

[ContinuousAdd E] (hs : StrictConvex 𝕜 s) (z : E) (c : 𝕝) : StrictConvex 𝕜 (z +ᵥ c • s)

Full source

theorem StrictConvex.affinity [ContinuousAdd E] (hs : StrictConvex 𝕜 s) (z : E) (c : 𝕝) :
    StrictConvex 𝕜 (z +ᵥ c • s) :=
  (hs.smul c).vadd z

Strict Convexity is Preserved under Affine Transformations

Informal description

Let $E$ be a topological space with a continuous addition operation and a scalar multiplication action by a partially ordered semiring $\mathbb{K}$. If $s \subseteq E$ is a strictly convex set, then for any $z \in E$ and scalar $c \in \mathbb{L}$, the affine transformation $z + c \cdot s$ is also strictly convex.

StrictConvex.preimage_smul theorem

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

Full source

theorem StrictConvex.preimage_smul (hs : StrictConvex 𝕜 s) (c : 𝕜) :
    StrictConvex 𝕜 ((fun z => c • z) ⁻¹' s) := by
  classical
    obtain rfl | hc := eq_or_ne c 0
    · simp_rw [zero_smul, preimage_const]
      split_ifs
      · exact strictConvex_univ
      · exact strictConvex_empty
    refine hs.linear_preimage (LinearMap.lsmul _ _ c) ?_ (smul_right_injective E hc)
    unfold LinearMap.lsmul LinearMap.mk₂ LinearMap.mk₂' LinearMap.mk₂'ₛₗ
    exact continuous_const_smul _

Preimage of Strictly Convex Set under Scalar Multiplication is Strictly Convex

Informal description

Let $\mathbb{K}$ be a partially ordered semiring and $E$ be a topological space with an additive commutative monoid structure and a scalar multiplication by $\mathbb{K}$. If $s \subseteq E$ is a strictly convex set and $c \in \mathbb{K}$, then the preimage of $s$ under the scalar multiplication map $z \mapsto c \cdot z$ is strictly convex in $E$.

StrictConvex.add_smul_mem theorem

 [AddRightStrictMono 𝕜] (hs : StrictConvex 𝕜 s) (hx : x ∈ s) (hxy : x + y ∈ s) (hy : y ≠ 0) {t : 𝕜} (ht₀ : 0 < t)
  (ht₁ : t < 1) : x + t • y ∈ interior s

Full source

theorem StrictConvex.add_smul_mem [AddRightStrictMono 𝕜]
    (hs : StrictConvex 𝕜 s) (hx : x ∈ s) (hxy : x + y ∈ s)
    (hy : y ≠ 0) {t : 𝕜} (ht₀ : 0 < t) (ht₁ : t < 1) : x + t • y ∈ interior s := by
  have h : x + t • y = (1 - t) • x + t • (x + y) := by match_scalars <;> field_simp
  rw [h]
  exact hs hx hxy (fun h => hy <| add_left_cancel (a := x) (by rw [← h, add_zero]))
    (sub_pos_of_lt ht₁) ht₀ (sub_add_cancel 1 t)

Strictly Convex Set Property: $x + t y \in \text{interior}(s)$ for $0 < t < 1$

Informal description

Let $\mathbb{K}$ be a partially ordered semiring and $E$ be a topological space with an additive commutative monoid structure and a scalar multiplication by $\mathbb{K}$. Given a strictly convex set $s \subseteq E$, a point $x \in s$, and a vector $y \neq 0$ such that $x + y \in s$, then for any $t \in \mathbb{K}$ with $0 < t < 1$, the point $x + t y$ lies in the interior of $s$.

StrictConvex.smul_mem_of_zero_mem theorem

 [AddRightStrictMono 𝕜] (hs : StrictConvex 𝕜 s) (zero_mem : (0 : E) ∈ s) (hx : x ∈ s) (hx₀ : x ≠ 0) {t : 𝕜}
  (ht₀ : 0 < t) (ht₁ : t < 1) : t • x ∈ interior s

Full source

theorem StrictConvex.smul_mem_of_zero_mem [AddRightStrictMono 𝕜]
    (hs : StrictConvex 𝕜 s) (zero_mem : (0 : E) ∈ s)
    (hx : x ∈ s) (hx₀ : x ≠ 0) {t : 𝕜} (ht₀ : 0 < t) (ht₁ : t < 1) : t • x ∈ interior s := by
  simpa using hs.add_smul_mem zero_mem (by simpa using hx) hx₀ ht₀ ht₁

Strictly Convex Set Property: $t x \in \text{interior}(s)$ for $0 < t < 1$ and $x \neq 0$

Informal description

Let $\mathbb{K}$ be a partially ordered semiring and $E$ be a topological space with an additive commutative monoid structure and a scalar multiplication by $\mathbb{K}$. Given a strictly convex set $s \subseteq E$ containing $0$, a nonzero point $x \in s$, and a scalar $t \in \mathbb{K}$ with $0 < t < 1$, the point $t x$ lies in the interior of $s$.

StrictConvex.add_smul_sub_mem theorem

 [AddRightMono 𝕜] (h : StrictConvex 𝕜 s) (hx : x ∈ s) (hy : y ∈ s) (hxy : x ≠ y) {t : 𝕜} (ht₀ : 0 < t) (ht₁ : t < 1) :
  x + t • (y - x) ∈ interior s

Full source

theorem StrictConvex.add_smul_sub_mem [AddRightMono 𝕜]
    (h : StrictConvex 𝕜 s) (hx : x ∈ s) (hy : y ∈ s) (hxy : x ≠ y)
    {t : 𝕜} (ht₀ : 0 < t) (ht₁ : t < 1) : x + t • (y - x) ∈ interior s := by
  apply h.openSegment_subset hx hy hxy
  rw [openSegment_eq_image']
  exact mem_image_of_mem _ ⟨ht₀, ht₁⟩

Strictly Convex Set Property: Convex Combination of Distinct Points Lies in Interior

Informal description

Let $\mathbb{K}$ be a partially ordered semiring and $E$ be a topological space with an additive commutative monoid structure and a scalar multiplication by $\mathbb{K}$. Given a strictly convex set $s \subseteq E$ and two distinct points $x, y \in s$, for any $t \in \mathbb{K}$ with $0 < t < 1$, the point $x + t(y - x)$ lies in the interior of $s$.

StrictConvex.affine_preimage theorem

 {s : Set F} (hs : StrictConvex 𝕜 s) {f : E →ᵃ[𝕜] F} (hf : Continuous f) (hfinj : Injective f) :
  StrictConvex 𝕜 (f ⁻¹' s)

Full source

/-- The preimage of a strictly convex set under an affine map is strictly convex. -/
theorem StrictConvex.affine_preimage {s : Set F} (hs : StrictConvex 𝕜 s) {f : E →ᵃ[𝕜] F}
    (hf : Continuous f) (hfinj : Injective f) : StrictConvex 𝕜 (f ⁻¹' s) := by
  intro x hx y hy hxy a b ha hb hab
  refine preimage_interior_subset_interior_preimage hf ?_
  rw [mem_preimage, Convex.combo_affine_apply hab]
  exact hs hx hy (hfinj.ne hxy) ha hb hab

Preimage of Strictly Convex Set under Injective Continuous Affine Map is Strictly Convex

Informal description

Let $E$ and $F$ be topological vector spaces over a partially ordered semiring $\mathbb{K}$, and let $s \subseteq F$ be a strictly convex set. If $f \colon E \to F$ is an injective continuous affine map, then the preimage $f^{-1}(s) \subseteq E$ is strictly convex.

StrictConvex.affine_image theorem

(hs : StrictConvex 𝕜 s) {f : E →ᵃ[𝕜] F} (hf : IsOpenMap f) : StrictConvex 𝕜 (f '' s)

Full source

/-- The image of a strictly convex set under an affine map is strictly convex. -/
theorem StrictConvex.affine_image (hs : StrictConvex 𝕜 s) {f : E →ᵃ[𝕜] F} (hf : IsOpenMap f) :
    StrictConvex 𝕜 (f '' s) := by
  rintro _ ⟨x, hx, rfl⟩ _ ⟨y, hy, rfl⟩ hxy a b ha hb hab
  exact
    hf.image_interior_subset _
      ⟨a • x + b • y, ⟨hs hx hy (ne_of_apply_ne _ hxy) ha hb hab, Convex.combo_affine_apply hab⟩⟩

Strict Convexity is Preserved under Open Affine Maps

Informal description

Let $E$ and $F$ be topological vector spaces over a partially ordered semiring $\mathbb{K}$, and let $s \subseteq E$ be a strictly convex set. If $f \colon E \to F$ is an affine map that is also an open map, then the image $f(s) \subseteq F$ is strictly convex.

StrictConvex.neg theorem

(hs : StrictConvex 𝕜 s) : StrictConvex 𝕜 (-s)

Full source

theorem StrictConvex.neg (hs : StrictConvex 𝕜 s) : StrictConvex 𝕜 (-s) :=
  hs.is_linear_preimage IsLinearMap.isLinearMap_neg continuous_id.neg neg_injective

Negation preserves strict convexity

Informal description

If a set $s$ in a topological vector space over a partially ordered semiring $\mathbb{K}$ is strictly convex, then its negation $-s = \{-x \mid x \in s\}$ is also strictly convex.

StrictConvex.sub theorem

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

Full source

theorem StrictConvex.sub (hs : StrictConvex 𝕜 s) (ht : StrictConvex 𝕜 t) : StrictConvex 𝕜 (s - t) :=
  (sub_eq_add_neg s t).symm ▸ hs.add ht.neg

Minkowski Difference of Strictly Convex Sets is Strictly Convex

Informal description

Let $E$ be a topological space with an additive commutative monoid structure and a scalar multiplication by a partially ordered semiring $\mathbb{K}$. If $s, t \subseteq E$ are strictly convex sets, then their Minkowski difference $s - t = \{x - y \mid x \in s, y \in t\}$ is also strictly convex.

strictConvex_iff_div theorem

 :
  StrictConvex 𝕜 s ↔
    s.Pairwise fun x y => ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → (a / (a + b)) • x + (b / (a + b)) • y ∈ interior s

Full source

/-- Alternative definition of set strict convexity, using division. -/
theorem strictConvex_iff_div :
    StrictConvexStrictConvex 𝕜 s ↔
      s.Pairwise fun x y =>
        ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → (a / (a + b)) • x + (b / (a + b)) • y ∈ interior s :=
  ⟨fun h x hx y hy hxy a b ha hb ↦ h hx hy hxy (by positivity) (by positivity) (by field_simp),
    fun h x hx y hy hxy a b ha hb hab ↦ by
    convert h hx hy hxy ha hb <;> rw [hab, div_one]⟩

Characterization of Strictly Convex Sets via Division

Informal description

A set $s$ in a topological space $E$ over a partially ordered semiring $\mathbb{K}$ is strictly convex if and only if for every pair of distinct points $x, y \in s$ and for any positive elements $a, b \in \mathbb{K}$, the point $\left(\frac{a}{a+b}\right) \cdot x + \left(\frac{b}{a+b}\right) \cdot y$ lies in the interior of $s$.

StrictConvex.mem_smul_of_zero_mem theorem

 (hs : StrictConvex 𝕜 s) (zero_mem : (0 : E) ∈ s) (hx : x ∈ s) (hx₀ : x ≠ 0) {t : 𝕜} (ht : 1 < t) : x ∈ t • interior s

Full source

theorem StrictConvex.mem_smul_of_zero_mem (hs : StrictConvex 𝕜 s) (zero_mem : (0 : E) ∈ s)
    (hx : x ∈ s) (hx₀ : x ≠ 0) {t : 𝕜} (ht : 1 < t) : x ∈ t • interior s := by
  rw [mem_smul_set_iff_inv_smul_mem₀ (by positivity)]
  exact hs.smul_mem_of_zero_mem zero_mem hx hx₀ (by positivity) (inv_lt_one_of_one_lt₀ ht)

Strictly Convex Set Property: $x \in t \cdot \text{interior}(s)$ for $t > 1$ and $x \neq 0$

Informal description

Let $\mathbb{K}$ be a partially ordered semiring and $E$ be a topological space with an additive commutative monoid structure and a scalar multiplication by $\mathbb{K}$. Given a strictly convex set $s \subseteq E$ containing $0$, a nonzero point $x \in s$, and a scalar $t \in \mathbb{K}$ with $t > 1$, the point $x$ lies in the dilation $t \cdot \text{interior}(s)$ of the interior of $s$.

strictConvex_iff_convex theorem

: StrictConvex 𝕜 s ↔ Convex 𝕜 s

Full source

/-- A set in a linear ordered field is strictly convex if and only if it is convex. -/
@[simp]
theorem strictConvex_iff_convex : StrictConvexStrictConvex 𝕜 s ↔ Convex 𝕜 s :=
  ⟨StrictConvex.convex, fun hs => hs.ordConnected.strictConvex⟩

Equivalence of Strict Convexity and Convexity in Ordered Semirings

Informal description

A set $s$ in a topological space $E$ over a partially ordered semiring $\mathbb{K}$ is strictly convex if and only if it is convex.

strictConvex_iff_ordConnected theorem

: StrictConvex 𝕜 s ↔ s.OrdConnected

Full source

theorem strictConvex_iff_ordConnected : StrictConvexStrictConvex 𝕜 s ↔ s.OrdConnected :=
  strictConvex_iff_convex.trans convex_iff_ordConnected

Equivalence of Strict Convexity and Order Connectedness

Informal description

A set $s$ in a topological space $E$ over a partially ordered semiring $\mathbb{K}$ is strictly convex if and only if it is order connected, meaning that for any two points $x, y \in s$, the closed interval $[x, y]$ is entirely contained in $s$.