Strictly convex sets #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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".
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) :
open_segment 𝕜 x y ⊆ interior s
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) :
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) :
strict_convex 𝕜 (⇑f ⁻¹' s)
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) :
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) :
strict_convex 𝕜 (⇑f ⁻¹' s)
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} :
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 𝕜} :
strict_convex 𝕜 s ↔ s.ord_connected
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 the forward direction of strict_convex_iff_ord_connected.