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_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
theorem strict_convex_iff_open_segment_subset {๐•œ : Type u_1} {E : Type u_3} [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)
theorem strict_convex.open_segment_subset {๐•œ : Type u_1} {E : Type u_3} [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
theorem strict_convex_empty {๐•œ : Type u_1} {E : Type u_3} [ordered_semiring ๐•œ] [topological_space E] [add_comm_monoid E] [has_scalar ๐•œ E] :
theorem strict_convex_univ {๐•œ : Type u_1} {E : Type u_3} [ordered_semiring ๐•œ] [topological_space E] [add_comm_monoid E] [has_scalar ๐•œ E] :
@[protected]
theorem strict_convex.eq {๐•œ : Type u_1} {E : Type u_3} [ordered_semiring ๐•œ] [topological_space E] [add_comm_monoid E] [has_scalar ๐•œ 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_scalar ๐•œ 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_scalar ๐•œ 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_scalar ๐•œ 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 {๐•œ : 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) :
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_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_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_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_interval {๐•œ : 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.interval 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 : ๐•) :
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) :

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 ๐•œ} :
strict_convex ๐•œ s โ†’ s.ord_connected

Alias of the forward direction of strict_convex_iff_ord_connected`.