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 𝕜] [TopologicalSpace E] [AddCommMonoid E] [SMul 𝕜 E] (s : Set E) : Prop

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

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

theorem strictConvex_iff_openSegment_subset {𝕜 : Type u_1} {E : Type u_3} [OrderedSemiring 𝕜] [TopologicalSpace E] [AddCommMonoid E] [SMul 𝕜 E] {s : Set E} : StrictConvex 𝕜 s ↔ s.Pairwise fun (x y : E) => openSegment 𝕜 x y ⊆ interior s

theorem StrictConvex.openSegment_subset {𝕜 : Type u_1} {E : Type u_3} [OrderedSemiring 𝕜] [TopologicalSpace E] [AddCommMonoid E] [SMul 𝕜 E] {s : Set E} {x y : E} (hs : StrictConvex 𝕜 s) (hx : x ∈ s) (hy : y ∈ s) (h : x ≠ y) : openSegment 𝕜 x y ⊆ interior s

theorem strictConvex_empty {𝕜 : Type u_1} {E : Type u_3} [OrderedSemiring 𝕜] [TopologicalSpace E] [AddCommMonoid E] [SMul 𝕜 E] : StrictConvex 𝕜 ∅

theorem strictConvex_univ {𝕜 : Type u_1} {E : Type u_3} [OrderedSemiring 𝕜] [TopologicalSpace E] [AddCommMonoid E] [SMul 𝕜 E] : StrictConvex 𝕜 Set.univ

theorem StrictConvex.eq {𝕜 : Type u_1} {E : Type u_3} [OrderedSemiring 𝕜] [TopologicalSpace E] [AddCommMonoid E] [SMul 𝕜 E] {s : Set E} {x 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 ∉ interior s) : x = y

theorem StrictConvex.inter {𝕜 : Type u_1} {E : Type u_3} [OrderedSemiring 𝕜] [TopologicalSpace E] [AddCommMonoid E] [SMul 𝕜 E] {s t : Set E} (hs : StrictConvex 𝕜 s) (ht : StrictConvex 𝕜 t) : StrictConvex 𝕜 (s ∩ t)

theorem Directed.strictConvex_iUnion {𝕜 : Type u_1} {E : Type u_3} [OrderedSemiring 𝕜] [TopologicalSpace E] [AddCommMonoid E] [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 𝕜] [TopologicalSpace E] [AddCommMonoid E] [SMul 𝕜 E] {S : Set (Set E)} (hdir : DirectedOn (fun (x1 x2 : Set E) => x1 ⊆ x2) S) (hS : ∀ s ∈ S, StrictConvex 𝕜 s) : StrictConvex 𝕜 (⋃₀ S)

theorem StrictConvex.convex {𝕜 : Type u_1} {E : Type u_3} [OrderedSemiring 𝕜] [TopologicalSpace E] [AddCommMonoid E] [Module 𝕜 E] {s : Set E} (hs : StrictConvex 𝕜 s) : Convex 𝕜 s

theorem Convex.strictConvex_of_isOpen {𝕜 : Type u_1} {E : Type u_3} [OrderedSemiring 𝕜] [TopologicalSpace E] [AddCommMonoid E] [Module 𝕜 E] {s : Set E} (h : IsOpen s) (hs : Convex 𝕜 s) : StrictConvex 𝕜 s

An open convex set is strictly convex.

theorem IsOpen.strictConvex_iff {𝕜 : Type u_1} {E : Type u_3} [OrderedSemiring 𝕜] [TopologicalSpace E] [AddCommMonoid E] [Module 𝕜 E] {s : Set E} (h : IsOpen s) : StrictConvex 𝕜 s ↔ Convex 𝕜 s

theorem strictConvex_singleton {𝕜 : Type u_1} {E : Type u_3} [OrderedSemiring 𝕜] [TopologicalSpace E] [AddCommMonoid E] [Module 𝕜 E] (c : E) : StrictConvex 𝕜 {c}

theorem Set.Subsingleton.strictConvex {𝕜 : Type u_1} {E : Type u_3} [OrderedSemiring 𝕜] [TopologicalSpace E] [AddCommMonoid E] [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 𝕜] [TopologicalSpace E] [TopologicalSpace F] [AddCommMonoid E] [AddCommMonoid F] [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 𝕜] [TopologicalSpace E] [TopologicalSpace F] [AddCommMonoid E] [AddCommMonoid F] [Module 𝕜 E] [Module 𝕜 F] {s : Set E} (hs : StrictConvex 𝕜 s) {f : E → F} (h : IsLinearMap 𝕜 f) (hf : IsOpenMap f) : StrictConvex 𝕜 (f '' s)

theorem StrictConvex.linear_preimage {𝕜 : Type u_1} {E : Type u_3} {F : Type u_4} [OrderedSemiring 𝕜] [TopologicalSpace E] [TopologicalSpace F] [AddCommMonoid E] [AddCommMonoid F] [Module 𝕜 E] [Module 𝕜 F] {s : Set F} (hs : StrictConvex 𝕜 s) (f : E →ₗ[𝕜] F) (hf : Continuous ⇑f) (hfinj : Function.Injective ⇑f) : StrictConvex 𝕜 (⇑f ⁻¹' s)

theorem StrictConvex.is_linear_preimage {𝕜 : Type u_1} {E : Type u_3} {F : Type u_4} [OrderedSemiring 𝕜] [TopologicalSpace E] [TopologicalSpace F] [AddCommMonoid E] [AddCommMonoid F] [Module 𝕜 E] [Module 𝕜 F] {s : Set F} (hs : StrictConvex 𝕜 s) {f : E → F} (h : IsLinearMap 𝕜 f) (hf : Continuous f) (hfinj : Function.Injective f) : StrictConvex 𝕜 (f ⁻¹' s)

theorem Set.OrdConnected.strictConvex {𝕜 : Type u_1} {β : Type u_5} [OrderedSemiring 𝕜] [TopologicalSpace β] [LinearOrderedCancelAddCommMonoid β] [OrderTopology β] [Module 𝕜 β] [OrderedSMul 𝕜 β] {s : Set β} (hs : s.OrdConnected) : StrictConvex 𝕜 s

theorem strictConvex_Iic {𝕜 : Type u_1} {β : Type u_5} [OrderedSemiring 𝕜] [TopologicalSpace β] [LinearOrderedCancelAddCommMonoid β] [OrderTopology β] [Module 𝕜 β] [OrderedSMul 𝕜 β] (r : β) : StrictConvex 𝕜 (Set.Iic r)

theorem strictConvex_Ici {𝕜 : Type u_1} {β : Type u_5} [OrderedSemiring 𝕜] [TopologicalSpace β] [LinearOrderedCancelAddCommMonoid β] [OrderTopology β] [Module 𝕜 β] [OrderedSMul 𝕜 β] (r : β) : StrictConvex 𝕜 (Set.Ici r)

theorem strictConvex_Iio {𝕜 : Type u_1} {β : Type u_5} [OrderedSemiring 𝕜] [TopologicalSpace β] [LinearOrderedCancelAddCommMonoid β] [OrderTopology β] [Module 𝕜 β] [OrderedSMul 𝕜 β] (r : β) : StrictConvex 𝕜 (Set.Iio r)

theorem strictConvex_Ioi {𝕜 : Type u_1} {β : Type u_5} [OrderedSemiring 𝕜] [TopologicalSpace β] [LinearOrderedCancelAddCommMonoid β] [OrderTopology β] [Module 𝕜 β] [OrderedSMul 𝕜 β] (r : β) : StrictConvex 𝕜 (Set.Ioi r)

theorem strictConvex_Icc {𝕜 : Type u_1} {β : Type u_5} [OrderedSemiring 𝕜] [TopologicalSpace β] [LinearOrderedCancelAddCommMonoid β] [OrderTopology β] [Module 𝕜 β] [OrderedSMul 𝕜 β] (r s : β) : StrictConvex 𝕜 (Set.Icc r s)

theorem strictConvex_Ioo {𝕜 : Type u_1} {β : Type u_5} [OrderedSemiring 𝕜] [TopologicalSpace β] [LinearOrderedCancelAddCommMonoid β] [OrderTopology β] [Module 𝕜 β] [OrderedSMul 𝕜 β] (r s : β) : StrictConvex 𝕜 (Set.Ioo r s)

theorem strictConvex_Ico {𝕜 : Type u_1} {β : Type u_5} [OrderedSemiring 𝕜] [TopologicalSpace β] [LinearOrderedCancelAddCommMonoid β] [OrderTopology β] [Module 𝕜 β] [OrderedSMul 𝕜 β] (r s : β) : StrictConvex 𝕜 (Set.Ico r s)

theorem strictConvex_Ioc {𝕜 : Type u_1} {β : Type u_5} [OrderedSemiring 𝕜] [TopologicalSpace β] [LinearOrderedCancelAddCommMonoid β] [OrderTopology β] [Module 𝕜 β] [OrderedSMul 𝕜 β] (r s : β) : StrictConvex 𝕜 (Set.Ioc r s)

theorem strictConvex_uIcc {𝕜 : Type u_1} {β : Type u_5} [OrderedSemiring 𝕜] [TopologicalSpace β] [LinearOrderedCancelAddCommMonoid β] [OrderTopology β] [Module 𝕜 β] [OrderedSMul 𝕜 β] (r s : β) : StrictConvex 𝕜 (Set.uIcc r s)

theorem strictConvex_uIoc {𝕜 : Type u_1} {β : Type u_5} [OrderedSemiring 𝕜] [TopologicalSpace β] [LinearOrderedCancelAddCommMonoid β] [OrderTopology β] [Module 𝕜 β] [OrderedSMul 𝕜 β] (r s : β) : StrictConvex 𝕜 (Ι r s)

theorem StrictConvex.preimage_add_right {𝕜 : Type u_1} {E : Type u_3} [OrderedSemiring 𝕜] [TopologicalSpace E] [AddCancelCommMonoid E] [ContinuousAdd E] [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 𝕜] [TopologicalSpace E] [AddCancelCommMonoid E] [ContinuousAdd E] [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 𝕜] [TopologicalSpace E] [AddCommGroup E] [Module 𝕜 E] [ContinuousAdd E] {s t : Set E} (hs : StrictConvex 𝕜 s) (ht : StrictConvex 𝕜 t) : StrictConvex 𝕜 (s + t)

theorem StrictConvex.add_left {𝕜 : Type u_1} {E : Type u_3} [OrderedSemiring 𝕜] [TopologicalSpace E] [AddCommGroup E] [Module 𝕜 E] [ContinuousAdd 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 𝕜] [TopologicalSpace E] [AddCommGroup E] [Module 𝕜 E] [ContinuousAdd 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 𝕜] [TopologicalSpace E] [AddCommGroup E] [Module 𝕜 E] [ContinuousAdd 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 𝕜] [TopologicalSpace E] [AddCommGroup E] [Module 𝕜 E] [LinearOrderedField 𝕝] [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 𝕜] [TopologicalSpace E] [AddCommGroup E] [Module 𝕜 E] [LinearOrderedField 𝕝] [Module 𝕝 E] [ContinuousConstSMul 𝕝 E] [LinearMap.CompatibleSMul E E 𝕜 𝕝] {s : Set E} [ContinuousAdd E] (hs : StrictConvex 𝕜 s) (z : E) (c : 𝕝) : StrictConvex 𝕜 (z +ᵥ c • s)

theorem StrictConvex.preimage_smul {𝕜 : Type u_1} {E : Type u_3} [OrderedCommSemiring 𝕜] [TopologicalSpace E] [AddCommGroup E] [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 𝕜] [TopologicalSpace E] [AddCommGroup E] [Module 𝕜 E] {s : Set E} {x y : E} [Nontrivial 𝕜] [DenselyOrdered 𝕜] (hs : StrictConvex 𝕜 s) (hx : x ∈ s) (hy : y ∈ s) (h : openSegment 𝕜 x y ⊆ frontier s) : x = y

theorem StrictConvex.add_smul_mem {𝕜 : Type u_1} {E : Type u_3} [OrderedRing 𝕜] [TopologicalSpace E] [AddCommGroup E] [Module 𝕜 E] {s : Set E} {x y : E} (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

theorem StrictConvex.smul_mem_of_zero_mem {𝕜 : Type u_1} {E : Type u_3} [OrderedRing 𝕜] [TopologicalSpace E] [AddCommGroup E] [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) : t • x ∈ interior s

theorem StrictConvex.add_smul_sub_mem {𝕜 : Type u_1} {E : Type u_3} [OrderedRing 𝕜] [TopologicalSpace E] [AddCommGroup E] [Module 𝕜 E] {s : Set E} {x 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) ∈ interior s

theorem StrictConvex.affine_preimage {𝕜 : Type u_1} {E : Type u_3} {F : Type u_4} [OrderedRing 𝕜] [TopologicalSpace E] [TopologicalSpace F] [AddCommGroup E] [AddCommGroup F] [Module 𝕜 E] [Module 𝕜 F] {s : Set F} (hs : StrictConvex 𝕜 s) {f : E →ᵃ[𝕜] F} (hf : Continuous ⇑f) (hfinj : Function.Injective ⇑f) : 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 𝕜] [TopologicalSpace E] [TopologicalSpace F] [AddCommGroup E] [AddCommGroup F] [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 𝕜] [TopologicalSpace E] [AddCommGroup E] [Module 𝕜 E] {s : Set E} [TopologicalAddGroup E] (hs : StrictConvex 𝕜 s) : StrictConvex 𝕜 (-s)

theorem StrictConvex.sub {𝕜 : Type u_1} {E : Type u_3} [OrderedRing 𝕜] [TopologicalSpace E] [AddCommGroup E] [Module 𝕜 E] {s t : Set E} [TopologicalAddGroup E] (hs : StrictConvex 𝕜 s) (ht : StrictConvex 𝕜 t) : StrictConvex 𝕜 (s - t)

theorem strictConvex_iff_div {𝕜 : Type u_1} {E : Type u_3} [LinearOrderedField 𝕜] [TopologicalSpace E] [AddCommGroup E] [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 ∈ interior s

Alternative definition of set strict convexity, using division.

theorem StrictConvex.mem_smul_of_zero_mem {𝕜 : Type u_1} {E : Type u_3} [LinearOrderedField 𝕜] [TopologicalSpace E] [AddCommGroup E] [Module 𝕜 E] {s : Set E} {x : E} (hs : StrictConvex 𝕜 s) (zero_mem : 0 ∈ s) (hx : x ∈ s) (hx₀ : x ≠ 0) {t : 𝕜} (ht : 1 < t) : x ∈ t • interior s

Convex sets in an ordered space

Relates Convex and Set.OrdConnected.

@[simp]

theorem strictConvex_iff_convex {𝕜 : Type u_1} [LinearOrderedField 𝕜] [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} [LinearOrderedField 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] {s : Set 𝕜} : StrictConvex 𝕜 s ↔ s.OrdConnected

theorem StrictConvex.ordConnected {𝕜 : Type u_1} [LinearOrderedField 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] {s : Set 𝕜} : StrictConvex 𝕜 s → s.OrdConnected

Alias of the forward direction of strictConvex_iff_ordConnected.