A compact notation for the concrete forward/backward bridges.

def Frourio.HF {X : Type u_1} [PseudoMetricSpace X] (F : X → ℝ) (lamEff : ℝ) : Prop

Equations

• Frourio.HF F lamEff = Frourio.EDE_to_EVI_concrete F lamEff

def Frourio.HB {X : Type u_1} [PseudoMetricSpace X] (F : X → ℝ) (lamEff : ℝ) : Prop

Equations

• Frourio.HB F lamEff = Frourio.EVI_to_EDE_concrete F lamEff

theorem Frourio.HF_from_pred {X : Type u_1} [PseudoMetricSpace X] (F : X → ℝ) (lamEff : ℝ) (Hpred : EDE_EVI_pred F lamEff) : HF F lamEff

Build HF from a pointwise equivalence predicate.

theorem Frourio.HB_from_pred {X : Type u_1} [PseudoMetricSpace X] (F : X → ℝ) (lamEff : ℝ) (Hpred : EDE_EVI_pred F lamEff) : HB F lamEff

Build HB from a pointwise equivalence predicate.

theorem Frourio.HF_from_pack {X : Type u_1} [PseudoMetricSpace X] (F : X → ℝ) (lamEff : ℝ) (H : EDEEVIAssumptions F lamEff) : HF F lamEff

Build HF from an EDEEVIAssumptions pack.

theorem Frourio.HB_from_pack {X : Type u_1} [PseudoMetricSpace X] (F : X → ℝ) (lamEff : ℝ) (H : EDEEVIAssumptions F lamEff) : HB F lamEff

Build HB from an EDEEVIAssumptions pack.

theorem Frourio.HF_from_global {X : Type u_1} [PseudoMetricSpace X] (F : X → ℝ) (lamEff : ℝ) (G : plfaEdeEviJko_equiv F lamEff) : HF F lamEff

Build HF from a global equivalence package.

theorem Frourio.HB_from_global {X : Type u_1} [PseudoMetricSpace X] (F : X → ℝ) (lamEff : ℝ) (G : plfaEdeEviJko_equiv F lamEff) : HB F lamEff

Build HB from a global equivalence package.

theorem Frourio.HF_from_flags_builder {X : Type u_1} [PseudoMetricSpace X] (F : X → ℝ) (lamEff : ℝ) (A : AnalyticFlags F lamEff) (H : EDE_EVI_from_analytic_flags F lamEff) : HF F lamEff

Build HF from analytic flags and a builder.

theorem Frourio.HB_from_flags_builder {X : Type u_1} [PseudoMetricSpace X] (F : X → ℝ) (lamEff : ℝ) (A : AnalyticFlags F lamEff) (H : EDE_EVI_from_analytic_flags F lamEff) : HB F lamEff

Build HB from analytic flags and a builder.

theorem Frourio.ede_evi_builder_from_HF_HB {X : Type u_1} [PseudoMetricSpace X] (F : X → ℝ) (lamEff : ℝ) (hF : HF F lamEff) (hB : HB F lamEff) : EDE_EVI_from_analytic_flags F lamEff

If both HF and HB hold, assemble the final builder.

def Frourio.EDE_EVI_short_input {X : Type u_1} [PseudoMetricSpace X] (F : X → ℝ) (lamEff : ℝ) : Prop

Shortcut input for building EDE_EVI_from_analytic_flags: either a global equivalence pack, or both concrete bridges.

Equations

• Frourio.EDE_EVI_short_input F lamEff = (Frourio.plfaEdeEviJko_equiv F lamEff ∨ Frourio.EDE_to_EVI_concrete F lamEff ∧ Frourio.EVI_to_EDE_concrete F lamEff)

theorem Frourio.ede_evi_from_short_input {X : Type u_1} [PseudoMetricSpace X] (F : X → ℝ) (lamEff : ℝ) (Hin : EDE_EVI_short_input F lamEff) : EDE_EVI_from_analytic_flags F lamEff

Build EDE_EVI_from_analytic_flags from the shortest available input.

theorem Frourio.ede_evi_from_pred_short {X : Type u_1} [PseudoMetricSpace X] (F : X → ℝ) (lamEff : ℝ) (Hpred : EDE_EVI_pred F lamEff) : EDE_EVI_from_analytic_flags F lamEff

From a pointwise EDE_EVI_pred, directly build the flags‑builder by materializing both concrete bridges then assembling them.

theorem Frourio.ede_evi_from_pack_short {X : Type u_1} [PseudoMetricSpace X] (F : X → ℝ) (lamEff : ℝ) (H : EDEEVIAssumptions F lamEff) : EDE_EVI_from_analytic_flags F lamEff

From an EDEEVIAssumptions pack (i.e., EDE⇔EVI pointwise), build the flags‑builder.

structure Frourio.AnalyticBridges {X : Type u_1} [PseudoMetricSpace X] (F : X → ℝ) (lamEff : ℝ) : Prop

• plfaEde : PLFA_EDE_from_analytic_flags F lamEff
• edeEvi : EDE_EVI_from_analytic_flags F lamEff
• jkoPlfa : JKO_PLFA_from_analytic_flags F

theorem Frourio.build_package_from_flags_and_bridges {X : Type u_1} [PseudoMetricSpace X] (F : X → ℝ) (lamEff : ℝ) (A : AnalyticFlags F lamEff) (B : AnalyticBridges F lamEff) : plfaEdeEviJko_equiv F lamEff

theorem Frourio.plfaEdeEviJko_equiv_from_flags {X : Type u_1} [PseudoMetricSpace X] (F : X → ℝ) (lamEff : ℝ) (H1 : PLFA_EDE_from_analytic_flags F lamEff) (H2 : EDE_EVI_from_analytic_flags F lamEff) (H3 : JKO_PLFA_from_analytic_flags F) (A : AnalyticFlags F lamEff) : plfaEdeEviJko_equiv F lamEff

theorem Frourio.global_sufficient_pack_from_flags_and_ede_evi_pack {X : Type u_1} [PseudoMetricSpace X] (F : X → ℝ) (lamEff : ℝ) (A : AnalyticFlags F lamEff) (HplfaEde : PLFA_EDE_from_analytic_flags F lamEff) (HedeEviPack : EDEEVIAssumptions F lamEff) (HjkoPlfa : JKO_PLFA_from_analytic_flags F) : GlobalSufficientPack F lamEff

Assemble a GlobalSufficientPack directly from core flags and an EDEEVIAssumptions pack (EDE ⇔ EVI), alongside the non-metric builders.

theorem Frourio.build_package_from_flags_and_ede_evi_pack {X : Type u_1} [PseudoMetricSpace X] (F : X → ℝ) (lamEff : ℝ) (A : AnalyticFlags F lamEff) (HplfaEde : PLFA_EDE_from_analytic_flags F lamEff) (HedeEviPack : EDEEVIAssumptions F lamEff) (HjkoPlfa : JKO_PLFA_from_analytic_flags F) : plfaEdeEviJko_equiv F lamEff

Build the full equivalence from flags, EDE⇔EVI pack, and non-metric builders.

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

Equations

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

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

Shared geodesic uniform evaluation predicate specialized to P.

Equations

• Frourio.GeodesicUniformEvalFor P u v = Frourio.GeodesicUniformEval P u v

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

Variant of TwoEVIWithForce that uses the shared geodesic predicate.

Equations

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

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

From the shared predicate variant, recover the original TwoEVIWithForce.

theorem Frourio.twoEVIWithForce_to_distance {X : Type u_1} [PseudoMetricSpace X] (P : EVIProblem X) (u v : ℝ → X) (H : TwoEVIWithForce P u v) (Hbridge : ∀ (η : ℝ), HbridgeWithError P u v η) : ∃ (η : ℝ), (gronwall_exponential_contraction_with_error_half_pred P.lam η fun (t : ℝ) => d2 (u t) (v t)) → ContractionPropertyWithError P u v η

theorem Frourio.twoEVIWithForceShared_to_distance {X : Type u_1} [PseudoMetricSpace X] (P : EVIProblem X) (u v : ℝ → X) (H : TwoEVIWithForceShared P u v) (Hbridge : ∀ (η : ℝ), HbridgeWithError P u v η) : ∃ (η : ℝ), (gronwall_exponential_contraction_with_error_half_pred P.lam η fun (t : ℝ) => d2 (u t) (v t)) → ContractionPropertyWithError P u v η

Shared variant: distance synchronization from TwoEVIWithForceShared.

theorem Frourio.twoEVIWithForce_to_distance_closed {X : Type u_1} [PseudoMetricSpace X] (P : EVIProblem X) (u v : ℝ → X) (H : TwoEVIWithForce P u v) (Hgr_all : ∀ (η : ℝ), gronwall_exponential_contraction_with_error_half_pred P.lam η fun (t : ℝ) => d2 (u t) (v t)) (Hbridge : ∀ (η : ℝ), HbridgeWithError P u v η) : ∃ (η : ℝ), ContractionPropertyWithError P u v η

theorem Frourio.twoEVIWithForceShared_to_distance_closed {X : Type u_1} [PseudoMetricSpace X] (P : EVIProblem X) (u v : ℝ → X) (H : TwoEVIWithForceShared P u v) (Hgr_all : ∀ (η : ℝ), gronwall_exponential_contraction_with_error_half_pred P.lam η fun (t : ℝ) => d2 (u t) (v t)) (Hbridge : ∀ (η : ℝ), HbridgeWithError P u v η) : ∃ (η : ℝ), ContractionPropertyWithError P u v η

Shared variant: closed distance synchronization from TwoEVIWithForceShared.

theorem Frourio.twoEVIWithForce_to_distance_concrete {X : Type u_1} [PseudoMetricSpace X] (P : EVIProblem X) (u v : ℝ → X) (H : TwoEVIWithForce P u v) : ∃ (η : ℝ), (gronwall_exponential_contraction_with_error_half_pred P.lam η fun (t : ℝ) => d2 (u t) (v t)) → ContractionPropertyWithError P u v η

Two‑EVI with force: distance synchronization using the concrete with‑error bridge from EVI.lean (no external bridge hypothesis needed).

theorem Frourio.twoEVIWithForceShared_to_distance_concrete {X : Type u_1} [PseudoMetricSpace X] (P : EVIProblem X) (u v : ℝ → X) (H : TwoEVIWithForceShared P u v) : ∃ (η : ℝ), (gronwall_exponential_contraction_with_error_half_pred P.lam η fun (t : ℝ) => d2 (u t) (v t)) → ContractionPropertyWithError P u v η

Shared variant: distance synchronization using the concrete with‑error bridge from EVI.lean (no external bridge hypothesis needed).

theorem Frourio.twoEVIWithForce_to_distance_concrete_closed {X : Type u_1} [PseudoMetricSpace X] (P : EVIProblem X) (u v : ℝ → X) (H : TwoEVIWithForce P u v) (Hgr_all : ∀ (η : ℝ), gronwall_exponential_contraction_with_error_half_pred P.lam η fun (t : ℝ) => d2 (u t) (v t)) : ∃ (η : ℝ), ContractionPropertyWithError P u v η

Closed form: if a Grönwall predicate holds for all η, then the two‑EVI with force yields a distance synchronization bound via the concrete bridge.

theorem Frourio.twoEVIWithForceShared_to_distance_concrete_closed {X : Type u_1} [PseudoMetricSpace X] (P : EVIProblem X) (u v : ℝ → X) (H : TwoEVIWithForceShared P u v) (Hgr_all : ∀ (η : ℝ), gronwall_exponential_contraction_with_error_half_pred P.lam η fun (t : ℝ) => d2 (u t) (v t)) : ∃ (η : ℝ), ContractionPropertyWithError P u v η

Shared variant: closed form of the concrete with‑error synchronization.

theorem Frourio.ede_iff_evi {X : Type u_1} [PseudoMetricSpace X] (F : X → ℝ) (lamEff : ℝ) (G : plfaEdeEviJko_equiv F lamEff) (ρ : ℝ → X) : EDE F ρ ↔ IsEVISolution { E := F, lam := lamEff } ρ

theorem Frourio.evi_iff_plfa {X : Type u_1} [PseudoMetricSpace X] (F : X → ℝ) (lamEff : ℝ) (G : plfaEdeEviJko_equiv F lamEff) (ρ : ℝ → X) : IsEVISolution { E := F, lam := lamEff } ρ ↔ PLFA F ρ

theorem Frourio.jko_to_evi {X : Type u_1} [PseudoMetricSpace X] (F : X → ℝ) (lamEff : ℝ) (G : plfaEdeEviJko_equiv F lamEff) (ρ0 : X) : JKO F ρ0 → ∃ (ρ : ℝ → X), ρ 0 = ρ0 ∧ IsEVISolution { E := F, lam := lamEff } ρ