Documentation

Mathlib.Analysis.Convex.Segment

Segments in vector spaces #

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 openSegment to convex.Icc and convex.Ioo? Should we also define clopenSegment/convex.Ico/convex.Ioc?

def segment (𝕜 : Type u_1) {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [SMul 𝕜 E] (x : E) (y : E) :
Set E

Segments in a vector space.

Equations
Instances For
    def openSegment (𝕜 : Type u_1) {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [SMul 𝕜 E] (x : E) (y : E) :
    Set E

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

    Equations
    Instances For
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        theorem segment_eq_image₂ (𝕜 : Type u_1) {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [SMul 𝕜 E] (x : E) (y : E) :
        segment 𝕜 x y = (fun p => p.fst x + p.snd y) '' {p | 0 p.fst 0 p.snd p.fst + p.snd = 1}
        theorem openSegment_eq_image₂ (𝕜 : Type u_1) {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [SMul 𝕜 E] (x : E) (y : E) :
        openSegment 𝕜 x y = (fun 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} [OrderedSemiring 𝕜] [AddCommMonoid E] [SMul 𝕜 E] (x : E) (y : E) :
        segment 𝕜 x y = segment 𝕜 y x
        theorem openSegment_symm (𝕜 : Type u_1) {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [SMul 𝕜 E] (x : E) (y : E) :
        openSegment 𝕜 x y = openSegment 𝕜 y x
        theorem openSegment_subset_segment (𝕜 : Type u_1) {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [SMul 𝕜 E] (x : E) (y : E) :
        openSegment 𝕜 x y segment 𝕜 x y
        theorem segment_subset_iff (𝕜 : Type u_1) {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [SMul 𝕜 E] {s : Set E} {x : E} {y : E} :
        segment 𝕜 x y s ∀ (a b : 𝕜), 0 a0 ba + b = 1a x + b y s
        theorem openSegment_subset_iff (𝕜 : Type u_1) {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [SMul 𝕜 E] {s : Set E} {x : E} {y : E} :
        openSegment 𝕜 x y s ∀ (a b : 𝕜), 0 < a0 < ba + b = 1a x + b y s
        theorem left_mem_segment (𝕜 : Type u_1) {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [MulActionWithZero 𝕜 E] (x : E) (y : E) :
        x segment 𝕜 x y
        theorem right_mem_segment (𝕜 : Type u_1) {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [MulActionWithZero 𝕜 E] (x : E) (y : E) :
        y segment 𝕜 x y
        @[simp]
        theorem segment_same (𝕜 : Type u_1) {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] (x : E) :
        segment 𝕜 x x = {x}
        theorem insert_endpoints_openSegment (𝕜 : Type u_1) {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] (x : E) (y : E) :
        insert x (insert y (openSegment 𝕜 x y)) = segment 𝕜 x y
        theorem mem_openSegment_of_ne_left_right {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] {x : E} {y : E} {z : E} (hx : x z) (hy : y z) (hz : z segment 𝕜 x y) :
        z openSegment 𝕜 x y
        theorem openSegment_subset_iff_segment_subset {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] {s : Set E} {x : E} {y : E} (hx : x s) (hy : y s) :
        openSegment 𝕜 x y s segment 𝕜 x y s
        @[simp]
        theorem openSegment_same (𝕜 : Type u_1) {E : Type u_2} [OrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] [Nontrivial 𝕜] [DenselyOrdered 𝕜] (x : E) :
        openSegment 𝕜 x x = {x}
        theorem segment_eq_image (𝕜 : Type u_1) {E : Type u_2} [OrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] (x : E) (y : E) :
        segment 𝕜 x y = (fun θ => (1 - θ) x + θ y) '' Set.Icc 0 1
        theorem openSegment_eq_image (𝕜 : Type u_1) {E : Type u_2} [OrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] (x : E) (y : E) :
        openSegment 𝕜 x y = (fun θ => (1 - θ) x + θ y) '' Set.Ioo 0 1
        theorem segment_eq_image' (𝕜 : Type u_1) {E : Type u_2} [OrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] (x : E) (y : E) :
        segment 𝕜 x y = (fun θ => x + θ (y - x)) '' Set.Icc 0 1
        theorem openSegment_eq_image' (𝕜 : Type u_1) {E : Type u_2} [OrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] (x : E) (y : E) :
        openSegment 𝕜 x y = (fun θ => x + θ (y - x)) '' Set.Ioo 0 1
        theorem segment_eq_image_lineMap (𝕜 : Type u_1) {E : Type u_2} [OrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] (x : E) (y : E) :
        segment 𝕜 x y = ↑(AffineMap.lineMap x y) '' Set.Icc 0 1
        theorem openSegment_eq_image_lineMap (𝕜 : Type u_1) {E : Type u_2} [OrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] (x : E) (y : E) :
        openSegment 𝕜 x y = ↑(AffineMap.lineMap x y) '' Set.Ioo 0 1
        @[simp]
        theorem image_segment (𝕜 : Type u_1) {E : Type u_2} {F : Type u_3} [OrderedRing 𝕜] [AddCommGroup E] [AddCommGroup F] [Module 𝕜 E] [Module 𝕜 F] (f : E →ᵃ[𝕜] F) (a : E) (b : E) :
        f '' segment 𝕜 a b = segment 𝕜 (f a) (f b)
        @[simp]
        theorem image_openSegment (𝕜 : Type u_1) {E : Type u_2} {F : Type u_3} [OrderedRing 𝕜] [AddCommGroup E] [AddCommGroup F] [Module 𝕜 E] [Module 𝕜 F] (f : E →ᵃ[𝕜] F) (a : E) (b : E) :
        f '' openSegment 𝕜 a b = openSegment 𝕜 (f a) (f b)
        @[simp]
        theorem vadd_segment (𝕜 : Type u_1) {E : Type u_2} {G : Type u_4} [OrderedRing 𝕜] [AddCommGroup E] [AddCommGroup G] [Module 𝕜 E] [AddTorsor G E] [VAddCommClass G E E] (a : G) (b : E) (c : E) :
        a +ᵥ segment 𝕜 b c = segment 𝕜 (a +ᵥ b) (a +ᵥ c)
        @[simp]
        theorem vadd_openSegment (𝕜 : Type u_1) {E : Type u_2} {G : Type u_4} [OrderedRing 𝕜] [AddCommGroup E] [AddCommGroup G] [Module 𝕜 E] [AddTorsor G E] [VAddCommClass G E E] (a : G) (b : E) (c : E) :
        a +ᵥ openSegment 𝕜 b c = openSegment 𝕜 (a +ᵥ b) (a +ᵥ c)
        @[simp]
        theorem mem_segment_translate (𝕜 : Type u_1) {E : Type u_2} [OrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] (a : E) {x : E} {b : E} {c : E} :
        a + x segment 𝕜 (a + b) (a + c) x segment 𝕜 b c
        @[simp]
        theorem mem_openSegment_translate (𝕜 : Type u_1) {E : Type u_2} [OrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] (a : E) {x : E} {b : E} {c : E} :
        a + x openSegment 𝕜 (a + b) (a + c) x openSegment 𝕜 b c
        theorem segment_translate_preimage (𝕜 : Type u_1) {E : Type u_2} [OrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] (a : E) (b : E) (c : E) :
        (fun x => a + x) ⁻¹' segment 𝕜 (a + b) (a + c) = segment 𝕜 b c
        theorem openSegment_translate_preimage (𝕜 : Type u_1) {E : Type u_2} [OrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] (a : E) (b : E) (c : E) :
        (fun x => a + x) ⁻¹' openSegment 𝕜 (a + b) (a + c) = openSegment 𝕜 b c
        theorem segment_translate_image (𝕜 : Type u_1) {E : Type u_2} [OrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] (a : E) (b : E) (c : E) :
        (fun x => a + x) '' segment 𝕜 b c = segment 𝕜 (a + b) (a + c)
        theorem openSegment_translate_image (𝕜 : Type u_1) {E : Type u_2} [OrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] (a : E) (b : E) (c : E) :
        (fun x => a + x) '' openSegment 𝕜 b c = openSegment 𝕜 (a + b) (a + c)
        theorem segment_inter_eq_endpoint_of_linearIndependent_sub (𝕜 : Type u_1) {E : Type u_2} [OrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {c : E} {x : E} {y : E} (h : LinearIndependent 𝕜 ![x - c, y - c]) :
        segment 𝕜 c x segment 𝕜 c y = {c}
        theorem sameRay_of_mem_segment {𝕜 : Type u_1} {E : Type u_2} [StrictOrderedCommRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {x : E} {y : E} {z : E} (h : x segment 𝕜 y z) :
        SameRay 𝕜 (x - y) (z - x)
        theorem segment_inter_eq_endpoint_of_linearIndependent_of_ne {𝕜 : Type u_1} {E : Type u_2} [OrderedCommRing 𝕜] [NoZeroDivisors 𝕜] [AddCommGroup E] [Module 𝕜 E] {x : E} {y : E} (h : LinearIndependent 𝕜 ![x, y]) {s : 𝕜} {t : 𝕜} (hs : s t) (c : E) :
        segment 𝕜 (c + x) (c + t y) segment 𝕜 (c + x) (c + s y) = {c + x}
        theorem midpoint_mem_segment {𝕜 : Type u_1} {E : Type u_2} [LinearOrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] [Invertible 2] (x : E) (y : E) :
        midpoint 𝕜 x y segment 𝕜 x y
        theorem mem_segment_sub_add {𝕜 : Type u_1} {E : Type u_2} [LinearOrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] [Invertible 2] (x : E) (y : E) :
        x segment 𝕜 (x - y) (x + y)
        theorem mem_segment_add_sub {𝕜 : Type u_1} {E : Type u_2} [LinearOrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] [Invertible 2] (x : E) (y : E) :
        x segment 𝕜 (x + y) (x - y)
        @[simp]
        theorem left_mem_openSegment_iff {𝕜 : Type u_1} {E : Type u_2} [LinearOrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {x : E} {y : E} [DenselyOrdered 𝕜] [NoZeroSMulDivisors 𝕜 E] :
        x openSegment 𝕜 x y x = y
        @[simp]
        theorem right_mem_openSegment_iff {𝕜 : Type u_1} {E : Type u_2} [LinearOrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {x : E} {y : E} [DenselyOrdered 𝕜] [NoZeroSMulDivisors 𝕜 E] :
        y openSegment 𝕜 x y x = y
        theorem mem_segment_iff_div {𝕜 : Type u_1} {E : Type u_2} [LinearOrderedSemifield 𝕜] [AddCommGroup E] [Module 𝕜 E] {x : E} {y : E} {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_openSegment_iff_div {𝕜 : Type u_1} {E : Type u_2} [LinearOrderedSemifield 𝕜] [AddCommGroup E] [Module 𝕜 E] {x : E} {y : E} {z : E} :
        x openSegment 𝕜 y z a b, 0 < a 0 < b (a / (a + b)) y + (b / (a + b)) z = x
        theorem mem_segment_iff_sameRay {𝕜 : Type u_1} {E : Type u_2} [LinearOrderedField 𝕜] [AddCommGroup E] [Module 𝕜 E] {x : E} {y : E} {z : E} :
        x segment 𝕜 y z SameRay 𝕜 (x - y) (z - x)
        theorem openSegment_subset_union {𝕜 : Type u_1} {E : Type u_2} [LinearOrderedField 𝕜] [AddCommGroup E] [Module 𝕜 E] (x : E) (y : E) {z : E} (hz : z Set.range ↑(AffineMap.lineMap x y)) :
        openSegment 𝕜 x y insert z (openSegment 𝕜 x z openSegment 𝕜 z y)

        If z = lineMap x y c is a point on the line passing through x and y, then the open segment openSegment 𝕜 x y is included in the union of the open segments openSegment 𝕜 x z, openSegment 𝕜 z y, and the point z. Informally, (x, y) ⊆ {z} ∪ (x, z) ∪ (z, y).

        Segments in an ordered space #

        Relates segment, openSegment and Set.Icc, Set.Ico, Set.Ioc, Set.Ioo

        theorem segment_subset_Icc {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [OrderedAddCommMonoid E] [Module 𝕜 E] [OrderedSMul 𝕜 E] {x : E} {y : E} (h : x y) :
        segment 𝕜 x y Set.Icc x y
        theorem openSegment_subset_Ioo {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [OrderedCancelAddCommMonoid E] [Module 𝕜 E] [OrderedSMul 𝕜 E] {x : E} {y : E} (h : x < y) :
        openSegment 𝕜 x y Set.Ioo x y
        theorem segment_subset_uIcc {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [LinearOrderedAddCommMonoid E] [Module 𝕜 E] [OrderedSMul 𝕜 E] (x : E) (y : E) :
        segment 𝕜 x y Set.uIcc x y
        theorem Convex.min_le_combo {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [LinearOrderedAddCommMonoid E] [Module 𝕜 E] [OrderedSMul 𝕜 E] {a : 𝕜} {b : 𝕜} (x : E) (y : E) (ha : 0 a) (hb : 0 b) (hab : a + b = 1) :
        min x y a x + b y
        theorem Convex.combo_le_max {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [LinearOrderedAddCommMonoid E] [Module 𝕜 E] [OrderedSMul 𝕜 E] {a : 𝕜} {b : 𝕜} (x : E) (y : E) (ha : 0 a) (hb : 0 b) (hab : a + b = 1) :
        a x + b y max x y
        theorem Icc_subset_segment {𝕜 : Type u_1} [LinearOrderedField 𝕜] {x : 𝕜} {y : 𝕜} :
        Set.Icc x y segment 𝕜 x y
        @[simp]
        theorem segment_eq_Icc {𝕜 : Type u_1} [LinearOrderedField 𝕜] {x : 𝕜} {y : 𝕜} (h : x y) :
        segment 𝕜 x y = Set.Icc x y
        theorem Ioo_subset_openSegment {𝕜 : Type u_1} [LinearOrderedField 𝕜] {x : 𝕜} {y : 𝕜} :
        Set.Ioo x y openSegment 𝕜 x y
        @[simp]
        theorem openSegment_eq_Ioo {𝕜 : Type u_1} [LinearOrderedField 𝕜] {x : 𝕜} {y : 𝕜} (h : x < y) :
        openSegment 𝕜 x y = Set.Ioo x y
        theorem segment_eq_Icc' {𝕜 : Type u_1} [LinearOrderedField 𝕜] (x : 𝕜) (y : 𝕜) :
        segment 𝕜 x y = Set.Icc (min x y) (max x y)
        theorem openSegment_eq_Ioo' {𝕜 : Type u_1} [LinearOrderedField 𝕜] {x : 𝕜} {y : 𝕜} (hxy : x y) :
        openSegment 𝕜 x y = Set.Ioo (min x y) (max x y)
        theorem segment_eq_uIcc {𝕜 : Type u_1} [LinearOrderedField 𝕜] (x : 𝕜) (y : 𝕜) :
        segment 𝕜 x y = Set.uIcc x y
        theorem Convex.mem_Icc {𝕜 : Type u_1} [LinearOrderedField 𝕜] {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} [LinearOrderedField 𝕜] {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} [LinearOrderedField 𝕜] {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} [LinearOrderedField 𝕜] {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} [OrderedSemiring 𝕜] [AddCommMonoid E] [AddCommMonoid F] [Module 𝕜 E] [Module 𝕜 F] (x : E × F) (y : E × F) :
        segment 𝕜 x y segment 𝕜 x.fst y.fst ×ˢ segment 𝕜 x.snd y.snd
        theorem Prod.openSegment_subset {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [OrderedSemiring 𝕜] [AddCommMonoid E] [AddCommMonoid F] [Module 𝕜 E] [Module 𝕜 F] (x : E × F) (y : E × F) :
        openSegment 𝕜 x y openSegment 𝕜 x.fst y.fst ×ˢ openSegment 𝕜 x.snd y.snd
        theorem Prod.image_mk_segment_left {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [OrderedSemiring 𝕜] [AddCommMonoid E] [AddCommMonoid F] [Module 𝕜 E] [Module 𝕜 F] (x₁ : E) (x₂ : E) (y : F) :
        (fun x => (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} [OrderedSemiring 𝕜] [AddCommMonoid E] [AddCommMonoid F] [Module 𝕜 E] [Module 𝕜 F] (x : E) (y₁ : F) (y₂ : F) :
        (fun y => (x, y)) '' segment 𝕜 y₁ y₂ = segment 𝕜 (x, y₁) (x, y₂)
        theorem Prod.image_mk_openSegment_left {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [OrderedSemiring 𝕜] [AddCommMonoid E] [AddCommMonoid F] [Module 𝕜 E] [Module 𝕜 F] (x₁ : E) (x₂ : E) (y : F) :
        (fun x => (x, y)) '' openSegment 𝕜 x₁ x₂ = openSegment 𝕜 (x₁, y) (x₂, y)
        @[simp]
        theorem Prod.image_mk_openSegment_right {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [OrderedSemiring 𝕜] [AddCommMonoid E] [AddCommMonoid F] [Module 𝕜 E] [Module 𝕜 F] (x : E) (y₁ : F) (y₂ : F) :
        (fun y => (x, y)) '' openSegment 𝕜 y₁ y₂ = openSegment 𝕜 (x, y₁) (x, y₂)
        theorem Pi.segment_subset {𝕜 : Type u_1} {ι : Type u_5} {π : ιType u_6} [OrderedSemiring 𝕜] [(i : ι) → AddCommMonoid (π i)] [(i : ι) → Module 𝕜 (π i)] {s : Set ι} (x : (i : ι) → π i) (y : (i : ι) → π i) :
        segment 𝕜 x y Set.pi s fun i => segment 𝕜 (x i) (y i)
        theorem Pi.openSegment_subset {𝕜 : Type u_1} {ι : Type u_5} {π : ιType u_6} [OrderedSemiring 𝕜] [(i : ι) → AddCommMonoid (π i)] [(i : ι) → Module 𝕜 (π i)] {s : Set ι} (x : (i : ι) → π i) (y : (i : ι) → π i) :
        openSegment 𝕜 x y Set.pi s fun i => openSegment 𝕜 (x i) (y i)
        theorem Pi.image_update_segment {𝕜 : Type u_1} {ι : Type u_5} {π : ιType u_6} [OrderedSemiring 𝕜] [(i : ι) → AddCommMonoid (π i)] [(i : ι) → Module 𝕜 (π i)] [DecidableEq ι] (i : ι) (x₁ : π i) (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_openSegment {𝕜 : Type u_1} {ι : Type u_5} {π : ιType u_6} [OrderedSemiring 𝕜] [(i : ι) → AddCommMonoid (π i)] [(i : ι) → Module 𝕜 (π i)] [DecidableEq ι] (i : ι) (x₁ : π i) (x₂ : π i) (y : (i : ι) → π i) :
        Function.update y i '' openSegment 𝕜 x₁ x₂ = openSegment 𝕜 (Function.update y i x₁) (Function.update y i x₂)