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

Concrete bridge from squared-distance to linear-distance contraction. It combines sqrt_d2_dist_prop, sqrt_mul_nonneg_prop, and sqrt_exp_halves_prop with Real.sqrt_le_sqrt to pass to distances.

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

Pack the concrete bridge as an Hbridge.

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

Equations

• Frourio.eviContraction P u v _hu _hv = Frourio.ContractionProperty P u v

@[reducible, inline]

abbrev Frourio.evi_contraction {X : Type u_1} [PseudoMetricSpace X] (P : EVIProblem X) (u v : ℝ → X) (hu : IsEVISolution P u) (hv : IsEVISolution P v) : Prop

Equations

• Frourio.evi_contraction P u v hu hv = Frourio.eviContraction P u v hu hv

theorem Frourio.evi_contraction_self {X : Type u_1} [PseudoMetricSpace X] (P : EVIProblem X) (u : ℝ → X) (_hu : IsEVISolution P u) : ContractionProperty P u u

EVI contraction (self-curve special case).

Proof sketch: For any curve u, the contraction inequality against itself reduces to 0 ≤ exp(-λ t) * 0, since dist (u t) (u t) = 0 = dist (u 0) (u 0). Thus the desired inequality holds by reflexivity of ≤ on 0.

This serves as a minimal, fully formal base case toward the full EVI contraction proof (Gronwall-based) developed in later phases.

theorem Frourio.evi_contraction_sq_from_gronwall {X : Type u_1} [PseudoMetricSpace X] (P : EVIProblem X) (u v : ℝ → X) (_hu : IsEVISolution P u) (_hv : IsEVISolution P v) (Hineq2 : ∀ (t : ℝ), DiniUpper (fun (τ : ℝ) => d2 (u τ) (v τ)) t + 2 * P.lam * d2 (u t) (v t) ≤ 0) (Hgr : gronwall_exponential_contraction_pred P.lam fun (t : ℝ) => d2 (u t) (v t)) : ContractionPropertySq P u v

If the upper Dini differential inequality holds for the squared distance and we have a Gronwall-type exponential contraction lemma for a function W, then we obtain the squared-distance contraction property. This bridges the EVI inequality to a ready-to-use decay statement without performing the sqrt-step to linear distance yet.

theorem Frourio.eviContraction_general {X : Type u_1} [PseudoMetricSpace X] (P : EVIProblem X) (u v : ℝ → X) (hu : IsEVISolution P u) (hv : IsEVISolution P v) (Hineq2 : ∀ (t : ℝ), DiniUpper (fun (τ : ℝ) => d2 (u τ) (v τ)) t + 2 * P.lam * d2 (u t) (v t) ≤ 0) (Hgr : gronwall_exponential_contraction_pred P.lam fun (t : ℝ) => d2 (u t) (v t)) (Hbridge : Hbridge P u v) : ContractionProperty P u v

Final general contraction theorem via a bridge from squared to linear distances. Given the squared-distance contraction and a user-provided bridge that converts it to the linear-distance statement (using monotonicity of sqrt and algebraic identities), we obtain the desired contraction property.

theorem Frourio.eviContraction_thm {X : Type u_1} [PseudoMetricSpace X] (P : EVIProblem X) (u v : ℝ → X) (hu : IsEVISolution P u) (hv : IsEVISolution P v) (Hineq2 : ∀ (t : ℝ), DiniUpper (fun (τ : ℝ) => d2 (u τ) (v τ)) t + 2 * P.lam * d2 (u t) (v t) ≤ 0) (Hgr : gronwall_exponential_contraction_pred P.lam fun (t : ℝ) => d2 (u t) (v t)) (Hbridge : Hbridge P u v) : ContractionProperty P u v

EVI contraction (named theorem form, P0 skeleton).

Proof strategy: Assume the squared-distance Dini inequality and a Grönwall exponential decay statement for W t = d2 (u t) (v t). This yields a ContractionPropertySq. A bridge hypothesis converts it into the linear ContractionProperty. Heavy analytic parts are abstracted as inputs.

theorem Frourio.evi_contraction_thm_concrete {X : Type u_1} [PseudoMetricSpace X] (P : EVIProblem X) (u v : ℝ → X) (hu : IsEVISolution P u) (hv : IsEVISolution P v) (Hineq2 : ∀ (t : ℝ), DiniUpper (fun (τ : ℝ) => d2 (u τ) (v τ)) t + 2 * P.lam * d2 (u t) (v t) ≤ 0) (Hgr : gronwall_exponential_contraction_pred P.lam fun (t : ℝ) => d2 (u t) (v t)) : ContractionProperty P u v

Concrete EVI contraction wrapper (closed via G1 + B1).

Given the squared-distance differential inequality for W t = d2(u t, v t) and the Grönwall predicate gronwall_exponential_contraction_pred, this derives the linear-distance contraction using the concrete bridge bridge_contraction_concrete.

This closes the contraction pipeline without requiring an external Hbridge argument.

structure Frourio.MixedErrorBound (X : Type u_1) [PseudoMetricSpace X] (u v : ℝ → X) : Type

• η : ℝ
• bound (_t : ℝ) : Prop

def Frourio.eviSumWithError {X : Type u_1} [PseudoMetricSpace X] (P : EVIProblem X) (u v : ℝ → X) (_hu : IsEVISolution P u) (_hv : IsEVISolution P v) (_geodesicBetween : Prop) (hR : MixedErrorBound X u v) : Prop

Equations

• Frourio.eviSumWithError P u v _hu _hv _geodesicBetween hR = ∀ (t : ℝ), 1 / 2 * Frourio.DiniUpper (fun (τ : ℝ) => Frourio.d2 (u τ) (v τ)) t + P.lam * Frourio.d2 (u t) (v t) ≤ hR.η

def Frourio.eviSumNoError {X : Type u_1} [PseudoMetricSpace X] (P : EVIProblem X) (u v : ℝ → X) (_hu : IsEVISolution P u) (_hv : IsEVISolution P v) (_geodesicBetween : Prop) : Prop

Mixed EVI sum without error (half form): expected output of the "add-and-absorb-cross-terms" step when the geometry yields no residual error.

Equations

• Frourio.eviSumNoError P u v _hu _hv _geodesicBetween = ∀ (t : ℝ), 1 / 2 * Frourio.DiniUpper (fun (τ : ℝ) => Frourio.d2 (u τ) (v τ)) t + P.lam * Frourio.d2 (u t) (v t) ≤ 0

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

Squared-distance synchronization with error (P0 skeleton).

Assume a mixed EVI inequality with error term η for W t = d2(u t, v t) and an inhomogeneous Grönwall lemma. Then

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

Bridging to linear distance can be added separately via a dedicated lemma.

Equations

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

theorem Frourio.eviSynchronizationSq_with_error {X : Type u_1} [PseudoMetricSpace X] (P : EVIProblem X) (u v : ℝ → X) (hu : IsEVISolution P u) (hv : IsEVISolution P v) (_geodesicBetween : Prop) (hR : MixedErrorBound X u v) (Hsum : eviSumWithError P u v hu hv _geodesicBetween hR) (Hgr : (∀ (t : ℝ), 1 / 2 * DiniUpper (fun (τ : ℝ) => d2 (u τ) (v τ)) t + P.lam * d2 (u t) (v t) ≤ hR.η) → ∀ (t : ℝ), d2 (u t) (v t) ≤ Real.exp (-(2 * P.lam) * t) * d2 (u 0) (v 0) + 2 * hR.η * t) : ContractionPropertySqWithError P u v hR.η

Synchronization with error in squared distance via inhomogeneous Grönwall.