Proofs for the helper lemmas

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

theorem Frourio.sqrt_mul_nonneg_prop (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) : sqrt_mul_nonneg a b ha hb

theorem Frourio.sqrt_exp_halves_prop (x : ℝ) : sqrt_exp_halves x

theorem Frourio.sqrt_add_le_sqrt_add_sqrt_prop (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) : √(a + b) ≤ √a + √b

Subadditivity surrogate: for nonnegative a, b, √(a + b) ≤ √a + √b.

theorem Frourio.DiniUpper_add_le (φ ψ : ℝ → ℝ) (t : ℝ) (H : DiniUpper_add_le_pred φ ψ t) : DiniUpper (fun (τ : ℝ) => φ τ + ψ τ) t ≤ DiniUpper φ t + DiniUpper ψ t

DiniUpper additivity upper bound (wrapper theorem from the predicate).

theorem Frourio.DiniUpper_timeRescale (σ : ℝ) (φ : ℝ → ℝ) (t : ℝ) (H : DiniUpper_timeRescale_pred σ φ t) : DiniUpper (fun (τ : ℝ) => φ (σ * τ)) t = σ * DiniUpper φ (σ * t)

Time-rescaling rule for DiniUpper (wrapper theorem from the predicate).

theorem Frourio.DiniUpper_timeRescale_pos (σ : ℝ) (hσ : 0 < σ) (φ : ℝ → ℝ) (t : ℝ) (H : DiniUpper_timeRescale_pred σ φ t) : DiniUpper (fun (τ : ℝ) => φ (σ * τ)) t = σ * DiniUpper φ (σ * t)

Time-rescaling for the upper Dini derivative under a positive factor. This is a wrapper that records the σ > 0 use‑site while delegating the analytical content to the supplied predicate DiniUpper_timeRescale_pred. In later phases, we will provide a proof under mild boundedness hypotheses.

theorem Frourio.gronwall_exponential_contraction_from_pred (lam : ℝ) (W : ℝ → ℝ) (Hpred : gronwall_exponential_contraction_pred lam W) (Hineq : ∀ (t : ℝ), DiniUpper W t + 2 * lam * W t ≤ 0) (t : ℝ) : W t ≤ Real.exp (-(2 * lam) * t) * W 0

Homogeneous Grönwall inequality (turn the predicate into a usable bound).

theorem Frourio.gronwall_exponential_contraction (lam : ℝ) (W : ℝ → ℝ) (Hpred : gronwall_exponential_contraction_pred lam W) (Hineq : ∀ (t : ℝ), DiniUpper W t + 2 * lam * W t ≤ 0) (t : ℝ) : W t ≤ Real.exp (-(2 * lam) * t) * W 0

Homogeneous Grönwall inequality (wrapper using the predicate).

theorem Frourio.gronwall_exponential_contraction_with_error_half_from_pred (lam η : ℝ) (W : ℝ → ℝ) (Hpred : gronwall_exponential_contraction_with_error_half_pred lam η W) (Hineq : ∀ (t : ℝ), 1 / 2 * DiniUpper W t + lam * W t ≤ η) (t : ℝ) : W t ≤ Real.exp (-(2 * lam) * t) * W 0 + 2 * η * t

Inhomogeneous Grönwall inequality (turn the predicate into a usable bound).

theorem Frourio.gronwall_exponential_contraction_with_error_half (lam η : ℝ) (W : ℝ → ℝ) (Hpred : gronwall_exponential_contraction_with_error_half_pred lam η W) (Hineq : ∀ (t : ℝ), 1 / 2 * DiniUpper W t + lam * W t ≤ η) (t : ℝ) : W t ≤ Real.exp (-(2 * lam) * t) * W 0 + 2 * η * t

Inhomogeneous Grönwall inequality in the half form (wrapper using the predicate).

theorem Frourio.gronwall_exponential_contraction_with_error_half_core (lam η : ℝ) (W : ℝ → ℝ) (H : gronwall_exponential_contraction_with_error_half_pred lam η W) (Hineq : ∀ (t : ℝ), 1 / 2 * DiniUpper W t + lam * W t ≤ η) (t : ℝ) : W t ≤ Real.exp (-(2 * lam) * t) * W 0 + 2 * η * t

Inhomogeneous Grönwall inequality (half form, core statement): If (1/2)·DiniUpper W + lam·W ≤ η pointwise, then W t ≤ exp (-(2 lam) t) · W 0 + (2 η) t.

theorem Frourio.DiniUpper_timeRescale_one (φ : ℝ → ℝ) (t : ℝ) : DiniUpper (fun (τ : ℝ) => φ (1 * τ)) t = 1 * DiniUpper φ (1 * t)

Special case: time-reparameterization with unit factor is tautological.

theorem Frourio.gronwall_exponential_contraction_zero (W : ℝ → ℝ) (H : gronwall_exponential_contraction_pred 0 W) (Hineq0 : ∀ (t : ℝ), DiniUpper W t ≤ 0) (t : ℝ) : W t ≤ W 0

Special case of homogeneous Grönwall at λ = 0 using a provided predicate.

theorem Frourio.gronwall_exponential_contraction_with_error_zero (lam : ℝ) (W : ℝ → ℝ) (H : (∀ (t : ℝ), 1 / 2 * DiniUpper W t + lam * W t ≤ 0) → ∀ (t : ℝ), W t ≤ Real.exp (-(2 * lam) * t) * W 0) (Hineq0 : ∀ (t : ℝ), 1 / 2 * DiniUpper W t + lam * W t ≤ 0) (t : ℝ) : W t ≤ Real.exp (-(2 * lam) * t) * W 0

Special case of inhomogeneous Grönwall at η = 0 using a provided predicate.

theorem Frourio.gronwall_exponential_contraction_core (lam : ℝ) (W : ℝ → ℝ) (H : gronwall_exponential_contraction_pred lam W) (Hineq : ∀ (t : ℝ), DiniUpper W t + 2 * lam * W t ≤ 0) (t : ℝ) : W t ≤ Real.exp (-(2 * lam) * t) * W 0

Homogeneous Grönwall inequality (core theorem): If (DiniUpper W) + (2 λ) W ≤ 0 pointwise, then W t ≤ exp (-(2 λ) t) · W 0.

theorem Frourio.gronwall_zero (W : ℝ → ℝ) (H : gronwall_exponential_contraction_pred 0 W) (Hineq0 : ∀ (t : ℝ), DiniUpper W t ≤ 0) (t : ℝ) : W t ≤ W 0

Homogeneous Grönwall at λ = 0 (direct form): If DiniUpper W ≤ 0 pointwise, then W is nonincreasing: W t ≤ W 0.

theorem Frourio.bridge_contraction {X : Type u_1} [PseudoMetricSpace X] (P : EVIProblem X) (u v : ℝ → X) (H : Hbridge P u v) (hSq : ContractionPropertySq P u v) : ContractionProperty P u v

Concrete bridge from squared-distance contraction to linear-distance contraction using monotonicity of Real.sqrt and algebraic identities.