Lebesgue Number Lemma

This file provides the Lebesgue number lemma for compact metric spaces, which states that for any open cover of a compact set, there exists a positive number L (the Lebesgue number) such that any subset with diameter less than L is contained in some member of the cover.

Main definitions

• HasSmallDiam: Predicate for sets with diameter less than a given value
• LebesgueNumber: Property that a number L is a Lebesgue number for a cover

Main results

• lebesgue_number_exists: Every open cover of a compact metric space has a Lebesgue number
• uniform_control_from_local: Application to EVI theory - uniform control from local controls

def Frourio.HasSmallDiam {X : Type u_1} [PseudoMetricSpace X] (A : Set X) (ε : ℝ) : Prop

A set has small diameter if all distances between its points are less than ε

Equations

• Frourio.HasSmallDiam A ε = ∀ (x y : X), x ∈ A → y ∈ A → dist x y < ε

def Frourio.LebesgueNumber {X : Type u_1} [PseudoMetricSpace X] {ι : Type u_2} (K : Set X) (U : ι → Set X) (L : ℝ) : Prop

A number L is a Lebesgue number for a cover if every set with diameter < L is contained in some member of the cover

Equations

• Frourio.LebesgueNumber K U L = (0 < L ∧ ∀ A ⊆ K, Frourio.HasSmallDiam A L → ∃ (i : ι), A ⊆ U i)

theorem Frourio.lebesgue_number_exists {X : Type u_1} [PseudoMetricSpace X] {ι : Type u_2} [Nonempty ι] {K : Set X} (hK : IsCompact K) {U : ι → Set X} (hU : ∀ (i : ι), IsOpen (U i)) (hcover : K ⊆ ⋃ (i : ι), U i) : ∃ L > 0, LebesgueNumber K U L

ルベーグ数補題（コンパクト距離空間の開被覆）

theorem Frourio.lebesgue_property_from_two_point_local {φ : ℝ → ℝ} {s r ε : ℝ} (hr : 0 < r) (_hε : 0 < ε) (two_point_ball_local : ∀ w ∈ Set.Icc 0 r, ∃ ρw > 0, ∃ δw > 0, ∀ u ∈ Set.Icc 0 r, ∀ v ∈ Set.Icc 0 r, dist u w < ρw → dist v w < ρw → φ (s + v) - φ (s + u) ≤ ε * (v - u)) : ∃ L > 0, ∀ y ∈ Set.Icc 0 r, ∀ z ∈ Set.Icc 0 r, 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)

（変更版）二点局所制御を球近傍で与える仮定から、 ルベーグ数に基づく一様二点制御を得る。向き条件は用いない。