Monotonicity lemmas from Dini derivatives

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

If the limsup of a function is ≤ 0, then for any ε > 0, the function is eventually ≤ ε

theorem Frourio.local_control_from_DiniUpperE (φ : ℝ → ℝ) (t ε : ℝ) (hε : 0 < ε) (h_dini : DiniUpperE φ t ≤ 0) : ∃ δ > 0, ∀ (h : ℝ), 0 < h ∧ h < δ → (φ (t + h) - φ t) / h ≤ ε

If DiniUpperE φ t ≤ 0 and ε > 0, then there exists δ > 0 such that for all h with 0 < h < δ, we have (φ(t+h) - φ(t))/h ≤ ε

theorem Frourio.telescoping_sum_real (t : ℕ → ℝ) (n : ℕ) : ∑ i ∈ Finset.range n, (t (i + 1) - t i) = t n - t 0

Pure telescoping identity on ℝ: ∑_{i=0}^{n-1} (t (i+1) - t i) = t n - t 0.

theorem Frourio.sum_bound_from_stepwise (φ : ℝ → ℝ) (s ε : ℝ) {N : ℕ} (t : ℕ → ℝ) (hstep : ∀ i < N, φ (s + t (i + 1)) - φ (s + t i) ≤ ε * (t (i + 1) - t i)) : ∑ i ∈ Finset.range N, (φ (s + t (i + 1)) - φ (s + t i)) ≤ ε * ∑ i ∈ Finset.range N, (t (i + 1) - t i)

If each short subinterval (t i, t (i+1)) satisfies the incremental bound, then summing gives the bound on the whole union.

theorem Frourio.global_from_uniform_small_interval_control (φ : ℝ → ℝ) (s r ε : ℝ) (hr_pos : 0 < r) (hL : ∃ 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)) : φ (s + r) ≤ φ s + ε * r

Global composition from a uniform small-interval control.

theorem Frourio.finite_chain_composition_core (φ : ℝ → ℝ) (s r ε : ℝ) (hr_pos : 0 < r) (hε_pos : 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)) : φ (s + r) ≤ φ s + ε * r

Core finite-chain composition, assuming ball-local two-point control. (lebesgue_property_from_two_point_local).

theorem Frourio.finite_chain_composition_with_usc (φ : ℝ → ℝ) (s r ε : ℝ) (hr_pos : 0 < r) (hε_pos : 0 < ε) (h_dini_all : ∀ u ∈ Set.Icc 0 r, DiniUpperE φ (s + u) ≤ 0) (h_usc : ∀ w ∈ Set.Icc 0 r, ∀ y₀ ∈ Set.Icc 0 r, |y₀ - w| < r / 4 → upper_semicontinuous_at_zero φ s y₀) : φ (s + r) ≤ φ s + ε * r

Correct version with upper semicontinuity hypothesis

theorem Frourio.limit_epsilon_to_zero (f g c : ℝ) (hc : 0 ≤ c) (h : ∀ ε > 0, f ≤ g + ε * c) : f ≤ g

If for all ε > 0 we have f ≤ g + ε*c where c ≥ 0, then f ≤ g

theorem Frourio.shifted_function_nonincreasing_with_usc (φ : ℝ → ℝ) (s : ℝ) (h_dini_shifted : ∀ u ≥ 0, DiniUpperE (fun (τ : ℝ) => φ (s + τ) - φ s) u ≤ 0) (h_usc : ∀ t > 0, ∀ w ∈ Set.Icc 0 t, ∀ y₀ ∈ Set.Icc 0 t, |y₀ - w| < t / 4 → upper_semicontinuous_at_zero φ s y₀) (t : ℝ) : t ≥ 0 → φ (s + t) ≤ φ s

theorem Frourio.nonincreasing_of_DiniUpperE_nonpos_with_usc (φ : ℝ → ℝ) (hD : ∀ (u : ℝ), DiniUpperE φ u ≤ 0) (h_usc : ∀ (s t : ℝ), s < t → ∀ w ∈ Set.Icc 0 (t - s), ∀ y₀ ∈ Set.Icc 0 (t - s), |y₀ - w| < (t - s) / 4 → upper_semicontinuous_at_zero φ s y₀) (s t : ℝ) : s ≤ t → φ t ≤ φ s

Main monotonicity theorem with upper semicontinuity: if DiniUpperE is non-positive everywhere and the function satisfies upper semicontinuity conditions, then the function is non-increasing

Generic predicate-level bridges between an abstract energy-dissipation predicate P : (X → ℝ) → (ℝ → X) → Prop and the EVI predicate. These are kept abstract here to avoid import cycles with PLFACore where EDE is defined; users can specialize P to EDE on the PLFA side.

def Frourio.EVIBridgeForward {X : Type u_1} [PseudoMetricSpace X] (P : (X → ℝ) → (ℝ → X) → Prop) (F : X → ℝ) (lam : ℝ) : Prop

Forward bridge: from an abstract predicate P F ρ to the EVI predicate for F. Specialize P to EDE on the PLFA side to obtain EDE → EVI.

Equations

• Frourio.EVIBridgeForward P F lam = ∀ (ρ : ℝ → X), P F ρ → Frourio.IsEVISolution { E := F, lam := lam } ρ

def Frourio.EVIBridgeBackward {X : Type u_1} [PseudoMetricSpace X] (P : (X → ℝ) → (ℝ → X) → Prop) (F : X → ℝ) (lam : ℝ) : Prop

Backward bridge: from the EVI predicate for F to an abstract predicate P F ρ. Specialize P to EDE on the PLFA side to obtain EVI → EDE.

Equations

• Frourio.EVIBridgeBackward P F lam = ∀ (ρ : ℝ → X), Frourio.IsEVISolution { E := F, lam := lam } ρ → P F ρ

def Frourio.EVIEquivBridge {X : Type u_1} [PseudoMetricSpace X] (P : (X → ℝ) → (ℝ → X) → Prop) (F : X → ℝ) (lam : ℝ) : Prop

Equivalence bridge: P F ρ holds iff the EVI predicate holds for F.

Equations

• Frourio.EVIEquivBridge P F lam = (Frourio.EVIBridgeForward P F lam ∧ Frourio.EVIBridgeBackward P F lam)

Geodesic uniform evaluation (two‑EVI input)

def Frourio.GeodesicUniformEval {X : Type u_1} [PseudoMetricSpace X] (P : EVIProblem X) (u v : ℝ → X) : Prop

Geodesic-uniform evaluation predicate used by two‑EVI assumptions. It provides, uniformly for all error levels η, a bridge from squared‑distance contraction to linear‑distance contraction. This matches the role geodesic regularity plays in AGS-type arguments and is sufficient for the with‑error pipeline in this phase.

Equations

• Frourio.GeodesicUniformEval P u v = ∀ (η : ℝ), Frourio.HbridgeWithError P u v η

theorem Frourio.geodesicUniform_to_bridge {X : Type u_1} [PseudoMetricSpace X] {P : EVIProblem X} {u v : ℝ → X} (G : GeodesicUniformEval P u v) (η : ℝ) : HbridgeWithError P u v η

Convenience: extract a bridge at a given error level from GeodesicUniformEval.