theorem Frourio.DiniUpper_add_le_of_finite (φ ψ : ℝ → ℝ) (t : ℝ) (hφ_fin : DiniUpperE φ t ≠ ⊤ ∧ DiniUpperE φ t ≠ ⊥) (hψ_fin : DiniUpperE ψ t ≠ ⊤ ∧ DiniUpperE ψ t ≠ ⊥) (hsum_fin : DiniUpperE (fun (τ : ℝ) => φ τ + ψ τ) t ≠ ⊤ ∧ DiniUpperE (fun (τ : ℝ) => φ τ + ψ τ) t ≠ ⊥) (hubφ : ∃ (M : ℝ), ∀ᶠ (h : ℝ) in nhdsWithin 0 (Set.Ioi 0), (φ (t + h) - φ t) / h ≤ M) (hlbφ : ∃ (m : ℝ), ∀ᶠ (h : ℝ) in nhdsWithin 0 (Set.Ioi 0), m ≤ (φ (t + h) - φ t) / h) (hubψ : ∃ (M : ℝ), ∀ᶠ (h : ℝ) in nhdsWithin 0 (Set.Ioi 0), (ψ (t + h) - ψ t) / h ≤ M) (hlbψ : ∃ (m : ℝ), ∀ᶠ (h : ℝ) in nhdsWithin 0 (Set.Ioi 0), m ≤ (ψ (t + h) - ψ t) / h) (hubsum : ∃ (M : ℝ), ∀ᶠ (h : ℝ) in nhdsWithin 0 (Set.Ioi 0), (φ (t + h) + ψ (t + h) - (φ t + ψ t)) / h ≤ M) (hlbsum : ∃ (m : ℝ), ∀ᶠ (h : ℝ) in nhdsWithin 0 (Set.Ioi 0), m ≤ (φ (t + h) + ψ (t + h) - (φ t + ψ t)) / h) : DiniUpper_add_le_pred φ ψ t

Real bridge from the EReal inequality: if all three upper Dini derivatives are finite in EReal (neither ⊤ nor ⊥), then the real-valued additivity upper bound holds.

theorem Frourio.DiniUpper_add_le_pred_of_bounds (φ ψ : ℝ → ℝ) (t : ℝ) (hφ_fin : DiniUpperE φ t ≠ ⊤ ∧ DiniUpperE φ t ≠ ⊥) (hψ_fin : DiniUpperE ψ t ≠ ⊤ ∧ DiniUpperE ψ t ≠ ⊥) (hsum_fin : DiniUpperE (fun (τ : ℝ) => φ τ + ψ τ) t ≠ ⊤ ∧ DiniUpperE (fun (τ : ℝ) => φ τ + ψ τ) t ≠ ⊥) (hubφ : ∃ (M : ℝ), ∀ᶠ (h : ℝ) in nhdsWithin 0 (Set.Ioi 0), (φ (t + h) - φ t) / h ≤ M) (hlbφ : ∃ (m : ℝ), ∀ᶠ (h : ℝ) in nhdsWithin 0 (Set.Ioi 0), m ≤ (φ (t + h) - φ t) / h) (hubψ : ∃ (M : ℝ), ∀ᶠ (h : ℝ) in nhdsWithin 0 (Set.Ioi 0), (ψ (t + h) - ψ t) / h ≤ M) (hlbψ : ∃ (m : ℝ), ∀ᶠ (h : ℝ) in nhdsWithin 0 (Set.Ioi 0), m ≤ (ψ (t + h) - ψ t) / h) (hubsum : ∃ (M : ℝ), ∀ᶠ (h : ℝ) in nhdsWithin 0 (Set.Ioi 0), (φ (t + h) + ψ (t + h) - (φ t + ψ t)) / h ≤ M) (hlbsum : ∃ (m : ℝ), ∀ᶠ (h : ℝ) in nhdsWithin 0 (Set.Ioi 0), m ≤ (φ (t + h) + ψ (t + h) - (φ t + ψ t)) / h) : DiniUpper_add_le_pred φ ψ t

Boundedness付き（上下の eventually 有界）での加法劣加法性。

theorem Frourio.forwardDiff_upper_bound_sum (φ ψ : ℝ → ℝ) (t : ℝ) (hubφ : ∃ (Mφ : ℝ), ∀ᶠ (h : ℝ) in nhdsWithin 0 (Set.Ioi 0), (φ (t + h) - φ t) / h ≤ Mφ) (hubψ : ∃ (Mψ : ℝ), ∀ᶠ (h : ℝ) in nhdsWithin 0 (Set.Ioi 0), (ψ (t + h) - ψ t) / h ≤ Mψ) : ∃ (M : ℝ), ∀ᶠ (h : ℝ) in nhdsWithin 0 (Set.Ioi 0), (φ (t + h) + ψ (t + h) - (φ t + ψ t)) / h ≤ M

Supply an eventual upper bound for the forward difference quotient of a sum from eventual upper bounds of the summands.

theorem Frourio.forwardDiff_lower_bound_sum (φ ψ : ℝ → ℝ) (t : ℝ) (hlbφ : ∃ (mφ : ℝ), ∀ᶠ (h : ℝ) in nhdsWithin 0 (Set.Ioi 0), mφ ≤ (φ (t + h) - φ t) / h) (hlbψ : ∃ (mψ : ℝ), ∀ᶠ (h : ℝ) in nhdsWithin 0 (Set.Ioi 0), mψ ≤ (ψ (t + h) - ψ t) / h) : ∃ (m : ℝ), ∀ᶠ (h : ℝ) in nhdsWithin 0 (Set.Ioi 0), m ≤ (φ (t + h) + ψ (t + h) - (φ t + ψ t)) / h

Supply an eventual lower bound for the forward difference quotient of a sum

theorem Frourio.DiniUpper_add_le_pred_holds (φ ψ : ℝ → ℝ) (t : ℝ) (hφ_fin : DiniUpperE φ t ≠ ⊤ ∧ DiniUpperE φ t ≠ ⊥) (hψ_fin : DiniUpperE ψ t ≠ ⊤ ∧ DiniUpperE ψ t ≠ ⊥) (hsum_fin : DiniUpperE (fun (τ : ℝ) => φ τ + ψ τ) t ≠ ⊤ ∧ DiniUpperE (fun (τ : ℝ) => φ τ + ψ τ) t ≠ ⊥) (hubφ : ∃ (M : ℝ), ∀ᶠ (h : ℝ) in nhdsWithin 0 (Set.Ioi 0), (φ (t + h) - φ t) / h ≤ M) (hlbφ : ∃ (m : ℝ), ∀ᶠ (h : ℝ) in nhdsWithin 0 (Set.Ioi 0), m ≤ (φ (t + h) - φ t) / h) (hubψ : ∃ (M : ℝ), ∀ᶠ (h : ℝ) in nhdsWithin 0 (Set.Ioi 0), (ψ (t + h) - ψ t) / h ≤ M) (hlbψ : ∃ (m : ℝ), ∀ᶠ (h : ℝ) in nhdsWithin 0 (Set.Ioi 0), m ≤ (ψ (t + h) - ψ t) / h) (hubsum : ∃ (M : ℝ), ∀ᶠ (h : ℝ) in nhdsWithin 0 (Set.Ioi 0), (φ (t + h) + ψ (t + h) - (φ t + ψ t)) / h ≤ M) (hlbsum : ∃ (m : ℝ), ∀ᶠ (h : ℝ) in nhdsWithin 0 (Set.Ioi 0), m ≤ (φ (t + h) + ψ (t + h) - (φ t + ψ t)) / h) : DiniUpper_add_le_pred φ ψ t

def Frourio.gronwall_exponential_contraction_pred (lam : ℝ) (W : ℝ → ℝ) : Prop

Gronwall-type exponential bound (statement): if a nonnegative function W satisfies a linear differential inequality in the upper Dini sense, then it contracts exponentially. Used to derive EVI contraction. This is a statement-only placeholder at this phase.

Equations

• Frourio.gronwall_exponential_contraction_pred lam W = ((∀ (t : ℝ), Frourio.DiniUpper W t + 2 * lam * W t ≤ 0) → ∀ (t : ℝ), W t ≤ Real.exp (-(2 * lam) * t) * W 0)

def Frourio.gronwall_exponential_contraction_with_error_half_pred (lam η : ℝ) (W : ℝ → ℝ) : Prop

Inhomogeneous Grönwall-type bound (statement)

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Frourio.ContractionProperty P u v = ∀ (t : ℝ), dist (u t) (v t) ≤ Real.exp (-P.lam * t) * dist (u 0) (v 0)

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

Squared-distance version of the contraction property, aligned with the Gronwall inequality that yields an exp (-(2λ) t) decay.

Equations

• Frourio.ContractionPropertySq P u v = ∀ (t : ℝ), Frourio.d2 (u t) (v t) ≤ Real.exp (-(2 * P.lam) * t) * Frourio.d2 (u 0) (v 0)

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

Bridge hypothesis from squared-distance contraction to linear-distance contraction. This encapsulates the usual sqrt-monotonicity and algebraic identities that convert

d2(u t, v t) ≤ exp (-(2λ) t) · d2(u 0, v 0)

into

dist(u t, v t) ≤ exp (-λ t) · dist(u 0, v 0).

At this phase, we keep it as a named predicate to be provided by later analytic lemmas, allowing higher-level theorems to depend only on this bridge without committing to heavy proofs here.

Equations

• Frourio.Hbridge P u v = (Frourio.ContractionPropertySq P u v → Frourio.ContractionProperty P u v)

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

Assumption pack providing a concrete bridge from squared-distance contraction to linear-distance contraction. In later phases this will be constructed from square-root monotonicity and algebraic identities.

• bridge : Hbridge P u v

theorem Frourio.Hbridge_from_assumptions {X : Type u_1} [PseudoMetricSpace X] {P : EVIProblem X} {u v : ℝ → X} (H : BridgeAssumptions P u v) : Hbridge P u v

Extract the bridge from the assumption pack.

Helper lemmas (statement-level) for the bridge

def Frourio.sqrt_d2_dist {X : Type u_1} [PseudoMetricSpace X] (x y : X) : Prop

Square root of the squared distance equals the distance (statement).

Equations

• Frourio.sqrt_d2_dist x y = (√(Frourio.d2 x y) = dist x y)

def Frourio.sqrt_mul_nonneg (a b : ℝ) (_ha : 0 ≤ a) (_hb : 0 ≤ b) : Prop

Factorization of the square root of a product under nonnegativity assumptions (statement). We parameterize the nonnegativity as explicit arguments to align with Real.sqrt_mul.

Equations

• Frourio.sqrt_mul_nonneg a b _ha _hb = (√(a * b) = √a * √b)

def Frourio.sqrt_exp_halves (x : ℝ) : Prop

Square root of an exponential halves the exponent (statement).

Equations

• Frourio.sqrt_exp_halves x = (√(Real.exp x) = Real.exp (x / 2))