mathlib3 documentation

analysis.convex.segment

Segments in vector spaces #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In a π•œ-vector space, we define the following objects and properties.

Notations #

We provide the following notation:

TODO #

Generalize all this file to affine spaces.

Should we rename segment and open_segment to convex.Icc and convex.Ioo? Should we also define clopen_segment/convex.Ico/convex.Ioc?

def segment (π•œ : Type u_1) {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [has_smul π•œ E] (x y : E) :
set E

Segments in a vector space.

Equations
def open_segment (π•œ : Type u_1) {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [has_smul π•œ 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
theorem segment_eq_imageβ‚‚ (π•œ : Type u_1) {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [has_smul π•œ 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}
theorem open_segment_eq_imageβ‚‚ (π•œ : Type u_1) {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [has_smul π•œ 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}
theorem segment_symm (π•œ : Type u_1) {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [has_smul π•œ E] (x y : E) :
segment π•œ x y = segment π•œ y x
theorem open_segment_symm (π•œ : Type u_1) {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [has_smul π•œ E] (x y : E) :
open_segment π•œ x y = open_segment π•œ y x
theorem open_segment_subset_segment (π•œ : Type u_1) {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [has_smul π•œ E] (x y : E) :
open_segment π•œ x y βŠ† segment π•œ x y
theorem segment_subset_iff (π•œ : Type u_1) {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [has_smul π•œ E] {s : set E} {x y : E} :
segment π•œ x y βŠ† s ↔ βˆ€ (a b : π•œ), 0 ≀ a β†’ 0 ≀ b β†’ a + b = 1 β†’ a β€’ x + b β€’ y ∈ s
theorem open_segment_subset_iff (π•œ : Type u_1) {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [has_smul π•œ E] {s : set E} {x y : E} :
open_segment π•œ x y βŠ† s ↔ βˆ€ (a b : π•œ), 0 < a β†’ 0 < b β†’ a + b = 1 β†’ a β€’ x + b β€’ y ∈ s
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
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
@[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}
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
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
theorem open_segment_subset_iff_segment_subset {π•œ : Type u_1} {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [module π•œ E] {s : set E} {x y : E} (hx : x ∈ s) (hy : y ∈ s) :
open_segment π•œ x y βŠ† s ↔ segment π•œ x y βŠ† s
@[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}
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
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
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
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
theorem segment_eq_image_line_map (π•œ : Type u_1) {E : Type u_2} [ordered_ring π•œ] [add_comm_group E] [module π•œ E] (x y : E) :
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) :
@[simp]
theorem image_segment (π•œ : 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)
@[simp]
theorem image_open_segment (π•œ : 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)
@[simp]
theorem vadd_segment (π•œ : Type u_1) {E : Type u_2} {G : Type u_4} [ordered_ring π•œ] [add_comm_group E] [add_comm_group G] [module π•œ E] [add_torsor G E] [vadd_comm_class G E E] (a : G) (b c : E) :
a +α΅₯ segment π•œ b c = segment π•œ (a +α΅₯ b) (a +α΅₯ c)
@[simp]
theorem vadd_open_segment (π•œ : Type u_1) {E : Type u_2} {G : Type u_4} [ordered_ring π•œ] [add_comm_group E] [add_comm_group G] [module π•œ E] [add_torsor G E] [vadd_comm_class G E E] (a : G) (b c : E) :
a +α΅₯ open_segment π•œ b c = open_segment π•œ (a +α΅₯ b) (a +α΅₯ c)
@[simp]
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
@[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
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
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
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)
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)
theorem same_ray_of_mem_segment {π•œ : Type u_1} {E : Type u_2} [strict_ordered_comm_ring π•œ] [add_comm_group E] [module π•œ E] {x y z : E} (h : x ∈ segment π•œ y z) :
same_ray π•œ (x - y) (z - x)
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
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)
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)
@[simp]
theorem left_mem_open_segment_iff {π•œ : Type u_1} {E : Type u_2} [linear_ordered_ring π•œ] [add_comm_group E] [module π•œ E] {x y : E} [densely_ordered π•œ] [no_zero_smul_divisors π•œ E] :
x ∈ open_segment π•œ x y ↔ x = y
@[simp]
theorem right_mem_open_segment_iff {π•œ : Type u_1} {E : Type u_2} [linear_ordered_ring π•œ] [add_comm_group E] [module π•œ E] {x y : E} [densely_ordered π•œ] [no_zero_smul_divisors π•œ E] :
y ∈ open_segment π•œ x y ↔ x = y
theorem mem_segment_iff_div {π•œ : Type u_1} {E : Type u_2} [linear_ordered_semifield π•œ] [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
theorem mem_open_segment_iff_div {π•œ : Type u_1} {E : Type u_2} [linear_ordered_semifield π•œ] [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
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)
theorem open_segment_subset_union {π•œ : Type u_1} {E : Type u_2} [linear_ordered_field π•œ] [add_comm_group E] [module π•œ E] (x y : E) {z : E} (hz : z ∈ set.range ⇑(affine_map.line_map x y)) :
open_segment π•œ x y βŠ† has_insert.insert z (open_segment π•œ x z βˆͺ open_segment π•œ z y)

If z = line_map x y c is a point on the line passing through x and y, then the open segment open_segment π•œ x y is included in the union of the open segments open_segment π•œ x z, open_segment π•œ z y, and the point z. Informally, (x, y) βŠ† {z} βˆͺ (x, z) βˆͺ (z, y).

Segments in an ordered space #

Relates segment, open_segment and set.Icc, set.Ico, set.Ioc, set.Ioo

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
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
theorem segment_subset_uIcc {π•œ : 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.uIcc x y
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] {a b : π•œ} (x y : E) (ha : 0 ≀ a) (hb : 0 ≀ b) (hab : a + b = 1) :
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] {a b : π•œ} (x y : E) (ha : 0 ≀ a) (hb : 0 ≀ b) (hab : a + b = 1) :
theorem Icc_subset_segment {π•œ : Type u_1} [linear_ordered_field π•œ] {x y : π•œ} :
set.Icc x y βŠ† segment π•œ x y
@[simp]
theorem segment_eq_Icc {π•œ : Type u_1} [linear_ordered_field π•œ] {x y : π•œ} (h : x ≀ y) :
segment π•œ x y = set.Icc x y
theorem Ioo_subset_open_segment {π•œ : Type u_1} [linear_ordered_field π•œ] {x y : π•œ} :
set.Ioo x y βŠ† open_segment π•œ x y
@[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
theorem segment_eq_Icc' {π•œ : Type u_1} [linear_ordered_field π•œ] (x y : π•œ) :
theorem open_segment_eq_Ioo' {π•œ : Type u_1} [linear_ordered_field π•œ] {x y : π•œ} (hxy : x β‰  y) :
theorem segment_eq_uIcc {π•œ : Type u_1} [linear_ordered_field π•œ] (x y : π•œ) :
segment π•œ x y = set.uIcc x y
theorem convex.mem_Icc {π•œ : Type u_1} [linear_ordered_field π•œ] {x y z : π•œ} (h : x ≀ y) :
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.

theorem convex.mem_Ioo {π•œ : Type u_1} [linear_ordered_field π•œ] {x y z : π•œ} (h : x < y) :
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.

theorem convex.mem_Ioc {π•œ : Type u_1} [linear_ordered_field π•œ] {x y z : π•œ} (h : x < y) :
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.

theorem convex.mem_Ico {π•œ : Type u_1} [linear_ordered_field π•œ] {x y z : π•œ} (h : x < y) :
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.

theorem prod.segment_subset {π•œ : 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] (x y : E Γ— F) :
segment π•œ x y βŠ† segment π•œ x.fst y.fst Γ—Λ’ segment π•œ x.snd y.snd
theorem prod.open_segment_subset {π•œ : 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] (x y : E Γ— F) :
open_segment π•œ x y βŠ† open_segment π•œ x.fst y.fst Γ—Λ’ open_segment π•œ x.snd y.snd
theorem prod.image_mk_segment_left {π•œ : 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] (x₁ xβ‚‚ : E) (y : F) :
(Ξ» (x : E), (x, y)) '' segment π•œ x₁ xβ‚‚ = segment π•œ (x₁, y) (xβ‚‚, y)
theorem prod.image_mk_segment_right {π•œ : 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] (x : E) (y₁ yβ‚‚ : F) :
(Ξ» (y : F), (x, y)) '' segment π•œ y₁ yβ‚‚ = segment π•œ (x, y₁) (x, yβ‚‚)
theorem prod.image_mk_open_segment_left {π•œ : 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] (x₁ xβ‚‚ : E) (y : F) :
(Ξ» (x : E), (x, y)) '' open_segment π•œ x₁ xβ‚‚ = open_segment π•œ (x₁, y) (xβ‚‚, y)
@[simp]
theorem prod.image_mk_open_segment_right {π•œ : 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] (x : E) (y₁ yβ‚‚ : F) :
(Ξ» (y : F), (x, y)) '' open_segment π•œ y₁ yβ‚‚ = open_segment π•œ (x, y₁) (x, yβ‚‚)
theorem pi.segment_subset {π•œ : Type u_1} {ΞΉ : Type u_5} {Ο€ : ΞΉ β†’ Type u_6} [ordered_semiring π•œ] [Ξ  (i : ΞΉ), add_comm_monoid (Ο€ i)] [Ξ  (i : ΞΉ), module π•œ (Ο€ i)] {s : set ΞΉ} (x y : Ξ  (i : ΞΉ), Ο€ i) :
segment π•œ x y βŠ† s.pi (Ξ» (i : ΞΉ), segment π•œ (x i) (y i))
theorem pi.open_segment_subset {π•œ : Type u_1} {ΞΉ : Type u_5} {Ο€ : ΞΉ β†’ Type u_6} [ordered_semiring π•œ] [Ξ  (i : ΞΉ), add_comm_monoid (Ο€ i)] [Ξ  (i : ΞΉ), module π•œ (Ο€ i)] {s : set ΞΉ} (x y : Ξ  (i : ΞΉ), Ο€ i) :
open_segment π•œ x y βŠ† s.pi (Ξ» (i : ΞΉ), open_segment π•œ (x i) (y i))
theorem pi.image_update_segment {π•œ : Type u_1} {ΞΉ : Type u_5} {Ο€ : ΞΉ β†’ Type u_6} [ordered_semiring π•œ] [Ξ  (i : ΞΉ), add_comm_monoid (Ο€ i)] [Ξ  (i : ΞΉ), module π•œ (Ο€ i)] [decidable_eq ΞΉ] (i : ΞΉ) (x₁ xβ‚‚ : Ο€ i) (y : Ξ  (i : ΞΉ), Ο€ i) :
function.update y i '' segment π•œ x₁ xβ‚‚ = segment π•œ (function.update y i x₁) (function.update y i xβ‚‚)
theorem pi.image_update_open_segment {π•œ : Type u_1} {ΞΉ : Type u_5} {Ο€ : ΞΉ β†’ Type u_6} [ordered_semiring π•œ] [Ξ  (i : ΞΉ), add_comm_monoid (Ο€ i)] [Ξ  (i : ΞΉ), module π•œ (Ο€ i)] [decidable_eq ΞΉ] (i : ΞΉ) (x₁ xβ‚‚ : Ο€ i) (y : Ξ  (i : ΞΉ), Ο€ i) :
function.update y i '' open_segment π•œ x₁ xβ‚‚ = open_segment π•œ (function.update y i x₁) (function.update y i xβ‚‚)