Oriented (Directed) Lebesgue Number Lemmas

This file implements the oriented versions of the Lebesgue number lemma for two-point local control. These lemmas handle the case where we have directional constraints (y ≤ z) in addition to distance bounds.

Main definitions

• OrientedProductSpace: The space K = {(y,z) ∈ I×I | y ≤ z}

Main results

• oriented_lebesgue_from_two_point_local: Lebesgue number for oriented two-point cover
• oriented_uniform_small_interval_control: Uniform control on small oriented intervals
• dist_eq_sub_of_le: In ℝ, if y ≤ z then dist y z = z - y

theorem Frourio.two_point_hasSmallDiam_iff {X : Type u_1} [PseudoMetricSpace X] {y z : X} {L : ℝ} (hL : 0 < L) : HasSmallDiam {y, z} L ↔ dist y z < L

L1 Helper: For a two-point set {y,z} in a metric space, HasSmallDiam {y,z} L iff dist y z < L

theorem Frourio.two_point_lebesgue {ι : Type u_1} [Nonempty ι] {K : Set ℝ} (hK : IsCompact K) {U : ι → Set ℝ} (hU : ∀ (i : ι), IsOpen (U i)) (hcover : K ⊆ ⋃ (i : ι), U i) : ∃ L > 0, ∀ (y z : ℝ), y ∈ K → z ∈ K → dist y z < L → ∃ (i : ι), y ∈ U i ∧ z ∈ U i

Lemma L1: Two-Point Lebesgue Number Lemma Given a subset form Lebesgue lemma, we can derive a two-point version that directly gives membership instead of subset inclusion

def Frourio.OrientedProductSpace (r : ℝ) : Set (ℝ × ℝ)

The oriented product space K = {(y,z) ∈ I×I | y ≤ z}

Equations

• Frourio.OrientedProductSpace r = {p : ℝ × ℝ | p.1 ∈ Set.Icc 0 r ∧ p.2 ∈ Set.Icc 0 r ∧ p.1 ≤ p.2}

theorem Frourio.dist_eq_sub_of_le {y z : ℝ} (h : y ≤ z) : dist y z = z - y

Additional Lemma 3: In ℝ, if y ≤ z then dist y z = z - y

theorem Frourio.oriented_lebesgue_from_two_point_local {φ : ℝ → ℝ} {s r ε : ℝ} (hr : 0 < r) (h_local : ∀ w ∈ Set.Icc 0 r, ∃ ρ_w > 0, ∃ δ_w > 0, ∀ (y z : ℝ), y ∈ Set.Icc 0 r → z ∈ Set.Icc 0 r → y ≤ z → dist y w < ρ_w → dist z w < ρ_w → z - y < δ_w → φ (s + z) - φ (s + y) ≤ ε * (z - y)) : ∃ L > 0, ∀ (y z : ℝ), y ∈ Set.Icc 0 r → z ∈ Set.Icc 0 r → y ≤ z → dist y z < L → ∃ w ∈ Set.Icc 0 r, ∃ δ_w > 0, dist y w < δ_w ∧ dist z w < δ_w ∧ φ (s + z) - φ (s + y) ≤ ε * (z - y)

Additional Lemma 1: Oriented Lebesgue from Two-Point Local Control Given oriented two-point local control, there exists a Lebesgue number L > 0 such that any pair (y,z) with y ≤ z and dist y z < L is contained in some local control neighborhood.

theorem Frourio.oriented_uniform_small_interval_control {φ : ℝ → ℝ} {s r ε : ℝ} (hr : 0 < r) (h_local : ∀ w ∈ Set.Icc 0 r, ∃ ρ_w > 0, ∃ δ_w > 0, ∀ (y z : ℝ), y ∈ Set.Icc 0 r → z ∈ Set.Icc 0 r → y ≤ z → dist y w < ρ_w → dist z w < ρ_w → z - y < δ_w → φ (s + z) - φ (s + y) ≤ ε * (z - y)) : ∃ L > 0, ∀ (y z : ℝ), y ∈ Set.Icc 0 r → z ∈ Set.Icc 0 r → y ≤ z → z - y < L → φ (s + z) - φ (s + y) ≤ ε * (z - y)

Additional Lemma 2: Oriented Uniform Small-Interval Control A corollary that directly gives uniform control on small oriented intervals.