theorem Frourio.jko_to_plfa_constant {X : Type u_1} (F : X → ℝ) : JKO_to_PLFA_pred F

Constant JKO→PLFA: from any initial point and a JKO initializer, produce a PLFA curve by taking the constant curve. This provides a minimizing-movement route without using the JKO witness.

MM-limit route (real-analytic flags)

noncomputable def Frourio.FqR : ℝ → ℝ

Quadratic energy on ℝ: Fq x = (1/2) x^2.

Equations

• Frourio.FqR x = 1 / 2 * x ^ 2

theorem Frourio.quadratic_halfConvex (lamEff : ℝ) : HalfConvex FqR lamEff

Trivial HalfConvex for FqR (placeholder flags: choose c = 0).

theorem Frourio.quadratic_strongUpperBound : StrongUpperBound FqR

Trivial StrongUpperBound for FqR (placeholder flags: choose c = 0).

theorem Frourio.ede_to_evi_quadratic_from_builder (lamEff : ℝ) (H : EDE_EVI_from_analytic_flags FqR lamEff) (ρ : ℝ → ℝ) : EDE FqR ρ → IsEVISolution { E := FqR, lam := lamEff } ρ

From an EDE⇔EVI builder on analytic flags, derive EDE → EVI for the quadratic energy on ℝ using the core flags.

theorem Frourio.ede_to_plfa_from_real_flags {X : Type u_1} [PseudoMetricSpace X] (F : X → ℝ) (lamEff : ℝ) (flags : AnalyticFlagsReal X F lamEff) (h_usc : ∀ (ρ : ℝ → X), ShiftedUSCHypothesis F ρ) (ρ : ℝ → X) : EDE F ρ → PLFA F ρ

EDE → PLFA under real analytic flags with USC hypothesis (convenience bridge). Uses the PLFACore real-flags builder and extracts the backward direction.

theorem Frourio.plfa_to_ede_from_real_flags {X : Type u_1} [PseudoMetricSpace X] (F : X → ℝ) (lamEff : ℝ) (flags : AnalyticFlagsReal X F lamEff) (h_usc : ∀ (ρ : ℝ → X), ShiftedUSCHypothesis F ρ) (ρ : ℝ → X) : PLFA F ρ → EDE F ρ

PLFA → EDE under real analytic flags with USC hypothesis (convenience bridge). Uses the PLFACore real-flags builder and extracts the forward direction.

theorem Frourio.jko_to_plfa_from_real_flags {X : Type u_1} [PseudoMetricSpace X] (F : X → ℝ) (lamEff : ℝ) (flags : AnalyticFlagsReal X F lamEff) : JKO_to_PLFA_pred F

JKO initializer → PLFA under real analytic flags (convenience).

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

From a minimizing-movement construction with real analytic flags, derive the PLFA bound (energy nonincreasing) for curves obtained in the continuous-time limit. This is a wrapper delegating to the real-flags JKO→PLFA route.

Equations

• Frourio.plfa_from_mm_limit F lamEff = ∀ (a : Frourio.AnalyticFlagsReal X F lamEff), Frourio.JKO_to_PLFA_pred F

theorem Frourio.plfa_from_mm_limit_impl {X : Type u_1} [PseudoMetricSpace X] (F : X → ℝ) (lamEff : ℝ) : plfa_from_mm_limit F lamEff

Implementation of plfa_from_mm_limit via the real-flags bridge.

theorem Frourio.ede_to_evi_from_flags_auto {X : Type u_1} [PseudoMetricSpace X] (F : X → ℝ) (lamEff : ℝ) (HC : HalfConvex F lamEff) (SUB : StrongUpperBound F) (H : EDE_EVI_from_analytic_flags F lamEff) : EDE_to_EVI_from_flags F lamEff

Auto directional bridges from analytic flags builder: forward (EDE → EVI). Supply core flags HalfConvex and StrongUpperBound and an EDE_EVI_from_analytic_flags builder to obtain the forward directional bridge.

theorem Frourio.evi_to_ede_from_flags_auto {X : Type u_1} [PseudoMetricSpace X] (F : X → ℝ) (lamEff : ℝ) (HC : HalfConvex F lamEff) (SUB : StrongUpperBound F) (H : EDE_EVI_from_analytic_flags F lamEff) : EVI_to_EDE_from_flags F lamEff

Auto directional bridges from analytic flags builder: backward (EVI → EDE).

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

From real analytic flags, and an EDE⇔EVI builder on placeholder flags, obtain the EDE⇔EVI predicate along the MM (real) route.

Equations

• Frourio.ede_evi_from_mm F lamEff = ∀ (a : Frourio.AnalyticFlagsReal X F lamEff), Frourio.EDE_EVI_pred F lamEff

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

Implementation: convert real flags to placeholder flags and apply the EDE⇔EVI builder on analytic flags.

theorem Frourio.plfaEdeEviJko_equiv_real {X : Type u_1} [PseudoMetricSpace X] (F : X → ℝ) (lamEff : ℝ) (flags : AnalyticFlagsReal X F lamEff) (h_usc : ∀ (ρ : ℝ → X), ShiftedUSCHypothesis F ρ) (HplfaEde : PLFA_EDE_from_real_flags F lamEff) (HedeEvi_builder : EDE_EVI_from_analytic_flags F lamEff) (HjkoPlfa : JKO_PLFA_from_real_flags F lamEff) : plfaEdeEviJko_equiv F lamEff

Real‑route full equivalence: using real analytic flags along with the PLFA/EDE and JKO→PLFA real‑bridges, and an EDE⇔EVI builder on placeholder flags.