# Strictly convex sets #

This file defines strictly convex sets.

A set is strictly convex if the open segment between any two distinct points lies in its interior.

def StrictConvex (๐ : Type u_1) {E : Type u_3} [OrderedSemiring ๐] [] [] [SMul ๐ E] (s : Set E) :

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".

Equations
Instances For
theorem strictConvex_iff_openSegment_subset {๐ : Type u_1} {E : Type u_3} [OrderedSemiring ๐] [] [] [SMul ๐ E] {s : Set E} :
StrictConvex ๐ s โ s.Pairwise fun (x y : E) => openSegment ๐ x y โ
theorem StrictConvex.openSegment_subset {๐ : Type u_1} {E : Type u_3} [OrderedSemiring ๐] [] [] [SMul ๐ E] {s : Set E} {x : E} {y : E} (hs : StrictConvex ๐ s) (hx : x โ s) (hy : y โ s) (h : x โ  y) :
openSegment ๐ x y โ
theorem strictConvex_empty {๐ : Type u_1} {E : Type u_3} [OrderedSemiring ๐] [] [] [SMul ๐ E] :
theorem strictConvex_univ {๐ : Type u_1} {E : Type u_3} [OrderedSemiring ๐] [] [] [SMul ๐ E] :
StrictConvex ๐ Set.univ
theorem StrictConvex.eq {๐ : Type u_1} {E : Type u_3} [OrderedSemiring ๐] [] [] [SMul ๐ E] {s : Set E} {x : E} {y : E} {a : ๐} {b : ๐} (hs : StrictConvex ๐ s) (hx : x โ s) (hy : y โ s) (ha : 0 < a) (hb : 0 < b) (hab : a + b = 1) (h : a โข x + b โข y โ ) :
x = y
theorem StrictConvex.inter {๐ : Type u_1} {E : Type u_3} [OrderedSemiring ๐] [] [] [SMul ๐ E] {s : Set E} {t : Set E} (hs : StrictConvex ๐ s) (ht : StrictConvex ๐ t) :
StrictConvex ๐ (s โฉ t)
theorem Directed.strictConvex_iUnion {๐ : Type u_1} {E : Type u_3} [OrderedSemiring ๐] [] [] [SMul ๐ E] {ฮน : Sort u_6} {s : ฮน โ Set E} (hdir : Directed (fun (x1 x2 : Set E) => x1 โ x2) s) (hs : โ โฆi : ฮนโฆ, StrictConvex ๐ (s i)) :
StrictConvex ๐ (โ (i : ฮน), s i)
theorem DirectedOn.strictConvex_sUnion {๐ : Type u_1} {E : Type u_3} [OrderedSemiring ๐] [] [] [SMul ๐ E] {S : Set (Set E)} (hdir : DirectedOn (fun (x1 x2 : Set E) => x1 โ x2) S) (hS : โ s โ S, StrictConvex ๐ s) :
theorem StrictConvex.convex {๐ : Type u_1} {E : Type u_3} [OrderedSemiring ๐] [] [] [Module ๐ E] {s : Set E} (hs : StrictConvex ๐ s) :
Convex ๐ s
theorem Convex.strictConvex_of_isOpen {๐ : Type u_1} {E : Type u_3} [OrderedSemiring ๐] [] [] [Module ๐ E] {s : Set E} (h : ) (hs : Convex ๐ s) :
StrictConvex ๐ s

An open convex set is strictly convex.

theorem IsOpen.strictConvex_iff {๐ : Type u_1} {E : Type u_3} [OrderedSemiring ๐] [] [] [Module ๐ E] {s : Set E} (h : ) :
StrictConvex ๐ s โ Convex ๐ s
theorem strictConvex_singleton {๐ : Type u_1} {E : Type u_3} [OrderedSemiring ๐] [] [] [Module ๐ E] (c : E) :
StrictConvex ๐ {c}
theorem Set.Subsingleton.strictConvex {๐ : Type u_1} {E : Type u_3} [OrderedSemiring ๐] [] [] [Module ๐ E] {s : Set E} (hs : s.Subsingleton) :
StrictConvex ๐ s
theorem StrictConvex.linear_image {๐ : Type u_1} {๐ : Type u_2} {E : Type u_3} {F : Type u_4} [OrderedSemiring ๐] [] [] [] [] [Module ๐ E] [Module ๐ F] {s : Set E} [Semiring ๐] [Module ๐ E] [Module ๐ F] [LinearMap.CompatibleSMul E F ๐ ๐] (hs : StrictConvex ๐ s) (f : E โโ[๐] F) (hf : IsOpenMap โf) :
StrictConvex ๐ (โf '' s)
theorem StrictConvex.is_linear_image {๐ : Type u_1} {E : Type u_3} {F : Type u_4} [OrderedSemiring ๐] [] [] [] [] [Module ๐ E] [Module ๐ F] {s : Set E} (hs : StrictConvex ๐ s) {f : E โ F} (h : IsLinearMap ๐ f) (hf : ) :
StrictConvex ๐ (f '' s)
theorem StrictConvex.linear_preimage {๐ : Type u_1} {E : Type u_3} {F : Type u_4} [OrderedSemiring ๐] [] [] [] [] [Module ๐ E] [Module ๐ F] {s : Set F} (hs : StrictConvex ๐ s) (f : E โโ[๐] F) (hf : Continuous โf) (hfinj : ) :
StrictConvex ๐ (โf โปยน' s)
theorem StrictConvex.is_linear_preimage {๐ : Type u_1} {E : Type u_3} {F : Type u_4} [OrderedSemiring ๐] [] [] [] [] [Module ๐ E] [Module ๐ F] {s : Set F} (hs : StrictConvex ๐ s) {f : E โ F} (h : IsLinearMap ๐ f) (hf : ) (hfinj : ) :
theorem Set.OrdConnected.strictConvex {๐ : Type u_1} {ฮฒ : Type u_5} [OrderedSemiring ๐] [] [] [Module ๐ ฮฒ] [OrderedSMul ๐ ฮฒ] {s : Set ฮฒ} (hs : s.OrdConnected) :
StrictConvex ๐ s
theorem strictConvex_Iic {๐ : Type u_1} {ฮฒ : Type u_5} [OrderedSemiring ๐] [] [] [Module ๐ ฮฒ] [OrderedSMul ๐ ฮฒ] (r : ฮฒ) :
StrictConvex ๐ (Set.Iic r)
theorem strictConvex_Ici {๐ : Type u_1} {ฮฒ : Type u_5} [OrderedSemiring ๐] [] [] [Module ๐ ฮฒ] [OrderedSMul ๐ ฮฒ] (r : ฮฒ) :
StrictConvex ๐ (Set.Ici r)
theorem strictConvex_Iio {๐ : Type u_1} {ฮฒ : Type u_5} [OrderedSemiring ๐] [] [] [Module ๐ ฮฒ] [OrderedSMul ๐ ฮฒ] (r : ฮฒ) :
StrictConvex ๐ (Set.Iio r)
theorem strictConvex_Ioi {๐ : Type u_1} {ฮฒ : Type u_5} [OrderedSemiring ๐] [] [] [Module ๐ ฮฒ] [OrderedSMul ๐ ฮฒ] (r : ฮฒ) :
StrictConvex ๐ (Set.Ioi r)
theorem strictConvex_Icc {๐ : Type u_1} {ฮฒ : Type u_5} [OrderedSemiring ๐] [] [] [Module ๐ ฮฒ] [OrderedSMul ๐ ฮฒ] (r : ฮฒ) (s : ฮฒ) :
StrictConvex ๐ (Set.Icc r s)
theorem strictConvex_Ioo {๐ : Type u_1} {ฮฒ : Type u_5} [OrderedSemiring ๐] [] [] [Module ๐ ฮฒ] [OrderedSMul ๐ ฮฒ] (r : ฮฒ) (s : ฮฒ) :
StrictConvex ๐ (Set.Ioo r s)
theorem strictConvex_Ico {๐ : Type u_1} {ฮฒ : Type u_5} [OrderedSemiring ๐] [] [] [Module ๐ ฮฒ] [OrderedSMul ๐ ฮฒ] (r : ฮฒ) (s : ฮฒ) :
StrictConvex ๐ (Set.Ico r s)
theorem strictConvex_Ioc {๐ : Type u_1} {ฮฒ : Type u_5} [OrderedSemiring ๐] [] [] [Module ๐ ฮฒ] [OrderedSMul ๐ ฮฒ] (r : ฮฒ) (s : ฮฒ) :
StrictConvex ๐ (Set.Ioc r s)
theorem strictConvex_uIcc {๐ : Type u_1} {ฮฒ : Type u_5} [OrderedSemiring ๐] [] [] [Module ๐ ฮฒ] [OrderedSMul ๐ ฮฒ] (r : ฮฒ) (s : ฮฒ) :
StrictConvex ๐ (Set.uIcc r s)
theorem strictConvex_uIoc {๐ : Type u_1} {ฮฒ : Type u_5} [OrderedSemiring ๐] [] [] [Module ๐ ฮฒ] [OrderedSMul ๐ ฮฒ] (r : ฮฒ) (s : ฮฒ) :
StrictConvex ๐ (ฮ r s)
theorem StrictConvex.preimage_add_right {๐ : Type u_1} {E : Type u_3} [OrderedSemiring ๐] [] [] [Module ๐ E] {s : Set E} (hs : StrictConvex ๐ s) (z : E) :
StrictConvex ๐ ((fun (x : E) => z + x) โปยน' s)

The translation of a strictly convex set is also strictly convex.

theorem StrictConvex.preimage_add_left {๐ : Type u_1} {E : Type u_3} [OrderedSemiring ๐] [] [] [Module ๐ E] {s : Set E} (hs : StrictConvex ๐ s) (z : E) :
StrictConvex ๐ ((fun (x : E) => x + z) โปยน' s)

The translation of a strictly convex set is also strictly convex.

theorem StrictConvex.add {๐ : Type u_1} {E : Type u_3} [OrderedSemiring ๐] [] [] [Module ๐ E] [] {s : Set E} {t : Set E} (hs : StrictConvex ๐ s) (ht : StrictConvex ๐ t) :
StrictConvex ๐ (s + t)
theorem StrictConvex.add_left {๐ : Type u_1} {E : Type u_3} [OrderedSemiring ๐] [] [] [Module ๐ E] [] {s : Set E} (hs : StrictConvex ๐ s) (z : E) :
StrictConvex ๐ ((fun (x : E) => z + x) '' s)
theorem StrictConvex.add_right {๐ : Type u_1} {E : Type u_3} [OrderedSemiring ๐] [] [] [Module ๐ E] [] {s : Set E} (hs : StrictConvex ๐ s) (z : E) :
StrictConvex ๐ ((fun (x : E) => x + z) '' s)
theorem StrictConvex.vadd {๐ : Type u_1} {E : Type u_3} [OrderedSemiring ๐] [] [] [Module ๐ E] [] {s : Set E} (hs : StrictConvex ๐ s) (x : E) :
StrictConvex ๐ (x +แตฅ s)

The translation of a strictly convex set is also strictly convex.

theorem StrictConvex.smul {๐ : Type u_1} {๐ : Type u_2} {E : Type u_3} [OrderedSemiring ๐] [] [] [Module ๐ E] [] [Module ๐ E] [ContinuousConstSMul ๐ E] [LinearMap.CompatibleSMul E E ๐ ๐] {s : Set E} (hs : StrictConvex ๐ s) (c : ๐) :
StrictConvex ๐ (c โข s)
theorem StrictConvex.affinity {๐ : Type u_1} {๐ : Type u_2} {E : Type u_3} [OrderedSemiring ๐] [] [] [Module ๐ E] [] [Module ๐ E] [ContinuousConstSMul ๐ E] [LinearMap.CompatibleSMul E E ๐ ๐] {s : Set E} [] (hs : StrictConvex ๐ s) (z : E) (c : ๐) :
StrictConvex ๐ (z +แตฅ c โข s)
theorem StrictConvex.preimage_smul {๐ : Type u_1} {E : Type u_3} [] [] [] [Module ๐ E] [NoZeroSMulDivisors ๐ E] [ContinuousConstSMul ๐ E] {s : Set E} (hs : StrictConvex ๐ s) (c : ๐) :
StrictConvex ๐ ((fun (z : E) => c โข z) โปยน' s)
theorem StrictConvex.eq_of_openSegment_subset_frontier {๐ : Type u_1} {E : Type u_3} [OrderedRing ๐] [] [] [Module ๐ E] {s : Set E} {x : E} {y : E} [Nontrivial ๐] [DenselyOrdered ๐] (hs : StrictConvex ๐ s) (hx : x โ s) (hy : y โ s) (h : openSegment ๐ x y โ ) :
x = y
theorem StrictConvex.add_smul_mem {๐ : Type u_1} {E : Type u_3} [OrderedRing ๐] [] [] [Module ๐ E] {s : Set E} {x : E} {y : E} (hs : StrictConvex ๐ s) (hx : x โ s) (hxy : x + y โ s) (hy : y โ  0) {t : ๐} (htโ : 0 < t) (htโ : t < 1) :
theorem StrictConvex.smul_mem_of_zero_mem {๐ : Type u_1} {E : Type u_3} [OrderedRing ๐] [] [] [Module ๐ E] {s : Set E} {x : E} (hs : StrictConvex ๐ s) (zero_mem : 0 โ s) (hx : x โ s) (hxโ : x โ  0) {t : ๐} (htโ : 0 < t) (htโ : t < 1) :
theorem StrictConvex.add_smul_sub_mem {๐ : Type u_1} {E : Type u_3} [OrderedRing ๐] [] [] [Module ๐ E] {s : Set E} {x : E} {y : E} (h : StrictConvex ๐ s) (hx : x โ s) (hy : y โ s) (hxy : x โ  y) {t : ๐} (htโ : 0 < t) (htโ : t < 1) :
x + t โข (y - x) โ
theorem StrictConvex.affine_preimage {๐ : Type u_1} {E : Type u_3} {F : Type u_4} [OrderedRing ๐] [] [] [] [] [Module ๐ E] [Module ๐ F] {s : Set F} (hs : StrictConvex ๐ s) {f : E โแต[๐] F} (hf : Continuous โf) (hfinj : ) :
StrictConvex ๐ (โf โปยน' s)

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

theorem StrictConvex.affine_image {๐ : Type u_1} {E : Type u_3} {F : Type u_4} [OrderedRing ๐] [] [] [] [] [Module ๐ E] [Module ๐ F] {s : Set E} (hs : StrictConvex ๐ s) {f : E โแต[๐] F} (hf : IsOpenMap โf) :
StrictConvex ๐ (โf '' s)

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

theorem StrictConvex.neg {๐ : Type u_1} {E : Type u_3} [OrderedRing ๐] [] [] [Module ๐ E] {s : Set E} (hs : StrictConvex ๐ s) :
StrictConvex ๐ (-s)
theorem StrictConvex.sub {๐ : Type u_1} {E : Type u_3} [OrderedRing ๐] [] [] [Module ๐ E] {s : Set E} {t : Set E} (hs : StrictConvex ๐ s) (ht : StrictConvex ๐ t) :
StrictConvex ๐ (s - t)
theorem strictConvex_iff_div {๐ : Type u_1} {E : Type u_3} [] [] [] [Module ๐ E] {s : Set E} :
StrictConvex ๐ s โ s.Pairwise fun (x y : E) => โ โฆa b : ๐โฆ, 0 < a โ 0 < b โ (a / (a + b)) โข x + (b / (a + b)) โข y โ

Alternative definition of set strict convexity, using division.

theorem StrictConvex.mem_smul_of_zero_mem {๐ : Type u_1} {E : Type u_3} [] [] [] [Module ๐ E] {s : Set E} {x : E} (hs : StrictConvex ๐ s) (zero_mem : 0 โ s) (hx : x โ s) (hxโ : x โ  0) {t : ๐} (ht : 1 < t) :

#### Convex sets in an ordered space #

Relates Convex and Set.OrdConnected.

@[simp]
theorem strictConvex_iff_convex {๐ : Type u_1} [] [TopologicalSpace ๐] [OrderTopology ๐] {s : Set ๐} :
StrictConvex ๐ s โ Convex ๐ s

A set in a linear ordered field is strictly convex if and only if it is convex.

theorem strictConvex_iff_ordConnected {๐ : Type u_1} [] [TopologicalSpace ๐] [OrderTopology ๐] {s : Set ๐} :
StrictConvex ๐ s โ s.OrdConnected
theorem StrictConvex.ordConnected {๐ : Type u_1} [] [TopologicalSpace ๐] [OrderTopology ๐] {s : Set ๐} :
StrictConvex ๐ s โ s.OrdConnected

Alias of the forward direction of strictConvex_iff_ordConnected.