analysis.convex.strict - mathlib docs

source

def strict_convex (𝕜 : Type u_1) {E : Type u_2} [ordered_semiring 𝕜] [topological_space E] [add_comm_monoid E] [has_scalar 𝕜 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

strict_convex 𝕜 s = s.pairwise (λ (x y : E), ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ interior s)

source

theorem strict_convex_iff_open_segment_subset {𝕜 : Type u_1} {E : Type u_2} [ordered_semiring 𝕜] [topological_space E] [add_comm_monoid E] [has_scalar 𝕜 E] {s : set E} :

strict_convex 𝕜 s ↔ s.pairwise (λ (x y : E), open_segment 𝕜 x y ⊆ interior s)

source

theorem strict_convex.open_segment_subset {𝕜 : Type u_1} {E : Type u_2} [ordered_semiring 𝕜] [topological_space E] [add_comm_monoid E] [has_scalar 𝕜 E] {s : set E} {x y : E} (hs : strict_convex 𝕜 s) (hx : x ∈ s) (hy : y ∈ s) (h : x ≠ y) :

open_segment 𝕜 x y ⊆ interior s

source

theorem strict_convex_empty {𝕜 : Type u_1} {E : Type u_2} [ordered_semiring 𝕜] [topological_space E] [add_comm_monoid E] [has_scalar 𝕜 E] :

strict_convex 𝕜 ∅

source

theorem strict_convex_univ {𝕜 : Type u_1} {E : Type u_2} [ordered_semiring 𝕜] [topological_space E] [add_comm_monoid E] [has_scalar 𝕜 E] :

strict_convex 𝕜 set.univ

source

@[protected]

theorem strict_convex.inter {𝕜 : Type u_1} {E : Type u_2} [ordered_semiring 𝕜] [topological_space E] [add_comm_monoid E] [has_scalar 𝕜 E] {s t : set E} (hs : strict_convex 𝕜 s) (ht : strict_convex 𝕜 t) :

strict_convex 𝕜 (s ∩ t)

source

theorem directed.strict_convex_Union {𝕜 : Type u_1} {E : Type u_2} [ordered_semiring 𝕜] [topological_space E] [add_comm_monoid E] [has_scalar 𝕜 E] {ι : Sort u_3} {s : ι → set E} (hdir : directed has_subset.subset s) (hs : ∀ ⦃i : ι⦄, strict_convex 𝕜 (s i)) :

strict_convex 𝕜 (⋃ (i : ι), s i)

source

theorem directed_on.strict_convex_sUnion {𝕜 : Type u_1} {E : Type u_2} [ordered_semiring 𝕜] [topological_space E] [add_comm_monoid E] [has_scalar 𝕜 E] {S : set (set E)} (hdir : directed_on has_subset.subset S) (hS : ∀ (s : set E), s ∈ S → strict_convex 𝕜 s) :

strict_convex 𝕜 (⋃₀S)

source

@[protected]

theorem strict_convex.convex {𝕜 : Type u_1} {E : Type u_2} [ordered_semiring 𝕜] [topological_space E] [add_comm_monoid E] [module 𝕜 E] {s : set E} (hs : strict_convex 𝕜 s) :

convex 𝕜 s

source

@[protected]

theorem convex.strict_convex {𝕜 : Type u_1} {E : Type u_2} [ordered_semiring 𝕜] [topological_space E] [add_comm_monoid E] [module 𝕜 E] {s : set E} (h : is_open s) (hs : convex 𝕜 s) :

strict_convex 𝕜 s

An open convex set is strictly convex.

source

theorem is_open.strict_convex_iff {𝕜 : Type u_1} {E : Type u_2} [ordered_semiring 𝕜] [topological_space E] [add_comm_monoid E] [module 𝕜 E] {s : set E} (h : is_open s) :

strict_convex 𝕜 s ↔ convex 𝕜 s

source

theorem strict_convex_singleton {𝕜 : Type u_1} {E : Type u_2} [ordered_semiring 𝕜] [topological_space E] [add_comm_monoid E] [module 𝕜 E] (c : E) :

strict_convex 𝕜 {c}

source

theorem set.subsingleton.strict_convex {𝕜 : Type u_1} {E : Type u_2} [ordered_semiring 𝕜] [topological_space E] [add_comm_monoid E] [module 𝕜 E] {s : set E} (hs : s.subsingleton) :

strict_convex 𝕜 s

source

theorem strict_convex.linear_image {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [ordered_semiring 𝕜] [topological_space E] [topological_space F] [add_comm_monoid E] [add_comm_monoid F] [module 𝕜 E] [module 𝕜 F] {s : set E} (hs : strict_convex 𝕜 s) (f : E →ₗ[𝕜] F) (hf : is_open_map ⇑f) :

strict_convex 𝕜 (⇑f '' s)

source

theorem strict_convex.is_linear_image {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [ordered_semiring 𝕜] [topological_space E] [topological_space F] [add_comm_monoid E] [add_comm_monoid F] [module 𝕜 E] [module 𝕜 F] {s : set E} (hs : strict_convex 𝕜 s) {f : E → F} (h : is_linear_map 𝕜 f) (hf : is_open_map f) :

strict_convex 𝕜 (f '' s)

source

theorem strict_convex.linear_preimage {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [ordered_semiring 𝕜] [topological_space E] [topological_space F] [add_comm_monoid E] [add_comm_monoid F] [module 𝕜 E] [module 𝕜 F] {s : set F} (hs : strict_convex 𝕜 s) (f : E →ₗ[𝕜] F) (hf : continuous ⇑f) (hfinj : function.injective ⇑f) :

strict_convex 𝕜 (⇑f ⁻¹' s)

source

theorem strict_convex.is_linear_preimage {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [ordered_semiring 𝕜] [topological_space E] [topological_space F] [add_comm_monoid E] [add_comm_monoid F] [module 𝕜 E] [module 𝕜 F] {s : set F} (hs : strict_convex 𝕜 s) {f : E → F} (h : is_linear_map 𝕜 f) (hf : continuous f) (hfinj : function.injective f) :

strict_convex 𝕜 (f ⁻¹' s)

source

theorem strict_convex_Iic {𝕜 : Type u_1} {β : Type u_4} [ordered_semiring 𝕜] [topological_space β] [linear_ordered_cancel_add_comm_monoid β] [order_topology β] [module 𝕜 β] [ordered_smul 𝕜 β] (r : β) :

strict_convex 𝕜 (set.Iic r)

source

theorem strict_convex_Ici {𝕜 : Type u_1} {β : Type u_4} [ordered_semiring 𝕜] [topological_space β] [linear_ordered_cancel_add_comm_monoid β] [order_topology β] [module 𝕜 β] [ordered_smul 𝕜 β] (r : β) :

strict_convex 𝕜 (set.Ici r)

source

theorem strict_convex_Icc {𝕜 : Type u_1} {β : Type u_4} [ordered_semiring 𝕜] [topological_space β] [linear_ordered_cancel_add_comm_monoid β] [order_topology β] [module 𝕜 β] [ordered_smul 𝕜 β] (r s : β) :

strict_convex 𝕜 (set.Icc r s)

source

theorem strict_convex_Iio {𝕜 : Type u_1} {β : Type u_4} [ordered_semiring 𝕜] [topological_space β] [linear_ordered_cancel_add_comm_monoid β] [order_topology β] [module 𝕜 β] [ordered_smul 𝕜 β] (r : β) :

strict_convex 𝕜 (set.Iio r)

source

theorem strict_convex_Ioi {𝕜 : Type u_1} {β : Type u_4} [ordered_semiring 𝕜] [topological_space β] [linear_ordered_cancel_add_comm_monoid β] [order_topology β] [module 𝕜 β] [ordered_smul 𝕜 β] (r : β) :

strict_convex 𝕜 (set.Ioi r)

source

theorem strict_convex_Ioo {𝕜 : Type u_1} {β : Type u_4} [ordered_semiring 𝕜] [topological_space β] [linear_ordered_cancel_add_comm_monoid β] [order_topology β] [module 𝕜 β] [ordered_smul 𝕜 β] (r s : β) :

strict_convex 𝕜 (set.Ioo r s)

source

theorem strict_convex_Ico {𝕜 : Type u_1} {β : Type u_4} [ordered_semiring 𝕜] [topological_space β] [linear_ordered_cancel_add_comm_monoid β] [order_topology β] [module 𝕜 β] [ordered_smul 𝕜 β] (r s : β) :

strict_convex 𝕜 (set.Ico r s)

source

theorem strict_convex_Ioc {𝕜 : Type u_1} {β : Type u_4} [ordered_semiring 𝕜] [topological_space β] [linear_ordered_cancel_add_comm_monoid β] [order_topology β] [module 𝕜 β] [ordered_smul 𝕜 β] (r s : β) :

strict_convex 𝕜 (set.Ioc r s)

source

theorem strict_convex_interval {𝕜 : Type u_1} {β : Type u_4} [ordered_semiring 𝕜] [topological_space β] [linear_ordered_cancel_add_comm_monoid β] [order_topology β] [module 𝕜 β] [ordered_smul 𝕜 β] (r s : β) :

strict_convex 𝕜 [r, s]

source

theorem strict_convex.preimage_add_right {𝕜 : Type u_1} {E : Type u_2} [ordered_semiring 𝕜] [topological_space E] [add_cancel_comm_monoid E] [has_continuous_add E] [module 𝕜 E] {s : set E} (hs : strict_convex 𝕜 s) (z : E) :

strict_convex 𝕜 ((λ (x : E), z + x) ⁻¹' s)

The translation of a strict_convex set is also strict_convex.

source

theorem strict_convex.preimage_add_left {𝕜 : Type u_1} {E : Type u_2} [ordered_semiring 𝕜] [topological_space E] [add_cancel_comm_monoid E] [has_continuous_add E] [module 𝕜 E] {s : set E} (hs : strict_convex 𝕜 s) (z : E) :

strict_convex 𝕜 ((λ (x : E), x + z) ⁻¹' s)

The translation of a strict_convex set is also strict_convex.

source

theorem strict_convex.add_left {𝕜 : Type u_1} {E : Type u_2} [ordered_semiring 𝕜] [topological_space E] [add_comm_group E] [module 𝕜 E] {s : set E} [has_continuous_add E] (hs : strict_convex 𝕜 s) (z : E) :

strict_convex 𝕜 ((λ (x : E), z + x) '' s)

source

theorem strict_convex.add_right {𝕜 : Type u_1} {E : Type u_2} [ordered_semiring 𝕜] [topological_space E] [add_comm_group E] [module 𝕜 E] {s : set E} [has_continuous_add E] (hs : strict_convex 𝕜 s) (z : E) :

strict_convex 𝕜 ((λ (x : E), x + z) '' s)

source

theorem strict_convex.add {𝕜 : Type u_1} {E : Type u_2} [ordered_semiring 𝕜] [topological_space E] [add_comm_group E] [module 𝕜 E] {s : set E} [has_continuous_add E] {t : set E} (hs : strict_convex 𝕜 s) (ht : strict_convex 𝕜 t) :

strict_convex 𝕜 (s + t)

source

theorem strict_convex.preimage_smul {𝕜 : Type u_1} {E : Type u_2} [ordered_comm_semiring 𝕜] [topological_space 𝕜] [topological_space E] [add_comm_group E] [module 𝕜 E] [no_zero_smul_divisors 𝕜 E] [has_continuous_smul 𝕜 E] {s : set E} (hs : strict_convex 𝕜 s) (c : 𝕜) :

strict_convex 𝕜 ((λ (z : E), c • z) ⁻¹' s)

source

theorem strict_convex.eq_of_open_segment_subset_frontier {𝕜 : Type u_1} {E : Type u_2} [ordered_ring 𝕜] [topological_space E] [add_comm_group E] [module 𝕜 E] {s : set E} {x y : E} [nontrivial 𝕜] [densely_ordered 𝕜] (hs : strict_convex 𝕜 s) (hx : x ∈ s) (hy : y ∈ s) (h : open_segment 𝕜 x y ⊆ frontier s) :

x = y

source

theorem strict_convex.add_smul_mem {𝕜 : Type u_1} {E : Type u_2} [ordered_ring 𝕜] [topological_space E] [add_comm_group E] [module 𝕜 E] {s : set E} {x y : E} (hs : strict_convex 𝕜 s) (hx : x ∈ s) (hxy : x + y ∈ s) (hy : y ≠ 0) {t : 𝕜} (ht₀ : 0 < t) (ht₁ : t < 1) :

x + t • y ∈ interior s

source

theorem strict_convex.smul_mem_of_zero_mem {𝕜 : Type u_1} {E : Type u_2} [ordered_ring 𝕜] [topological_space E] [add_comm_group E] [module 𝕜 E] {s : set E} {x : E} (hs : strict_convex 𝕜 s) (zero_mem : 0 ∈ s) (hx : x ∈ s) (hx₀ : x ≠ 0) {t : 𝕜} (ht₀ : 0 < t) (ht₁ : t < 1) :

t • x ∈ interior s

source

theorem strict_convex.add_smul_sub_mem {𝕜 : Type u_1} {E : Type u_2} [ordered_ring 𝕜] [topological_space E] [add_comm_group E] [module 𝕜 E] {s : set E} {x y : E} (h : strict_convex 𝕜 s) (hx : x ∈ s) (hy : y ∈ s) (hxy : x ≠ y) {t : 𝕜} (ht₀ : 0 < t) (ht₁ : t < 1) :

x + t • (y - x) ∈ interior s

source

theorem strict_convex.affine_preimage {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [ordered_ring 𝕜] [topological_space E] [topological_space F] [add_comm_group E] [add_comm_group F] [module 𝕜 E] [module 𝕜 F] {s : set F} (hs : strict_convex 𝕜 s) {f : E →ᵃ[𝕜] F} (hf : continuous ⇑f) (hfinj : function.injective ⇑f) :

strict_convex 𝕜 (⇑f ⁻¹' s)

The preimage of a strict_convex set under an affine map is strict_convex.

source

theorem strict_convex.affine_image {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [ordered_ring 𝕜] [topological_space E] [topological_space F] [add_comm_group E] [add_comm_group F] [module 𝕜 E] [module 𝕜 F] {s : set E} (hs : strict_convex 𝕜 s) {f : E →ᵃ[𝕜] F} (hf : is_open_map ⇑f) :

strict_convex 𝕜 (⇑f '' s)

The image of a strict_convex set under an affine map is strict_convex.

source

theorem strict_convex.neg {𝕜 : Type u_1} {E : Type u_2} [ordered_ring 𝕜] [topological_space E] [add_comm_group E] [module 𝕜 E] {s : set E} [topological_add_group E] (hs : strict_convex 𝕜 s) :

strict_convex 𝕜 ((λ (z : E), -z) '' s)

source

theorem strict_convex.neg_preimage {𝕜 : Type u_1} {E : Type u_2} [ordered_ring 𝕜] [topological_space E] [add_comm_group E] [module 𝕜 E] {s : set E} [topological_add_group E] (hs : strict_convex 𝕜 s) :

strict_convex 𝕜 ((λ (z : E), -z) ⁻¹' s)

source

theorem strict_convex.smul {𝕜 : Type u_1} {E : Type u_2} [linear_ordered_field 𝕜] [topological_space E] [add_comm_group E] [module 𝕜 E] {s : set E} [topological_space 𝕜] [has_continuous_smul 𝕜 E] (hs : strict_convex 𝕜 s) (c : 𝕜) :

strict_convex 𝕜 (c • s)

source

theorem strict_convex.affinity {𝕜 : Type u_1} {E : Type u_2} [linear_ordered_field 𝕜] [topological_space E] [add_comm_group E] [module 𝕜 E] {s : set E} [topological_space 𝕜] [has_continuous_add E] [has_continuous_smul 𝕜 E] (hs : strict_convex 𝕜 s) (z : E) (c : 𝕜) :

strict_convex 𝕜 ((λ (x : E), z + c • x) '' s)

source

theorem strict_convex_iff_div {𝕜 : Type u_1} {E : Type u_2} [linear_ordered_field 𝕜] [topological_space E] [add_comm_group E] [module 𝕜 E] {s : set E} :

strict_convex 𝕜 s ↔ s.pairwise (λ (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.

source

theorem strict_convex.mem_smul_of_zero_mem {𝕜 : Type u_1} {E : Type u_2} [linear_ordered_field 𝕜] [topological_space E] [add_comm_group E] [module 𝕜 E] {s : set E} {x : E} (hs : strict_convex 𝕜 s) (zero_mem : 0 ∈ s) (hx : x ∈ s) (hx₀ : x ≠ 0) {t : 𝕜} (ht : 1 < t) :

x ∈ t • interior s

source

@[simp]

theorem strict_convex_iff_convex {𝕜 : Type u_1} [linear_ordered_field 𝕜] [topological_space 𝕜] [order_topology 𝕜] {s : set 𝕜} :

strict_convex 𝕜 s ↔ convex 𝕜 s

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

source

theorem strict_convex_iff_ord_connected {𝕜 : Type u_1} [linear_ordered_field 𝕜] [topological_space 𝕜] [order_topology 𝕜] {s : set 𝕜} :

strict_convex 𝕜 s ↔ s.ord_connected

source

theorem strict_convex.ord_connected {𝕜 : Type u_1} [linear_ordered_field 𝕜] [topological_space 𝕜] [order_topology 𝕜] {s : set 𝕜} :

strict_convex 𝕜 s → s.ord_connected

Alias of strict_convex_iff_ord_connected.

mathlib documentation

Strictly convex sets #

TODO #

Convex sets in an ordered space #