Right-Hand Dini Upper Derivative: ε–δ Extraction and Filter Lemmas

This file implements the minimal analytic lemmas needed for robust proofs of local control from right-hand Dini upper derivatives.

Main results

• lemma_R1_eventually_le_from_limsup: Eventually ≤ from limsup ≤
• lemma_R2_right_filter_extraction: Right-filter ε–δ extraction
• lemma_R3_ereal_coercion: EReal coercion simplification (references to Mathlib)
• lemma_R4_multiply_positive: Multiply by a positive increment
• right_epsilon_delta_from_dini_nonpos: Main corollary combining all lemmas

theorem Frourio.lemma_R1_eventually_le_from_limsup {α : Type u_1} {f : α → ℝ} {l : Filter α} {c : ℝ} (h : Filter.limsup (fun (x : α) => ↑(f x)) l ≤ ↑c) (η : ℝ) (hη : 0 < η) : ∀ᶠ (x : α) in l, f x ≤ c + η

Lemma R1: Eventually-≤ from limsup ≤ If limsup f l ≤ c, then for every η > 0, eventually f x ≤ c + η.

theorem Frourio.lemma_R1_nonpos_special {α : Type u_1} {f : α → ℝ} {l : Filter α} (h : Filter.limsup (fun (x : α) => ↑(f x)) l ≤ 0) (ε : ℝ) (hε : 0 < ε) : ∀ᶠ (x : α) in l, f x ≤ ε

Specialized version with c = 0 for Dini applications

theorem Frourio.lemma_R2_right_filter_extraction {P : ℝ → Prop} (h : ∀ᶠ (h : ℝ) in nhdsWithin 0 (Set.Ioi 0), P h) : ∃ δ > 0, ∀ (h : ℝ), 0 < h → h < δ → P h

Lemma R2: Right-filter ε–δ extraction If P holds eventually in nhdsWithin 0 (0,+∞), then there exists δ > 0 such that P h holds for all 0 < h < δ.

theorem Frourio.lemma_R3a_coe_lt (x y : ℝ) : ↑x < ↑y ↔ x < y

Lemma R3a: EReal coercion for <

theorem Frourio.lemma_R3b_coe_le (x y : ℝ) : ↑x ≤ ↑y ↔ x ≤ y

Lemma R3b: EReal coercion for ≤

theorem Frourio.lemma_R4_multiply_positive {φ : ℝ → ℝ} {t h ε : ℝ} (hh_pos : 0 < h) (hq : (φ (t + h) - φ t) / h ≤ ε) : φ (t + h) - φ t ≤ ε * h

Lemma R4: Multiply by a positive increment If h > 0 and q(h) ≤ ε, then φ(t+h) - φ(t) ≤ ε·h.

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

Corollary: Right ε–δ from DiniUpperE ≤ 0 Given DiniUpperE φ t ≤ 0 and ε > 0, there exists δ > 0 such that for all 0 < h < δ, we have φ(t+h) - φ(t) ≤ ε·h.

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

Convenience wrapper that matches the signature in EVICore6