theorem Frourio.local_control_from_DiniUpperE_right {φ : ℝ → ℝ} {ε : ℝ} (t : ℝ) (hDini : DiniUpperE φ t ≤ 0) (hε : 0 < ε) : ∃ δ > 0, ∀ (h : ℝ), 0 < h → h < δ → φ (t + h) - φ t ≤ ε * h

Lemma A: Local control from right-sided Dini upper derivative. If DiniUpperE φ t ≤ 0 and ε > 0, then there exists δ > 0 such that for all 0 < h < δ, we have φ(t+h) - φ(t) ≤ ε h.

theorem Frourio.directed_two_point_local_with_usc {φ : ℝ → ℝ} {s r ε w : ℝ} (hw : w ∈ Set.Icc 0 r) (hr : 0 < r) (hDini : ∀ u ∈ Set.Icc 0 r, DiniUpperE φ (s + u) ≤ 0) (hUSC : ∀ y₀ ∈ Set.Icc 0 r, |y₀ - w| < r / 4 → upper_semicontinuous_at_zero φ s y₀) (hε : 0 < ε) : ∃ ρ_w > 0, ∃ δ_w > 0, ∀ (y z : ℝ), y ∈ Set.Icc 0 r → z ∈ Set.Icc 0 r → y ≤ z → |y - w| < ρ_w → |z - w| < ρ_w → z - y < δ_w → φ (s + z) - φ (s + y) ≤ ε * (z - y)

Version of directed_two_point_local with upper semicontinuity hypothesis

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

The directed product space K = {(y,z) ∈ I×I | y ≤ z} with max metric

Equations

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

def Frourio.maxDist (p q : ℝ × ℝ) : ℝ

Max metric on the product space

Equations

• Frourio.maxDist p q = max |p.1 - q.1| |p.2 - q.2|

theorem Frourio.lebesgue_number_for_directed_cover_with_usc {φ : ℝ → ℝ} {s r ε : ℝ} (hDini : ∀ u ∈ Set.Icc 0 r, DiniUpperE φ (s + u) ≤ 0) (hUSC : ∀ w ∈ Set.Icc 0 r, ∀ y₀ ∈ Set.Icc 0 r, |y₀ - w| < r / 4 → upper_semicontinuous_at_zero φ s y₀) (hε : 0 < ε) (hr : 0 < r) : ∃ 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)

Complete version of Lemma C: Lebesgue number with upper semicontinuity hypothesis. This is the correct formulation with all necessary hypotheses.

theorem Frourio.uniform_small_interval_control_with_usc {φ : ℝ → ℝ} {s r ε : ℝ} (hDini : ∀ u ∈ Set.Icc 0 r, DiniUpperE φ (s + u) ≤ 0) (hUSC : ∀ w ∈ Set.Icc 0 r, ∀ y₀ ∈ Set.Icc 0 r, |y₀ - w| < r / 4 → upper_semicontinuous_at_zero φ s y₀) (hε : 0 < ε) (hr : 0 < r) : ∃ 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)

Complete version of Proposition D with upper semicontinuity hypothesis

theorem Frourio.global_evaluation_from_partition_with_usc {φ : ℝ → ℝ} {s r ε : ℝ} (hDini : ∀ u ∈ Set.Icc 0 r, DiniUpperE φ (s + u) ≤ 0) (hUSC : ∀ w ∈ Set.Icc 0 r, ∀ y₀ ∈ Set.Icc 0 r, |y₀ - w| < r / 4 → upper_semicontinuous_at_zero φ s y₀) (hε : 0 < ε) (hr : 0 < r) : φ (s + r) ≤ φ s + ε * r

Corollary: Global evaluation via finite chain composition (with USC). Using partition and telescoping sum, we get φ(s+r) ≤ φ(s) + εr.

theorem Frourio.nonincreasing_of_DiniUpperE_nonpos_right_with_usc {φ : ℝ → ℝ} (hDini : ∀ (t : ℝ), DiniUpperE φ t ≤ 0) (hUSC : ∀ (s r : ℝ), r > 0 → ∀ w ∈ Set.Icc 0 r, ∀ y₀ ∈ Set.Icc 0 r, |y₀ - w| < r / 4 → upper_semicontinuous_at_zero φ s y₀) (s t : ℝ) : s ≤ t → φ t ≤ φ s

Complete version with upper semicontinuity hypothesis