Documentation

Mathlib.Analysis.Convex.Strict

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) :

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 ๐•œ] [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] :
    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) :
    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) :
    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) :
    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) :
    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) :
    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) :

    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.