analysis.convex.basic - mathlib docs

source

def segment (𝕜 : Type u_1) {E : Type u_2} [ordered_semiring 𝕜] [add_comm_monoid E] [has_scalar 𝕜 E] (x y : E) :

set E

Segments in a vector space.

Equations

segment 𝕜 x y = {z : E | ∃ (a b : 𝕜) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1), a • x + b • y = z}

source

def open_segment (𝕜 : Type u_1) {E : Type u_2} [ordered_semiring 𝕜] [add_comm_monoid E] [has_scalar 𝕜 E] (x y : E) :

set E

Open segment in a vector space. Note that open_segment 𝕜 x x = {x} instead of being ∅ when the base semiring has some element between 0 and 1.

Equations

open_segment 𝕜 x y = {z : E | ∃ (a b : 𝕜) (ha : 0 < a) (hb : 0 < b) (hab : a + b = 1), a • x + b • y = z}

source

theorem segment_eq_image₂ (𝕜 : Type u_1) {E : Type u_2} [ordered_semiring 𝕜] [add_comm_monoid E] [has_scalar 𝕜 E] (x y : E) :

segment 𝕜 x y = (λ (p : 𝕜 × 𝕜), p.fst • x + p.snd • y) '' {p : 𝕜 × 𝕜 | 0 ≤ p.fst ∧ 0 ≤ p.snd ∧ p.fst + p.snd = 1}

source

theorem open_segment_eq_image₂ (𝕜 : Type u_1) {E : Type u_2} [ordered_semiring 𝕜] [add_comm_monoid E] [has_scalar 𝕜 E] (x y : E) :

open_segment 𝕜 x y = (λ (p : 𝕜 × 𝕜), p.fst • x + p.snd • y) '' {p : 𝕜 × 𝕜 | 0 < p.fst ∧ 0 < p.snd ∧ p.fst + p.snd = 1}

source

theorem segment_symm (𝕜 : Type u_1) {E : Type u_2} [ordered_semiring 𝕜] [add_comm_monoid E] [has_scalar 𝕜 E] (x y : E) :

segment 𝕜 x y = segment 𝕜 y x

source

theorem open_segment_symm (𝕜 : Type u_1) {E : Type u_2} [ordered_semiring 𝕜] [add_comm_monoid E] [has_scalar 𝕜 E] (x y : E) :

open_segment 𝕜 x y = open_segment 𝕜 y x

source

theorem open_segment_subset_segment (𝕜 : Type u_1) {E : Type u_2} [ordered_semiring 𝕜] [add_comm_monoid E] [has_scalar 𝕜 E] (x y : E) :

open_segment 𝕜 x y ⊆ segment 𝕜 x y

source

theorem segment_subset_iff (𝕜 : Type u_1) {E : Type u_2} [ordered_semiring 𝕜] [add_comm_monoid E] [has_scalar 𝕜 E] {x y : E} {s : set E} :

segment 𝕜 x y ⊆ s ↔ ∀ (a b : 𝕜), 0 ≤ a → 0 ≤ b → a + b = 1 → a • x + b • y ∈ s

source

theorem open_segment_subset_iff (𝕜 : Type u_1) {E : Type u_2} [ordered_semiring 𝕜] [add_comm_monoid E] [has_scalar 𝕜 E] {x y : E} {s : set E} :

open_segment 𝕜 x y ⊆ s ↔ ∀ (a b : 𝕜), 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s

source

theorem left_mem_segment (𝕜 : Type u_1) {E : Type u_2} [ordered_semiring 𝕜] [add_comm_monoid E] [mul_action_with_zero 𝕜 E] (x y : E) :

x ∈ segment 𝕜 x y

source

theorem right_mem_segment (𝕜 : Type u_1) {E : Type u_2} [ordered_semiring 𝕜] [add_comm_monoid E] [mul_action_with_zero 𝕜 E] (x y : E) :

y ∈ segment 𝕜 x y

source

@[simp]

theorem segment_same (𝕜 : Type u_1) {E : Type u_2} [ordered_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] (x : E) :

segment 𝕜 x x = {x}

source

theorem insert_endpoints_open_segment (𝕜 : Type u_1) {E : Type u_2} [ordered_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] (x y : E) :

has_insert.insert x (has_insert.insert y (open_segment 𝕜 x y)) = segment 𝕜 x y

source

theorem mem_open_segment_of_ne_left_right {𝕜 : Type u_1} {E : Type u_2} [ordered_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] {x y z : E} (hx : x ≠ z) (hy : y ≠ z) (hz : z ∈ segment 𝕜 x y) :

z ∈ open_segment 𝕜 x y

source

theorem open_segment_subset_iff_segment_subset {𝕜 : Type u_1} {E : Type u_2} [ordered_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] {x y : E} {s : set E} (hx : x ∈ s) (hy : y ∈ s) :

open_segment 𝕜 x y ⊆ s ↔ segment 𝕜 x y ⊆ s

source

@[simp]

theorem open_segment_same (𝕜 : Type u_1) {E : Type u_2} [ordered_ring 𝕜] [add_comm_group E] [module 𝕜 E] [nontrivial 𝕜] [densely_ordered 𝕜] (x : E) :

open_segment 𝕜 x x = {x}

source

theorem segment_eq_image (𝕜 : Type u_1) {E : Type u_2} [ordered_ring 𝕜] [add_comm_group E] [module 𝕜 E] (x y : E) :

segment 𝕜 x y = (λ (θ : 𝕜), (1 - θ) • x + θ • y) '' set.Icc 0 1

source

theorem open_segment_eq_image (𝕜 : Type u_1) {E : Type u_2} [ordered_ring 𝕜] [add_comm_group E] [module 𝕜 E] (x y : E) :

open_segment 𝕜 x y = (λ (θ : 𝕜), (1 - θ) • x + θ • y) '' set.Ioo 0 1

source

theorem segment_eq_image' (𝕜 : Type u_1) {E : Type u_2} [ordered_ring 𝕜] [add_comm_group E] [module 𝕜 E] (x y : E) :

segment 𝕜 x y = (λ (θ : 𝕜), x + θ • (y - x)) '' set.Icc 0 1

source

theorem open_segment_eq_image' (𝕜 : Type u_1) {E : Type u_2} [ordered_ring 𝕜] [add_comm_group E] [module 𝕜 E] (x y : E) :

open_segment 𝕜 x y = (λ (θ : 𝕜), x + θ • (y - x)) '' set.Ioo 0 1

source

theorem segment_eq_image_line_map (𝕜 : Type u_1) {E : Type u_2} [ordered_ring 𝕜] [add_comm_group E] [module 𝕜 E] (x y : E) :

segment 𝕜 x y = ⇑(affine_map.line_map x y) '' set.Icc 0 1

source

theorem open_segment_eq_image_line_map (𝕜 : Type u_1) {E : Type u_2} [ordered_ring 𝕜] [add_comm_group E] [module 𝕜 E] (x y : E) :

open_segment 𝕜 x y = ⇑(affine_map.line_map x y) '' set.Ioo 0 1

source

theorem segment_image (𝕜 : Type u_1) {E : Type u_2} {F : Type u_3} [ordered_ring 𝕜] [add_comm_group E] [add_comm_group F] [module 𝕜 E] [module 𝕜 F] (f : E →ₗ[𝕜] F) (a b : E) :

⇑f '' segment 𝕜 a b = segment 𝕜 (⇑f a) (⇑f b)

source

@[simp]

theorem open_segment_image (𝕜 : Type u_1) {E : Type u_2} {F : Type u_3} [ordered_ring 𝕜] [add_comm_group E] [add_comm_group F] [module 𝕜 E] [module 𝕜 F] (f : E →ₗ[𝕜] F) (a b : E) :

⇑f '' open_segment 𝕜 a b = open_segment 𝕜 (⇑f a) (⇑f b)

source

theorem mem_segment_translate (𝕜 : Type u_1) {E : Type u_2} [ordered_ring 𝕜] [add_comm_group E] [module 𝕜 E] (a : E) {x b c : E} :

a + x ∈ segment 𝕜 (a + b) (a + c) ↔ x ∈ segment 𝕜 b c

source

@[simp]

theorem mem_open_segment_translate (𝕜 : Type u_1) {E : Type u_2} [ordered_ring 𝕜] [add_comm_group E] [module 𝕜 E] (a : E) {x b c : E} :

a + x ∈ open_segment 𝕜 (a + b) (a + c) ↔ x ∈ open_segment 𝕜 b c

source

theorem segment_translate_preimage (𝕜 : Type u_1) {E : Type u_2} [ordered_ring 𝕜] [add_comm_group E] [module 𝕜 E] (a b c : E) :

(λ (x : E), a + x) ⁻¹' segment 𝕜 (a + b) (a + c) = segment 𝕜 b c

source

theorem open_segment_translate_preimage (𝕜 : Type u_1) {E : Type u_2} [ordered_ring 𝕜] [add_comm_group E] [module 𝕜 E] (a b c : E) :

(λ (x : E), a + x) ⁻¹' open_segment 𝕜 (a + b) (a + c) = open_segment 𝕜 b c

source

theorem segment_translate_image (𝕜 : Type u_1) {E : Type u_2} [ordered_ring 𝕜] [add_comm_group E] [module 𝕜 E] (a b c : E) :

(λ (x : E), a + x) '' segment 𝕜 b c = segment 𝕜 (a + b) (a + c)

source

theorem open_segment_translate_image (𝕜 : Type u_1) {E : Type u_2} [ordered_ring 𝕜] [add_comm_group E] [module 𝕜 E] (a b c : E) :

(λ (x : E), a + x) '' open_segment 𝕜 b c = open_segment 𝕜 (a + b) (a + c)

source

theorem same_ray_of_mem_segment {𝕜 : Type u_1} {E : Type u_2} [ordered_comm_ring 𝕜] [add_comm_group E] [module 𝕜 E] {x y z : E} (h : x ∈ segment 𝕜 y z) :

same_ray 𝕜 (x - y) (z - x)

source

theorem midpoint_mem_segment {𝕜 : Type u_1} {E : Type u_2} [linear_ordered_ring 𝕜] [add_comm_group E] [module 𝕜 E] [invertible 2] (x y : E) :

midpoint 𝕜 x y ∈ segment 𝕜 x y

source

theorem mem_segment_sub_add {𝕜 : Type u_1} {E : Type u_2} [linear_ordered_ring 𝕜] [add_comm_group E] [module 𝕜 E] [invertible 2] (x y : E) :

x ∈ segment 𝕜 (x - y) (x + y)

source

theorem mem_segment_add_sub {𝕜 : Type u_1} {E : Type u_2} [linear_ordered_ring 𝕜] [add_comm_group E] [module 𝕜 E] [invertible 2] (x y : E) :

x ∈ segment 𝕜 (x + y) (x - y)

source

@[simp]

theorem left_mem_open_segment_iff {𝕜 : Type u_1} {E : Type u_2} [linear_ordered_ring 𝕜] [add_comm_group E] [module 𝕜 E] [densely_ordered 𝕜] [no_zero_smul_divisors 𝕜 E] {x y : E} :

x ∈ open_segment 𝕜 x y ↔ x = y

source

@[simp]

theorem right_mem_open_segment_iff {𝕜 : Type u_1} {E : Type u_2} [linear_ordered_ring 𝕜] [add_comm_group E] [module 𝕜 E] [densely_ordered 𝕜] [no_zero_smul_divisors 𝕜 E] {x y : E} :

y ∈ open_segment 𝕜 x y ↔ x = y

source

theorem mem_segment_iff_same_ray {𝕜 : Type u_1} {E : Type u_2} [linear_ordered_field 𝕜] [add_comm_group E] [module 𝕜 E] {x y z : E} :

x ∈ segment 𝕜 y z ↔ same_ray 𝕜 (x - y) (z - x)

source

theorem mem_segment_iff_div {𝕜 : Type u_1} {E : Type u_2} [linear_ordered_field 𝕜] [add_comm_group E] [module 𝕜 E] {x y z : E} :

x ∈ segment 𝕜 y z ↔ ∃ (a b : 𝕜), 0 ≤ a ∧ 0 ≤ b ∧ 0 < a + b ∧ (a / (a + b)) • y + (b / (a + b)) • z = x

source

theorem mem_open_segment_iff_div {𝕜 : Type u_1} {E : Type u_2} [linear_ordered_field 𝕜] [add_comm_group E] [module 𝕜 E] {x y z : E} :

x ∈ open_segment 𝕜 y z ↔ ∃ (a b : 𝕜), 0 < a ∧ 0 < b ∧ (a / (a + b)) • y + (b / (a + b)) • z = x

source

theorem segment_subset_Icc {𝕜 : Type u_1} {E : Type u_2} [ordered_semiring 𝕜] [ordered_add_comm_monoid E] [module 𝕜 E] [ordered_smul 𝕜 E] {x y : E} (h : x ≤ y) :

segment 𝕜 x y ⊆ set.Icc x y

source

theorem open_segment_subset_Ioo {𝕜 : Type u_1} {E : Type u_2} [ordered_semiring 𝕜] [ordered_cancel_add_comm_monoid E] [module 𝕜 E] [ordered_smul 𝕜 E] {x y : E} (h : x < y) :

open_segment 𝕜 x y ⊆ set.Ioo x y

source

theorem segment_subset_interval {𝕜 : Type u_1} {E : Type u_2} [ordered_semiring 𝕜] [linear_ordered_add_comm_monoid E] [module 𝕜 E] [ordered_smul 𝕜 E] (x y : E) :

segment 𝕜 x y ⊆ set.interval x y

source

theorem convex.min_le_combo {𝕜 : Type u_1} {E : Type u_2} [ordered_semiring 𝕜] [linear_ordered_add_comm_monoid E] [module 𝕜 E] [ordered_smul 𝕜 E] (x y : E) {a b : 𝕜} (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) :

linear_order.min x y ≤ a • x + b • y

source

theorem convex.combo_le_max {𝕜 : Type u_1} {E : Type u_2} [ordered_semiring 𝕜] [linear_ordered_add_comm_monoid E] [module 𝕜 E] [ordered_smul 𝕜 E] (x y : E) {a b : 𝕜} (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) :

a • x + b • y ≤ linear_order.max x y

source

theorem Icc_subset_segment {𝕜 : Type u_1} [linear_ordered_field 𝕜] {x y : 𝕜} :

set.Icc x y ⊆ segment 𝕜 x y

source

@[simp]

theorem segment_eq_Icc {𝕜 : Type u_1} [linear_ordered_field 𝕜] {x y : 𝕜} (h : x ≤ y) :

segment 𝕜 x y = set.Icc x y

source

theorem Ioo_subset_open_segment {𝕜 : Type u_1} [linear_ordered_field 𝕜] {x y : 𝕜} :

set.Ioo x y ⊆ open_segment 𝕜 x y

source

@[simp]

theorem open_segment_eq_Ioo {𝕜 : Type u_1} [linear_ordered_field 𝕜] {x y : 𝕜} (h : x < y) :

open_segment 𝕜 x y = set.Ioo x y

source

theorem segment_eq_Icc' {𝕜 : Type u_1} [linear_ordered_field 𝕜] (x y : 𝕜) :

segment 𝕜 x y = set.Icc (linear_order.min x y) (linear_order.max x y)

source

theorem open_segment_eq_Ioo' {𝕜 : Type u_1} [linear_ordered_field 𝕜] {x y : 𝕜} (hxy : x ≠ y) :

open_segment 𝕜 x y = set.Ioo (linear_order.min x y) (linear_order.max x y)

source

theorem segment_eq_interval {𝕜 : Type u_1} [linear_ordered_field 𝕜] (x y : 𝕜) :

segment 𝕜 x y = set.interval x y

source

theorem convex.mem_Icc {𝕜 : Type u_1} [linear_ordered_field 𝕜] {x y : 𝕜} (h : x ≤ y) {z : 𝕜} :

z ∈ set.Icc x y ↔ ∃ (a b : 𝕜), 0 ≤ a ∧ 0 ≤ b ∧ a + b = 1 ∧ a * x + b * y = z

A point is in an Icc iff it can be expressed as a convex combination of the endpoints.

source

theorem convex.mem_Ioo {𝕜 : Type u_1} [linear_ordered_field 𝕜] {x y : 𝕜} (h : x < y) {z : 𝕜} :

z ∈ set.Ioo x y ↔ ∃ (a b : 𝕜), 0 < a ∧ 0 < b ∧ a + b = 1 ∧ a * x + b * y = z

A point is in an Ioo iff it can be expressed as a strict convex combination of the endpoints.

source

theorem convex.mem_Ioc {𝕜 : Type u_1} [linear_ordered_field 𝕜] {x y : 𝕜} (h : x < y) {z : 𝕜} :

z ∈ set.Ioc x y ↔ ∃ (a b : 𝕜), 0 ≤ a ∧ 0 < b ∧ a + b = 1 ∧ a * x + b * y = z

A point is in an Ioc iff it can be expressed as a semistrict convex combination of the endpoints.

source

theorem convex.mem_Ico {𝕜 : Type u_1} [linear_ordered_field 𝕜] {x y : 𝕜} (h : x < y) {z : 𝕜} :

z ∈ set.Ico x y ↔ ∃ (a b : 𝕜), 0 < a ∧ 0 ≤ b ∧ a + b = 1 ∧ a * x + b * y = z

A point is in an Ico iff it can be expressed as a semistrict convex combination of the endpoints.

source

def convex (𝕜 : Type u_1) {E : Type u_2} [ordered_semiring 𝕜] [add_comm_monoid E] [has_scalar 𝕜 E] (s : set E) :

Prop

Convexity of sets.

Equations

convex 𝕜 s = ∀ ⦃x y : E⦄, x ∈ s → y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • x + b • y ∈ s

source

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

convex 𝕜 s ↔ ∀ ⦃x y : E⦄, x ∈ s → y ∈ s → segment 𝕜 x y ⊆ s

source

theorem convex.segment_subset {𝕜 : Type u_1} {E : Type u_2} [ordered_semiring 𝕜] [add_comm_monoid E] [has_scalar 𝕜 E] {s : set E} (h : convex 𝕜 s) {x y : E} (hx : x ∈ s) (hy : y ∈ s) :

segment 𝕜 x y ⊆ s

source

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

open_segment 𝕜 x y ⊆ s

source

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

convex 𝕜 s ↔ ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • s + b • s ⊆ s

Alternative definition of set convexity, in terms of pointwise set operations.

source

theorem convex.set_combo_subset {𝕜 : Type u_1} {E : Type u_2} [ordered_semiring 𝕜] [add_comm_monoid E] [has_scalar 𝕜 E] {s : set E} :

convex 𝕜 s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • s + b • s ⊆ s

Alias of the forward direction of convex_iff_pointwise_add_subset`.

source

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

convex 𝕜 ∅

source

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

convex 𝕜 set.univ

source

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

convex 𝕜 (s ∩ t)

source

theorem convex_sInter {𝕜 : Type u_1} {E : Type u_2} [ordered_semiring 𝕜] [add_comm_monoid E] [has_scalar 𝕜 E] {S : set (set E)} (h : ∀ (s : set E), s ∈ S → convex 𝕜 s) :

convex 𝕜 (⋂₀ S)

source

theorem convex_Inter {𝕜 : Type u_1} {E : Type u_2} [ordered_semiring 𝕜] [add_comm_monoid E] [has_scalar 𝕜 E] {ι : Sort u_3} {s : ι → set E} (h : ∀ (i : ι), convex 𝕜 (s i)) :

convex 𝕜 (⋂ (i : ι), s i)

source

theorem convex_Inter₂ {𝕜 : Type u_1} {E : Type u_2} [ordered_semiring 𝕜] [add_comm_monoid E] [has_scalar 𝕜 E] {ι : Sort u_3} {κ : ι → Sort u_4} {s : Π (i : ι), κ i → set E} (h : ∀ (i : ι) (j : κ i), convex 𝕜 (s i j)) :

convex 𝕜 (⋂ (i : ι) (j : κ i), s i j)

source

theorem convex.prod {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [ordered_semiring 𝕜] [add_comm_monoid E] [add_comm_monoid F] [has_scalar 𝕜 E] [has_scalar 𝕜 F] {s : set E} {t : set F} (hs : convex 𝕜 s) (ht : convex 𝕜 t) :

convex 𝕜 (s ×ˢ t)

source

theorem convex_pi {𝕜 : Type u_1} [ordered_semiring 𝕜] {ι : Type u_2} {E : ι → Type u_3} [Π (i : ι), add_comm_monoid (E i)] [Π (i : ι), has_scalar 𝕜 (E i)] {s : set ι} {t : Π (i : ι), set (E i)} (ht : ∀ (i : ι), convex 𝕜 (t i)) :

convex 𝕜 (s.pi t)

source

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

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

source

theorem directed_on.convex_sUnion {𝕜 : Type u_1} {E : Type u_2} [ordered_semiring 𝕜] [add_comm_monoid E] [has_scalar 𝕜 E] {c : set (set E)} (hdir : directed_on has_subset.subset c) (hc : ∀ ⦃A : set E⦄, A ∈ c → convex 𝕜 A) :

convex 𝕜 (⋃₀c)

source

theorem convex_iff_open_segment_subset {𝕜 : Type u_1} {E : Type u_2} [ordered_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] {s : set E} :

convex 𝕜 s ↔ ∀ ⦃x y : E⦄, x ∈ s → y ∈ s → open_segment 𝕜 x y ⊆ s

source

theorem convex_iff_forall_pos {𝕜 : Type u_1} {E : Type u_2} [ordered_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] {s : set E} :

convex 𝕜 s ↔ ∀ ⦃x y : E⦄, x ∈ s → y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s

source

theorem convex_iff_pairwise_pos {𝕜 : Type u_1} {E : Type u_2} [ordered_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] {s : set E} :

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

source

@[protected]

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

convex 𝕜 s

source

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

convex 𝕜 {c}

source

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

convex 𝕜 (⇑f '' s)

source

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

convex 𝕜 (f '' s)

source

theorem convex.linear_preimage {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [ordered_semiring 𝕜] [add_comm_monoid E] [add_comm_monoid F] [module 𝕜 E] [module 𝕜 F] {s : set F} (hs : convex 𝕜 s) (f : E →ₗ[𝕜] F) :

convex 𝕜 (⇑f ⁻¹' s)

source

theorem convex.is_linear_preimage {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [ordered_semiring 𝕜] [add_comm_monoid E] [add_comm_monoid F] [module 𝕜 E] [module 𝕜 F] {s : set F} (hs : convex 𝕜 s) {f : E → F} (hf : is_linear_map 𝕜 f) :

convex 𝕜 (f ⁻¹' s)

source

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

convex 𝕜 (s + t)

source

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

convex 𝕜 (z +ᵥ s)

source

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

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

source

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

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

The translation of a convex set is also convex.

source

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

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

The translation of a convex set is also convex.

source

theorem convex_Iic {𝕜 : Type u_1} {β : Type u_4} [ordered_semiring 𝕜] [ordered_add_comm_monoid β] [module 𝕜 β] [ordered_smul 𝕜 β] (r : β) :

convex 𝕜 (set.Iic r)

source

theorem convex_Ici {𝕜 : Type u_1} {β : Type u_4} [ordered_semiring 𝕜] [ordered_add_comm_monoid β] [module 𝕜 β] [ordered_smul 𝕜 β] (r : β) :

convex 𝕜 (set.Ici r)

source

theorem convex_Icc {𝕜 : Type u_1} {β : Type u_4} [ordered_semiring 𝕜] [ordered_add_comm_monoid β] [module 𝕜 β] [ordered_smul 𝕜 β] (r s : β) :

convex 𝕜 (set.Icc r s)

source

theorem convex_halfspace_le {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ordered_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] [ordered_add_comm_monoid β] [module 𝕜 β] [ordered_smul 𝕜 β] {f : E → β} (h : is_linear_map 𝕜 f) (r : β) :

convex 𝕜 {w : E | f w ≤ r}

source

theorem convex_halfspace_ge {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ordered_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] [ordered_add_comm_monoid β] [module 𝕜 β] [ordered_smul 𝕜 β] {f : E → β} (h : is_linear_map 𝕜 f) (r : β) :

convex 𝕜 {w : E | r ≤ f w}

source

theorem convex_hyperplane {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ordered_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] [ordered_add_comm_monoid β] [module 𝕜 β] [ordered_smul 𝕜 β] {f : E → β} (h : is_linear_map 𝕜 f) (r : β) :

convex 𝕜 {w : E | f w = r}

source

theorem convex_Iio {𝕜 : Type u_1} {β : Type u_4} [ordered_semiring 𝕜] [ordered_cancel_add_comm_monoid β] [module 𝕜 β] [ordered_smul 𝕜 β] (r : β) :

convex 𝕜 (set.Iio r)

source

theorem convex_Ioi {𝕜 : Type u_1} {β : Type u_4} [ordered_semiring 𝕜] [ordered_cancel_add_comm_monoid β] [module 𝕜 β] [ordered_smul 𝕜 β] (r : β) :

convex 𝕜 (set.Ioi r)

source

theorem convex_Ioo {𝕜 : Type u_1} {β : Type u_4} [ordered_semiring 𝕜] [ordered_cancel_add_comm_monoid β] [module 𝕜 β] [ordered_smul 𝕜 β] (r s : β) :

convex 𝕜 (set.Ioo r s)

source

theorem convex_Ico {𝕜 : Type u_1} {β : Type u_4} [ordered_semiring 𝕜] [ordered_cancel_add_comm_monoid β] [module 𝕜 β] [ordered_smul 𝕜 β] (r s : β) :

convex 𝕜 (set.Ico r s)

source

theorem convex_Ioc {𝕜 : Type u_1} {β : Type u_4} [ordered_semiring 𝕜] [ordered_cancel_add_comm_monoid β] [module 𝕜 β] [ordered_smul 𝕜 β] (r s : β) :

convex 𝕜 (set.Ioc r s)

source

theorem convex_halfspace_lt {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ordered_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] [ordered_cancel_add_comm_monoid β] [module 𝕜 β] [ordered_smul 𝕜 β] {f : E → β} (h : is_linear_map 𝕜 f) (r : β) :

convex 𝕜 {w : E | f w < r}

source

theorem convex_halfspace_gt {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ordered_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] [ordered_cancel_add_comm_monoid β] [module 𝕜 β] [ordered_smul 𝕜 β] {f : E → β} (h : is_linear_map 𝕜 f) (r : β) :

convex 𝕜 {w : E | r < f w}

source

theorem convex_interval {𝕜 : Type u_1} {β : Type u_4} [ordered_semiring 𝕜] [linear_ordered_add_comm_monoid β] [module 𝕜 β] [ordered_smul 𝕜 β] (r s : β) :

convex 𝕜 (set.interval r s)

source

theorem monotone_on.convex_le {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ordered_semiring 𝕜] [linear_ordered_add_comm_monoid E] [ordered_add_comm_monoid β] [module 𝕜 E] [ordered_smul 𝕜 E] {s : set E} {f : E → β} (hf : monotone_on f s) (hs : convex 𝕜 s) (r : β) :

convex 𝕜 {x ∈ s | f x ≤ r}

source

theorem monotone_on.convex_lt {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ordered_semiring 𝕜] [linear_ordered_add_comm_monoid E] [ordered_add_comm_monoid β] [module 𝕜 E] [ordered_smul 𝕜 E] {s : set E} {f : E → β} (hf : monotone_on f s) (hs : convex 𝕜 s) (r : β) :

convex 𝕜 {x ∈ s | f x < r}

source

theorem monotone_on.convex_ge {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ordered_semiring 𝕜] [linear_ordered_add_comm_monoid E] [ordered_add_comm_monoid β] [module 𝕜 E] [ordered_smul 𝕜 E] {s : set E} {f : E → β} (hf : monotone_on f s) (hs : convex 𝕜 s) (r : β) :

convex 𝕜 {x ∈ s | r ≤ f x}

source

theorem monotone_on.convex_gt {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ordered_semiring 𝕜] [linear_ordered_add_comm_monoid E] [ordered_add_comm_monoid β] [module 𝕜 E] [ordered_smul 𝕜 E] {s : set E} {f : E → β} (hf : monotone_on f s) (hs : convex 𝕜 s) (r : β) :

convex 𝕜 {x ∈ s | r < f x}

source

theorem antitone_on.convex_le {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ordered_semiring 𝕜] [linear_ordered_add_comm_monoid E] [ordered_add_comm_monoid β] [module 𝕜 E] [ordered_smul 𝕜 E] {s : set E} {f : E → β} (hf : antitone_on f s) (hs : convex 𝕜 s) (r : β) :

convex 𝕜 {x ∈ s | f x ≤ r}

source

theorem antitone_on.convex_lt {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ordered_semiring 𝕜] [linear_ordered_add_comm_monoid E] [ordered_add_comm_monoid β] [module 𝕜 E] [ordered_smul 𝕜 E] {s : set E} {f : E → β} (hf : antitone_on f s) (hs : convex 𝕜 s) (r : β) :

convex 𝕜 {x ∈ s | f x < r}

source

theorem antitone_on.convex_ge {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ordered_semiring 𝕜] [linear_ordered_add_comm_monoid E] [ordered_add_comm_monoid β] [module 𝕜 E] [ordered_smul 𝕜 E] {s : set E} {f : E → β} (hf : antitone_on f s) (hs : convex 𝕜 s) (r : β) :

convex 𝕜 {x ∈ s | r ≤ f x}

source

theorem antitone_on.convex_gt {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ordered_semiring 𝕜] [linear_ordered_add_comm_monoid E] [ordered_add_comm_monoid β] [module 𝕜 E] [ordered_smul 𝕜 E] {s : set E} {f : E → β} (hf : antitone_on f s) (hs : convex 𝕜 s) (r : β) :

convex 𝕜 {x ∈ s | r < f x}

source

theorem monotone.convex_le {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ordered_semiring 𝕜] [linear_ordered_add_comm_monoid E] [ordered_add_comm_monoid β] [module 𝕜 E] [ordered_smul 𝕜 E] {f : E → β} (hf : monotone f) (r : β) :

convex 𝕜 {x : E | f x ≤ r}

source

theorem monotone.convex_lt {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ordered_semiring 𝕜] [linear_ordered_add_comm_monoid E] [ordered_add_comm_monoid β] [module 𝕜 E] [ordered_smul 𝕜 E] {f : E → β} (hf : monotone f) (r : β) :

convex 𝕜 {x : E | f x ≤ r}

source

theorem monotone.convex_ge {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ordered_semiring 𝕜] [linear_ordered_add_comm_monoid E] [ordered_add_comm_monoid β] [module 𝕜 E] [ordered_smul 𝕜 E] {f : E → β} (hf : monotone f) (r : β) :

convex 𝕜 {x : E | r ≤ f x}

source

theorem monotone.convex_gt {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ordered_semiring 𝕜] [linear_ordered_add_comm_monoid E] [ordered_add_comm_monoid β] [module 𝕜 E] [ordered_smul 𝕜 E] {f : E → β} (hf : monotone f) (r : β) :

convex 𝕜 {x : E | f x ≤ r}

source

theorem antitone.convex_le {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ordered_semiring 𝕜] [linear_ordered_add_comm_monoid E] [ordered_add_comm_monoid β] [module 𝕜 E] [ordered_smul 𝕜 E] {f : E → β} (hf : antitone f) (r : β) :

convex 𝕜 {x : E | f x ≤ r}

source

theorem antitone.convex_lt {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ordered_semiring 𝕜] [linear_ordered_add_comm_monoid E] [ordered_add_comm_monoid β] [module 𝕜 E] [ordered_smul 𝕜 E] {f : E → β} (hf : antitone f) (r : β) :

convex 𝕜 {x : E | f x < r}

source

theorem antitone.convex_ge {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ordered_semiring 𝕜] [linear_ordered_add_comm_monoid E] [ordered_add_comm_monoid β] [module 𝕜 E] [ordered_smul 𝕜 E] {f : E → β} (hf : antitone f) (r : β) :

convex 𝕜 {x : E | r ≤ f x}

source

theorem antitone.convex_gt {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ordered_semiring 𝕜] [linear_ordered_add_comm_monoid E] [ordered_add_comm_monoid β] [module 𝕜 E] [ordered_smul 𝕜 E] {f : E → β} (hf : antitone f) (r : β) :

convex 𝕜 {x : E | r < f x}

source

theorem convex.combo_eq_vadd {𝕜 : Type u_1} {E : Type u_2} [ordered_semiring 𝕜] [add_comm_group E] [module 𝕜 E] {a b : 𝕜} {x y : E} (h : a + b = 1) :

a • x + b • y = b • (y - x) + x

source

theorem convex_segment {𝕜 : Type u_1} {E : Type u_2} [ordered_semiring 𝕜] [add_comm_group E] [module 𝕜 E] (x y : E) :

convex 𝕜 (segment 𝕜 x y)

source

theorem convex_open_segment {𝕜 : Type u_1} {E : Type u_2} [ordered_semiring 𝕜] [add_comm_group E] [module 𝕜 E] (a b : E) :

convex 𝕜 (open_segment 𝕜 a b)

source

theorem convex.smul {𝕜 : Type u_1} {E : Type u_2} [ordered_comm_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] {s : set E} (hs : convex 𝕜 s) (c : 𝕜) :

convex 𝕜 (c • s)

source

theorem convex.smul_preimage {𝕜 : Type u_1} {E : Type u_2} [ordered_comm_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] {s : set E} (hs : convex 𝕜 s) (c : 𝕜) :

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

source

theorem convex.affinity {𝕜 : Type u_1} {E : Type u_2} [ordered_comm_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] {s : set E} (hs : convex 𝕜 s) (z : E) (c : 𝕜) :

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

source

theorem convex.add_smul_mem {𝕜 : Type u_1} {E : Type u_2} [ordered_ring 𝕜] [add_comm_group E] [module 𝕜 E] {s : set E} (hs : convex 𝕜 s) {x y : E} (hx : x ∈ s) (hy : x + y ∈ s) {t : 𝕜} (ht : t ∈ set.Icc 0 1) :

x + t • y ∈ s

source

theorem convex.smul_mem_of_zero_mem {𝕜 : Type u_1} {E : Type u_2} [ordered_ring 𝕜] [add_comm_group E] [module 𝕜 E] {s : set E} (hs : convex 𝕜 s) {x : E} (zero_mem : 0 ∈ s) (hx : x ∈ s) {t : 𝕜} (ht : t ∈ set.Icc 0 1) :

t • x ∈ s

source

theorem convex.add_smul_sub_mem {𝕜 : Type u_1} {E : Type u_2} [ordered_ring 𝕜] [add_comm_group E] [module 𝕜 E] {s : set E} (h : convex 𝕜 s) {x y : E} (hx : x ∈ s) (hy : y ∈ s) {t : 𝕜} (ht : t ∈ set.Icc 0 1) :

x + t • (y - x) ∈ s

source

theorem affine_subspace.convex {𝕜 : Type u_1} {E : Type u_2} [ordered_ring 𝕜] [add_comm_group E] [module 𝕜 E] (Q : affine_subspace 𝕜 E) :

convex 𝕜 ↑Q

Affine subspaces are convex.

source

theorem convex.combo_affine_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [ordered_ring 𝕜] [add_comm_group E] [add_comm_group F] [module 𝕜 E] [module 𝕜 F] {a b : 𝕜} {x y : E} {f : E →ᵃ[𝕜] F} (h : a + b = 1) :

⇑f (a • x + b • y) = a • ⇑f x + b • ⇑f y

Applying an affine map to an affine combination of two points yields an affine combination of the images.

source

theorem convex.affine_preimage {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [ordered_ring 𝕜] [add_comm_group E] [add_comm_group F] [module 𝕜 E] [module 𝕜 F] (f : E →ᵃ[𝕜] F) {s : set F} (hs : convex 𝕜 s) :

convex 𝕜 (⇑f ⁻¹' s)

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

source

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

convex 𝕜 (⇑f '' s)

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

source

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

convex 𝕜 (-s)

source

theorem convex.sub {𝕜 : Type u_1} {E : Type u_2} [ordered_ring 𝕜] [add_comm_group E] [module 𝕜 E] {s t : set E} (hs : convex 𝕜 s) (ht : convex 𝕜 t) :

convex 𝕜 (s - t)

source

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

convex 𝕜 s ↔ ∀ ⦃x y : E⦄, x ∈ s → y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → 0 < a + b → (a / (a + b)) • x + (b / (a + b)) • y ∈ s

Alternative definition of set convexity, using division.

source

theorem convex.mem_smul_of_zero_mem {𝕜 : Type u_1} {E : Type u_2} [linear_ordered_field 𝕜] [add_comm_group E] [module 𝕜 E] {s : set E} (h : convex 𝕜 s) {x : E} (zero_mem : 0 ∈ s) (hx : x ∈ s) {t : 𝕜} (ht : 1 ≤ t) :

x ∈ t • s

source

theorem convex.add_smul {𝕜 : Type u_1} {E : Type u_2} [linear_ordered_field 𝕜] [add_comm_group E] [module 𝕜 E] {s : set E} (h_conv : convex 𝕜 s) {p q : 𝕜} (hp : 0 ≤ p) (hq : 0 ≤ q) :

(p + q) • s = p • s + q • s

source

theorem set.ord_connected.convex_of_chain {𝕜 : Type u_1} {E : Type u_2} [ordered_semiring 𝕜] [ordered_add_comm_monoid E] [module 𝕜 E] [ordered_smul 𝕜 E] {s : set E} (hs : s.ord_connected) (h : is_chain has_le.le s) :

convex 𝕜 s

source

theorem set.ord_connected.convex {𝕜 : Type u_1} {E : Type u_2} [ordered_semiring 𝕜] [linear_ordered_add_comm_monoid E] [module 𝕜 E] [ordered_smul 𝕜 E] {s : set E} (hs : s.ord_connected) :

convex 𝕜 s

source

theorem convex_iff_ord_connected {𝕜 : Type u_1} [linear_ordered_field 𝕜] {s : set 𝕜} :

convex 𝕜 s ↔ s.ord_connected

source

theorem convex.ord_connected {𝕜 : Type u_1} [linear_ordered_field 𝕜] {s : set 𝕜} :

convex 𝕜 s → s.ord_connected

Alias of the forward direction of convex_iff_ord_connected`.

source

theorem submodule.convex {𝕜 : Type u_1} {E : Type u_2} [ordered_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] (K : submodule 𝕜 E) :

convex 𝕜 ↑K

source

theorem subspace.convex {𝕜 : Type u_1} {E : Type u_2} [linear_ordered_field 𝕜] [add_comm_group E] [module 𝕜 E] (K : subspace 𝕜 E) :

convex 𝕜 ↑K

source

def std_simplex (𝕜 : Type u_1) (ι : Type u_5) [ordered_semiring 𝕜] [fintype ι] :

set (ι → 𝕜)

The standard simplex in the space of functions ι → 𝕜 is the set of vectors with non-negative coordinates with total sum 1. This is the free object in the category of convex spaces.

Equations

std_simplex 𝕜 ι = {f : ι → 𝕜 | (∀ (x : ι), 0 ≤ f x) ∧ finset.univ.sum (λ (x : ι), f x) = 1}

source

theorem std_simplex_eq_inter (𝕜 : Type u_1) (ι : Type u_5) [ordered_semiring 𝕜] [fintype ι] :

std_simplex 𝕜 ι = (⋂ (x : ι), {f : ι → 𝕜 | 0 ≤ f x}) ∩ {f : ι → 𝕜 | finset.univ.sum (λ (x : ι), f x) = 1}

source

theorem convex_std_simplex (𝕜 : Type u_1) (ι : Type u_5) [ordered_semiring 𝕜] [fintype ι] :

convex 𝕜 (std_simplex 𝕜 ι)

source

theorem ite_eq_mem_std_simplex (𝕜 : Type u_1) {ι : Type u_5} [ordered_semiring 𝕜] [fintype ι] (i : ι) :

(λ (j : ι), ite (i = j) 1 0) ∈ std_simplex 𝕜 ι

mathlib documentation

Convex sets and functions in vector spaces #

Notations #

TODO #

Segment #

Segments in an ordered space #

Convexity of sets #

Convex sets in an ordered space #

Convexity of submodules/subspaces #

Simplex #