noncomputable def Frourio.quotient_function (φ : ℝ → ℝ) (s y h : ℝ) : ℝ

The quotient function q(y,h) = (φ(s + (y + h)) - φ(s + y)) / h for h > 0

Equations

• Frourio.quotient_function φ s y h = (φ (s + (y + h)) - φ (s + y)) / h

def Frourio.upper_semicontinuous_at_zero (φ : ℝ → ℝ) (s y₀ : ℝ) : Prop

Upper semicontinuity condition for the quotient function at h = 0

Equations

• Frourio.upper_semicontinuous_at_zero φ s y₀ = ∀ ε > 0, ∃ α > 0, ∃ β > 0, ∀ (y h : ℝ), |y - y₀| < α → 0 < h → h < β → Frourio.quotient_function φ s y h < ε

theorem Frourio.lemma_U1_parametric_uniformization {φ : ℝ → ℝ} {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 h : ℝ), |y - w| < ρ_w → 0 < h → h < δ_w → quotient_function φ s y h ≤ ε

Lemma U1: Parametric right-ε–δ uniformization at a base point Given upper semicontinuity and Dini conditions near w, we get uniform bounds.

theorem Frourio.lemma_U2_directed_two_point {φ : ℝ → ℝ} {s r w ρ_w δ_w ε : ℝ} (h_uniform : ∀ (y h : ℝ), |y - w| < ρ_w → 0 < h → h < δ_w → quotient_function φ s y h ≤ ε) (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)

Lemma U2: Directed two-point control from U1 From uniform bounds on the quotient, get the two-point estimate.

theorem Frourio.lemma_U3_metric_form (y w ρ : ℝ) : |y - w| < ρ ↔ dist y w < ρ

Lemma U3: Metric form equivalence On ℝ, |y - w| < ρ is equivalent to dist y w < ρ.

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

For y ≤ z, dist y z = z - y

theorem Frourio.directed_two_point_local_uniform {φ : ℝ → ℝ} {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 → dist y w < ρ_w → dist z w < ρ_w → z - y < δ_w → φ (s + z) - φ (s + y) ≤ ε * (z - y)

Main Theorem: Directed two-point local control with uniform bounds Combining U1, U2, and U3 to get the desired control around w.

theorem Frourio.directed_two_point_local_abs {φ : ℝ → ℝ} {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)

Alternative version using absolute values directly