mathlib documentation

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 strict_convex (π•œ : Type u_1) {E : Type u_3} [ordered_semiring π•œ] [topological_space E] [add_comm_monoid E] [has_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
theorem strict_convex_iff_open_segment_subset {π•œ : Type u_1} {E : Type u_3} [ordered_semiring π•œ] [topological_space E] [add_comm_monoid E] [has_smul π•œ E] {s : set E} :
strict_convex π•œ s ↔ s.pairwise (Ξ» (x y : E), open_segment π•œ x y βŠ† interior s)
theorem strict_convex.open_segment_subset {π•œ : Type u_1} {E : Type u_3} [ordered_semiring π•œ] [topological_space E] [add_comm_monoid E] [has_smul π•œ E] {s : set E} {x y : E} (hs : strict_convex π•œ s) (hx : x ∈ s) (hy : y ∈ s) (h : x β‰  y) :
theorem strict_convex_empty {π•œ : Type u_1} {E : Type u_3} [ordered_semiring π•œ] [topological_space E] [add_comm_monoid E] [has_smul π•œ E] :
theorem strict_convex_univ {π•œ : Type u_1} {E : Type u_3} [ordered_semiring π•œ] [topological_space E] [add_comm_monoid E] [has_smul π•œ E] :
@[protected]
theorem strict_convex.eq {π•œ : Type u_1} {E : Type u_3} [ordered_semiring π•œ] [topological_space E] [add_comm_monoid E] [has_smul π•œ E] {s : set E} {x y : E} {a b : π•œ} (hs : strict_convex π•œ 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
@[protected]
theorem strict_convex.inter {π•œ : Type u_1} {E : Type u_3} [ordered_semiring π•œ] [topological_space E] [add_comm_monoid E] [has_smul π•œ E] {s t : set E} (hs : strict_convex π•œ s) (ht : strict_convex π•œ t) :
strict_convex π•œ (s ∩ t)
theorem directed.strict_convex_Union {π•œ : Type u_1} {E : Type u_3} [ordered_semiring π•œ] [topological_space E] [add_comm_monoid E] [has_smul π•œ E] {ΞΉ : Sort u_2} {s : ΞΉ β†’ set E} (hdir : directed has_subset.subset s) (hs : βˆ€ ⦃i : ι⦄, strict_convex π•œ (s i)) :
strict_convex π•œ (⋃ (i : ΞΉ), s i)
theorem directed_on.strict_convex_sUnion {π•œ : Type u_1} {E : Type u_3} [ordered_semiring π•œ] [topological_space E] [add_comm_monoid E] [has_smul π•œ E] {S : set (set E)} (hdir : directed_on has_subset.subset S) (hS : βˆ€ (s : set E), s ∈ S β†’ strict_convex π•œ s) :
@[protected]
theorem strict_convex.convex {π•œ : Type u_1} {E : Type u_3} [ordered_semiring π•œ] [topological_space E] [add_comm_monoid E] [module π•œ E] {s : set E} (hs : strict_convex π•œ s) :
convex π•œ s
@[protected]
theorem convex.strict_convex_of_open {π•œ : Type u_1} {E : Type u_3} [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.

theorem is_open.strict_convex_iff {π•œ : Type u_1} {E : Type u_3} [ordered_semiring π•œ] [topological_space E] [add_comm_monoid E] [module π•œ E] {s : set E} (h : is_open s) :
strict_convex π•œ s ↔ convex π•œ s
theorem strict_convex_singleton {π•œ : Type u_1} {E : Type u_3} [ordered_semiring π•œ] [topological_space E] [add_comm_monoid E] [module π•œ E] (c : E) :
strict_convex π•œ {c}
theorem set.subsingleton.strict_convex {π•œ : Type u_1} {E : Type u_3} [ordered_semiring π•œ] [topological_space E] [add_comm_monoid E] [module π•œ E] {s : set E} (hs : s.subsingleton) :
strict_convex π•œ s
theorem strict_convex.linear_image {π•œ : Type u_1} {𝕝 : Type u_2} {E : Type u_3} {F : Type u_4} [ordered_semiring π•œ] [topological_space E] [topological_space F] [add_comm_monoid E] [add_comm_monoid F] [module π•œ E] [module π•œ F] {s : set E} [semiring 𝕝] [module 𝕝 E] [module 𝕝 F] [linear_map.compatible_smul E F π•œ 𝕝] (hs : strict_convex π•œ s) (f : E β†’β‚—[𝕝] F) (hf : is_open_map ⇑f) :
strict_convex π•œ (⇑f '' s)
theorem strict_convex.is_linear_image {π•œ : Type u_1} {E : Type u_3} {F : Type u_4} [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)
theorem strict_convex.linear_preimage {π•œ : Type u_1} {E : Type u_3} {F : Type u_4} [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) :
theorem strict_convex.is_linear_preimage {π•œ : Type u_1} {E : Type u_3} {F : Type u_4} [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)
@[protected]
theorem set.ord_connected.strict_convex {π•œ : Type u_1} {Ξ² : Type u_5} [ordered_semiring π•œ] [topological_space Ξ²] [linear_ordered_cancel_add_comm_monoid Ξ²] [order_topology Ξ²] [module π•œ Ξ²] [ordered_smul π•œ Ξ²] {s : set Ξ²} (hs : s.ord_connected) :
strict_convex π•œ s
theorem strict_convex_Iic {π•œ : Type u_1} {Ξ² : Type u_5} [ordered_semiring π•œ] [topological_space Ξ²] [linear_ordered_cancel_add_comm_monoid Ξ²] [order_topology Ξ²] [module π•œ Ξ²] [ordered_smul π•œ Ξ²] (r : Ξ²) :
strict_convex π•œ (set.Iic r)
theorem strict_convex_Ici {π•œ : Type u_1} {Ξ² : Type u_5} [ordered_semiring π•œ] [topological_space Ξ²] [linear_ordered_cancel_add_comm_monoid Ξ²] [order_topology Ξ²] [module π•œ Ξ²] [ordered_smul π•œ Ξ²] (r : Ξ²) :
strict_convex π•œ (set.Ici r)
theorem strict_convex_Iio {π•œ : Type u_1} {Ξ² : Type u_5} [ordered_semiring π•œ] [topological_space Ξ²] [linear_ordered_cancel_add_comm_monoid Ξ²] [order_topology Ξ²] [module π•œ Ξ²] [ordered_smul π•œ Ξ²] (r : Ξ²) :
strict_convex π•œ (set.Iio r)
theorem strict_convex_Ioi {π•œ : Type u_1} {Ξ² : Type u_5} [ordered_semiring π•œ] [topological_space Ξ²] [linear_ordered_cancel_add_comm_monoid Ξ²] [order_topology Ξ²] [module π•œ Ξ²] [ordered_smul π•œ Ξ²] (r : Ξ²) :
strict_convex π•œ (set.Ioi r)
theorem strict_convex_Icc {π•œ : Type u_1} {Ξ² : Type u_5} [ordered_semiring π•œ] [topological_space Ξ²] [linear_ordered_cancel_add_comm_monoid Ξ²] [order_topology Ξ²] [module π•œ Ξ²] [ordered_smul π•œ Ξ²] (r s : Ξ²) :
strict_convex π•œ (set.Icc r s)
theorem strict_convex_Ioo {π•œ : Type u_1} {Ξ² : Type u_5} [ordered_semiring π•œ] [topological_space Ξ²] [linear_ordered_cancel_add_comm_monoid Ξ²] [order_topology Ξ²] [module π•œ Ξ²] [ordered_smul π•œ Ξ²] (r s : Ξ²) :
strict_convex π•œ (set.Ioo r s)
theorem strict_convex_Ico {π•œ : Type u_1} {Ξ² : Type u_5} [ordered_semiring π•œ] [topological_space Ξ²] [linear_ordered_cancel_add_comm_monoid Ξ²] [order_topology Ξ²] [module π•œ Ξ²] [ordered_smul π•œ Ξ²] (r s : Ξ²) :
strict_convex π•œ (set.Ico r s)
theorem strict_convex_Ioc {π•œ : Type u_1} {Ξ² : Type u_5} [ordered_semiring π•œ] [topological_space Ξ²] [linear_ordered_cancel_add_comm_monoid Ξ²] [order_topology Ξ²] [module π•œ Ξ²] [ordered_smul π•œ Ξ²] (r s : Ξ²) :
strict_convex π•œ (set.Ioc r s)
theorem strict_convex_uIcc {π•œ : Type u_1} {Ξ² : Type u_5} [ordered_semiring π•œ] [topological_space Ξ²] [linear_ordered_cancel_add_comm_monoid Ξ²] [order_topology Ξ²] [module π•œ Ξ²] [ordered_smul π•œ Ξ²] (r s : Ξ²) :
strict_convex π•œ (set.uIcc r s)
theorem strict_convex_uIoc {π•œ : Type u_1} {Ξ² : Type u_5} [ordered_semiring π•œ] [topological_space Ξ²] [linear_ordered_cancel_add_comm_monoid Ξ²] [order_topology Ξ²] [module π•œ Ξ²] [ordered_smul π•œ Ξ²] (r s : Ξ²) :
strict_convex π•œ (set.uIoc r s)
theorem strict_convex.preimage_add_right {π•œ : Type u_1} {E : Type u_3} [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 strictly convex set is also strictly convex.

theorem strict_convex.preimage_add_left {π•œ : Type u_1} {E : Type u_3} [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 strictly convex set is also strictly convex.

theorem strict_convex.add {π•œ : Type u_1} {E : Type u_3} [ordered_semiring π•œ] [topological_space E] [add_comm_group E] [module π•œ E] [has_continuous_add E] {s t : set E} (hs : strict_convex π•œ s) (ht : strict_convex π•œ t) :
strict_convex π•œ (s + t)
theorem strict_convex.add_left {π•œ : Type u_1} {E : Type u_3} [ordered_semiring π•œ] [topological_space E] [add_comm_group E] [module π•œ E] [has_continuous_add E] {s : set E} (hs : strict_convex π•œ s) (z : E) :
strict_convex π•œ ((Ξ» (x : E), z + x) '' s)
theorem strict_convex.add_right {π•œ : Type u_1} {E : Type u_3} [ordered_semiring π•œ] [topological_space E] [add_comm_group E] [module π•œ E] [has_continuous_add E] {s : set E} (hs : strict_convex π•œ s) (z : E) :
strict_convex π•œ ((Ξ» (x : E), x + z) '' s)
theorem strict_convex.vadd {π•œ : Type u_1} {E : Type u_3} [ordered_semiring π•œ] [topological_space E] [add_comm_group E] [module π•œ E] [has_continuous_add E] {s : set E} (hs : strict_convex π•œ s) (x : E) :
strict_convex π•œ (x +α΅₯ s)

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

theorem strict_convex.smul {π•œ : Type u_1} {𝕝 : Type u_2} {E : Type u_3} [ordered_semiring π•œ] [topological_space E] [add_comm_group E] [module π•œ E] [linear_ordered_field 𝕝] [module 𝕝 E] [has_continuous_const_smul 𝕝 E] [linear_map.compatible_smul E E π•œ 𝕝] {s : set E} (hs : strict_convex π•œ s) (c : 𝕝) :
strict_convex π•œ (c β€’ s)
theorem strict_convex.affinity {π•œ : Type u_1} {𝕝 : Type u_2} {E : Type u_3} [ordered_semiring π•œ] [topological_space E] [add_comm_group E] [module π•œ E] [linear_ordered_field 𝕝] [module 𝕝 E] [has_continuous_const_smul 𝕝 E] [linear_map.compatible_smul E E π•œ 𝕝] {s : set E} [has_continuous_add E] (hs : strict_convex π•œ s) (z : E) (c : 𝕝) :
strict_convex π•œ (z +α΅₯ c β€’ s)
theorem strict_convex.preimage_smul {π•œ : Type u_1} {E : Type u_3} [ordered_comm_semiring π•œ] [topological_space E] [add_comm_group E] [module π•œ E] [no_zero_smul_divisors π•œ E] [has_continuous_const_smul π•œ E] {s : set E} (hs : strict_convex π•œ s) (c : π•œ) :
strict_convex π•œ ((Ξ» (z : E), c β€’ z) ⁻¹' s)
theorem strict_convex.eq_of_open_segment_subset_frontier {π•œ : Type u_1} {E : Type u_3} [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
theorem strict_convex.add_smul_mem {π•œ : Type u_1} {E : Type u_3} [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) :
theorem strict_convex.smul_mem_of_zero_mem {π•œ : Type u_1} {E : Type u_3} [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) :
theorem strict_convex.add_smul_sub_mem {π•œ : Type u_1} {E : Type u_3} [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
theorem strict_convex.affine_preimage {π•œ : Type u_1} {E : Type u_3} {F : Type u_4} [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) :

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

theorem strict_convex.affine_image {π•œ : Type u_1} {E : Type u_3} {F : Type u_4} [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 strictly convex set under an affine map is strictly convex.

theorem strict_convex.neg {π•œ : Type u_1} {E : Type u_3} [ordered_ring π•œ] [topological_space E] [add_comm_group E] [module π•œ E] {s : set E} [topological_add_group E] (hs : strict_convex π•œ s) :
strict_convex π•œ (-s)
theorem strict_convex.sub {π•œ : Type u_1} {E : Type u_3} [ordered_ring π•œ] [topological_space E] [add_comm_group E] [module π•œ E] {s t : set E} [topological_add_group E] (hs : strict_convex π•œ s) (ht : strict_convex π•œ t) :
strict_convex π•œ (s - t)
theorem strict_convex_iff_div {π•œ : Type u_1} {E : Type u_3} [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.

theorem strict_convex.mem_smul_of_zero_mem {π•œ : Type u_1} {E : Type u_3} [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) :

Convex sets in an ordered space #

Relates convex and set.ord_connected.

@[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.

theorem strict_convex_iff_ord_connected {π•œ : Type u_1} [linear_ordered_field π•œ] [topological_space π•œ] [order_topology π•œ] {s : set π•œ} :
theorem strict_convex.ord_connected {π•œ : Type u_1} [linear_ordered_field π•œ] [topological_space π•œ] [order_topology π•œ] {s : set π•œ} :

Alias of the forward direction of strict_convex_iff_ord_connected.