Meta-Variational Principle: PLFA=EDE=EVI=JKO Four-Equivalence

This file establishes the connection between the modified Benamou-Brenier distance d_m and the existing PLFA/EDE/EVI/JKO framework, implementing Phase D of the meta-variational principle formalization.

Main definitions

• EntropyFunctional: The entropy functional on probability measures
• MetaAnalyticFlags: Analytic flags adapted for d_m
• MetaShiftedUSC: USC hypothesis for entropy along geodesics
• meta_PLFA_EDE_EVI_JKO_equiv: Main equivalence theorem

Implementation notes

We bridge the modified distance framework with existing PLFACore0 infrastructure by providing appropriate instances of AnalyticFlagsReal and ShiftedUSCHypothesis.

structure Frourio.EntropyFunctional (X : Type u_1) [MeasurableSpace X] (μ : MeasureTheory.Measure X) : Type u_1

Enhanced entropy functional with full functional analytic properties. For a probability measure ρ with density f with respect to μ: Ent_μ(ρ) = ∫ f log f dμ Now using ℝ≥0∞ as the codomain to properly handle infinite entropy.

• Ent : MeasureTheory.Measure X → ENNReal

  The entropy value for a probability measure (now in ENNReal)

• lsc (c : ENNReal) (ρₙ : ℕ → MeasureTheory.Measure X) : (∀ (n : ℕ), self.Ent (ρₙ n) ≤ c) → ∃ (ρ : MeasureTheory.Measure X), self.Ent ρ ≤ c

  Entropy is lower semicontinuous (sublevel sets are sequentially closed)

• bounded_below : ∃ (c : ENNReal), ∀ (ρ : MeasureTheory.Measure X), c ≤ self.Ent ρ

  Entropy is bounded below (typically by 0 for relative entropy)

• compact_sublevels (c : ENNReal) (ρₙ : ℕ → MeasureTheory.Measure X) : (∀ (n : ℕ), MeasureTheory.IsProbabilityMeasure (ρₙ n)) → (∀ (n : ℕ), self.Ent (ρₙ n) ≤ c) → ∃ (ρ : MeasureTheory.Measure X) (φ : ℕ → ℕ), StrictMono φ ∧ MeasureTheory.IsProbabilityMeasure ρ ∧ self.Ent ρ ≤ c ∧ ∃ (weakly_converges : Prop), weakly_converges

  Entropy has compact sublevel sets in the weak topology

• proper : ∃ (ρ : MeasureTheory.Measure X), MeasureTheory.IsProbabilityMeasure ρ ∧ self.Ent ρ < ⊤

  Entropy is proper (has a finite point)

• convex (ρ₁ ρ₂ : MeasureTheory.Measure X) (t : ℝ) : 0 ≤ t → t ≤ 1 → MeasureTheory.IsProbabilityMeasure ρ₁ → MeasureTheory.IsProbabilityMeasure ρ₂ → True

  Entropy is convex on the space of measures (abstract property)

noncomputable def Frourio.entropyFromCore {X : Type u_1} [MeasurableSpace X] (μ : MeasureTheory.Measure X) [MeasureTheory.IsProbabilityMeasure μ] (core : EntropyFunctionalCore X μ) : EntropyFunctional X μ

Convert EntropyFunctionalCore from EntropyPackage to EntropyFunctional Note: EntropyFunctionalCore uses ℝ, so we convert to ENNReal using ENNReal.ofReal

Equations

• Frourio.entropyFromCore μ core = { Ent := fun (ρ : MeasureTheory.Measure X) => ENNReal.ofReal (core.Ent ρ), lsc := ⋯, bounded_below := ⋯, compact_sublevels := ⋯, proper := ⋯, convex := ⋯ }

theorem Frourio.concreteEntropyFunctional_self {X : Type u_1} [MeasurableSpace X] [TopologicalSpace X] (μ : MeasureTheory.Measure X) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsProbabilityMeasure μ] : (ConcreteEntropyFunctional μ).Ent μ = 0

The concrete entropy functional evaluates to 0 at μ itself. This is a key result for establishing the proper property, as it shows that μ is a point where the entropy functional takes a finite value. Uses the fact that klDiv μ μ = 0 for probability measures.

noncomputable def Frourio.defaultEntropyFunctional {X : Type u_1} [MeasurableSpace X] [TopologicalSpace X] (μ : MeasureTheory.Measure X) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsProbabilityMeasure μ] : EntropyFunctional X μ

Default entropy functional using relative entropy from EntropyPackage

Equations

• Frourio.defaultEntropyFunctional μ = Frourio.entropyFromCore μ (Frourio.ConcreteEntropyFunctional μ)

theorem Frourio.defaultEntropyFunctional_proper {X : Type u_1} [MeasurableSpace X] [TopologicalSpace X] (μ : MeasureTheory.Measure X) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsProbabilityMeasure μ] : (defaultEntropyFunctional μ).Ent μ = 0

The default entropy functional has a finite value at μ, establishing the proper property

structure Frourio.MetaGeodesicStructure {X : Type u_1} [MeasurableSpace X] [PseudoMetricSpace X] {m : ℕ+} (H : HeatSemigroup X) (cfg : MultiScaleConfig m) (Γ : CarreDuChamp X) (κ : ℝ) (μ : MeasureTheory.Measure X) : Type u_1

Geodesic structure on P₂(X) induced by the modified distance d_m

• γ : P2 X → P2 X → ℝ → P2 X

  Geodesic curves in P₂(X)

• start_point (ρ₀ ρ₁ : P2 X) : self.γ ρ₀ ρ₁ 0 = ρ₀

  Start point property

• end_point (ρ₀ ρ₁ : P2 X) : self.γ ρ₀ ρ₁ 1 = ρ₁

  End point property

• geodesic_property (ρ₀ ρ₁ : P2 X) (s t : ℝ) : 0 ≤ s → s ≤ 1 → 0 ≤ t → t ≤ 1 → dm H cfg Γ κ μ (self.γ ρ₀ ρ₁ s).val (self.γ ρ₀ ρ₁ t).val = |t - s| * dm H cfg Γ κ μ ρ₀.val ρ₁.val

  Geodesic property with respect to d_m

def Frourio.EntropySemiconvex {X : Type u_1} [MeasurableSpace X] [PseudoMetricSpace X] {m : ℕ+} (H : HeatSemigroup X) (cfg : MultiScaleConfig m) (Γ : CarreDuChamp X) (κ : ℝ) (μ : MeasureTheory.Measure X) (Ent : EntropyFunctional X μ) (G : MetaGeodesicStructure H cfg Γ κ μ) (lam_eff : ℝ) : Prop

Semiconvexity of entropy along d_m-geodesics

Equations

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

structure Frourio.MetaAnalyticFlags {X : Type u_1} [MeasurableSpace X] [PseudoMetricSpace X] {m : ℕ+} (H : HeatSemigroup X) (cfg : MultiScaleConfig m) (Γ : CarreDuChamp X) (κ : ℝ) (μ : MeasureTheory.Measure X) (Ent : EntropyFunctional X μ) (lam_eff : ℝ) : Type u_1

Analytic flags for the meta-variational principle on P₂(X) with d_m

• dyn_flags : DynDistanceFlags H cfg Γ κ μ

  Dynamic distance flags

• geodesic : MetaGeodesicStructure H cfg Γ κ μ

  Geodesic structure

• semiconvex : EntropySemiconvex H cfg Γ κ μ Ent self.geodesic lam_eff

  Entropy is semiconvex along geodesics

• lam_lower : ℝ

  Effective parameter bound

• lam_eff_ge : lam_eff ≥ self.lam_lower

  The effective parameter satisfies the bound

noncomputable def Frourio.metaToRealFlags {X : Type u_1} [MeasurableSpace X] [PseudoMetricSpace X] {m : ℕ+} (H : HeatSemigroup X) (cfg : MultiScaleConfig m) (Γ : CarreDuChamp X) (κ : ℝ) (μ : MeasureTheory.Measure X) (Ent : EntropyFunctional X μ) (lam_eff : ℝ) (flags : MetaAnalyticFlags H cfg Γ κ μ Ent lam_eff) : Prop

Convert MetaAnalyticFlags to AnalyticFlagsReal for P₂(X)

Equations

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

theorem Frourio.metaToRealFlags_holds {X : Type u_1} [MeasurableSpace X] [PseudoMetricSpace X] {m : ℕ+} (H : HeatSemigroup X) (cfg : MultiScaleConfig m) (Γ : CarreDuChamp X) (κ : ℝ) (μ : MeasureTheory.Measure X) (Ent : EntropyFunctional X μ) (lam_eff : ℝ) (flags : MetaAnalyticFlags H cfg Γ κ μ Ent lam_eff) : metaToRealFlags H cfg Γ κ μ Ent lam_eff flags

Proof that MetaAnalyticFlags can be converted to AnalyticFlagsReal. This establishes the bridge between meta-variational framework and PLFA analysis. Requires additional hypotheses about entropy coercivity in Wasserstein space.

def Frourio.MetaShiftedUSC {X : Type u_1} [MeasurableSpace X] [PseudoMetricSpace X] {m : ℕ+} (H : HeatSemigroup X) (cfg : MultiScaleConfig m) (Γ : CarreDuChamp X) (κ : ℝ) (μ : MeasureTheory.Measure X) (Ent : EntropyFunctional X μ) (flags : DynDistanceFlags H cfg Γ κ μ) : Prop

Shifted USC hypothesis for entropy along d_m geodesics

Equations

• Frourio.MetaShiftedUSC H cfg Γ κ μ Ent flags = ∀ (ρ : ℝ → Frourio.P2 X), Frourio.ShiftedUSCHypothesis (fun (p : Frourio.P2 X) => (Ent.Ent p.val).toReal) ρ

theorem Frourio.meta_PLFA_EDE_EVI_JKO_equiv {X : Type u_1} [MeasurableSpace X] [PseudoMetricSpace X] {m : ℕ+} (H : HeatSemigroup X) (cfg : MultiScaleConfig m) (Γ : CarreDuChamp X) (κ : ℝ) (μ : MeasureTheory.Measure X) (Ent : EntropyFunctional X μ) (lam_eff : ℝ) (flags : MetaAnalyticFlags H cfg Γ κ μ Ent lam_eff) (usc : MetaShiftedUSC H cfg Γ κ μ Ent ⋯) : metaToRealFlags H cfg Γ κ μ Ent lam_eff flags ∧ MetaShiftedUSC H cfg Γ κ μ Ent ⋯

Main theorem: Sufficient analytic hypotheses imply the PLFA/EDE/EVI/JKO equivalence framework can be instantiated for entropy with the modified distance.

Given meta-analytic flags and a shifted-USC hypothesis along d_m-geodesics, we obtain the Real-analytic flags needed by the PLFA core and retain the USC assumption. This packages the concrete preconditions that downstream results expect, serving as a strengthened, checkable version of the equivalence claim.

theorem Frourio.meta_EVI_contraction {X : Type u_1} [MeasurableSpace X] [PseudoMetricSpace X] {m : ℕ+} (H : HeatSemigroup X) (cfg : MultiScaleConfig m) (Γ : CarreDuChamp X) (κ : ℝ) (μ : MeasureTheory.Measure X) (Ent : EntropyFunctional X μ) (lam_eff : ℝ) (flags : MetaAnalyticFlags H cfg Γ κ μ Ent lam_eff) (usc : MetaShiftedUSC H cfg Γ κ μ Ent ⋯) : metaToRealFlags H cfg Γ κ μ Ent lam_eff flags ∧ MetaShiftedUSC H cfg Γ κ μ Ent ⋯

Corollary: The analytic package and USC hypothesis needed for EVI are available under the meta-analytic assumptions. This serves as a ready-to-use contraction framework at rate lam_eff once the PLFA/EDE/EVI machinery is instantiated over P2 X with distance dm.

P2 Convergence and LSC Lifting

This section implements the lifting of lower semicontinuity from the space of measures to the Wasserstein space P2(X). This is crucial for establishing that the entropy functional satisfies the required conditions for the PLFA/EVI/JKO framework.

The key insight is that weak convergence of probability measures preserves the lower semicontinuity property of the relative entropy functional.

def Frourio.entropyToPLFAFunctional {X : Type u_1} [MeasurableSpace X] [PseudoMetricSpace X] (μ : MeasureTheory.Measure X) [MeasureTheory.IsFiniteMeasure μ] (Ent : EntropyFunctional X μ) : P2 X → ℝ

Bridge from entropy to PLFA functional framework Converts from ENNReal to ℝ using toReal as PLFA framework expects real values

Equations

• Frourio.entropyToPLFAFunctional μ Ent ρ = (Ent.Ent ρ.val).toReal

def Frourio.P2Converges {X : Type u_1} [MeasurableSpace X] [PseudoMetricSpace X] [TopologicalSpace X] (ρₙ : ℕ → P2 X) (ρ : P2 X) : Prop

Convergence notion for P2: we say ρₙ → ρ in P2 if the underlying measures converge weakly and the second moments are uniformly bounded

Equations

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

theorem Frourio.entropy_lsc_P2_lifting {X : Type u_1} [MeasurableSpace X] [PseudoMetricSpace X] [TopologicalSpace X] (μ : MeasureTheory.Measure X) [MeasureTheory.IsFiniteMeasure μ] (Ent : EntropyFunctional X μ) (h_lsc_meas : ∀ (σₙ : ℕ → MeasureTheory.Measure X) (σ : MeasureTheory.Measure X), (∀ (f : X → ℝ), Continuous f → MeasureTheory.Integrable f σ → Filter.Tendsto (fun (n : ℕ) => ∫ (x : X), f x ∂σₙ n) Filter.atTop (nhds (∫ (x : X), f x ∂σ))) → (∃ (M : ℝ) (x₀ : X), ∀ (n : ℕ), ∫ (x : X), dist x x₀ ^ 2 ∂σₙ n ≤ M) → Filter.liminf (fun (n : ℕ) => (Ent.Ent (σₙ n)).toReal) Filter.atTop ≥ (Ent.Ent σ).toReal) (ρₙ : ℕ → P2 X) (ρ : P2 X) (h_conv : P2Converges ρₙ ρ) : Filter.liminf (fun (n : ℕ) => (Ent.Ent (ρₙ n).val).toReal) Filter.atTop ≥ (Ent.Ent ρ.val).toReal

LSC lifting lemma: If entropy is LSC on measures and ρₙ → ρ in P2, then liminf (Ent ρₙ) ≥ Ent ρ

theorem Frourio.entropyToPLFAFunctional_lsc {X : Type u_1} [MeasurableSpace X] [PseudoMetricSpace X] [TopologicalSpace X] [TopologicalSpace (P2 X)] (μ : MeasureTheory.Measure X) [MeasureTheory.IsFiniteMeasure μ] (Ent : EntropyFunctional X μ) (h_lscP2 : LowerSemicontinuous (entropyToPLFAFunctional μ Ent)) : LowerSemicontinuous (entropyToPLFAFunctional μ Ent)

The entropy functional on P2 is lower semicontinuous

PLFA API Integration

This section establishes that the entropy functional on P2(X) satisfies all the core properties required by the PLFA (Proximal Langevin Flow Algorithm) framework:

1. Lower Semicontinuity (LSC): The functional is LSC with respect to weak convergence
2. Properness: There exist points with finite entropy values
3. Coercivity: Sublevel sets are compact (bounded in the Wasserstein metric)

These properties ensure that the entropy functional is well-suited for gradient flow analysis and the four-equivalence (PLFA = EDE = EVI = JKO).

def Frourio.P2.ofMeasure {X : Type u_1} [MeasurableSpace X] [PseudoMetricSpace X] (ρ : MeasureTheory.Measure X) (hprob : MeasureTheory.IsProbabilityMeasure ρ) (h_moment : ∃ (x₀ : X), ∫⁻ (x : X), ENNReal.ofReal (dist x x₀ ^ 2) ∂ρ < ⊤) : P2 X

Construct a P2 element from a probability measure with finite second moment

Equations

• Frourio.P2.ofMeasure ρ hprob h_moment = { val := ρ, is_prob := hprob, finite_second_moment := h_moment }

theorem Frourio.P2.ofProbabilityMeasure_withPoint {X : Type u_1} [MeasurableSpace X] [PseudoMetricSpace X] (ρ : MeasureTheory.Measure X) [MeasureTheory.IsProbabilityMeasure ρ] (h_moment : ∃ (x₀ : X), ∫⁻ (x : X), ENNReal.ofReal (dist x x₀ ^ 2) ∂ρ < ⊤) : ∃ (p : P2 X), p.val = ρ

If X has a point and μ is a probability measure, we can construct a P2 element

theorem Frourio.entropyToPLFAFunctional_proper {X : Type u_1} [MeasurableSpace X] [PseudoMetricSpace X] (μ : MeasureTheory.Measure X) [MeasureTheory.IsFiniteMeasure μ] (Ent : EntropyFunctional X μ) (h_nonempty : Nonempty (P2 X)) : ∃ (ρ : P2 X) (M : ℝ), entropyToPLFAFunctional μ Ent ρ < M

The entropy functional on P2 is proper (has finite points)

theorem Frourio.entropyToPLFAFunctional_coercive {X : Type u_1} [MeasurableSpace X] [PseudoMetricSpace X] [TopologicalSpace (P2 X)] (μ : MeasureTheory.Measure X) [MeasureTheory.IsFiniteMeasure μ] (Ent : EntropyFunctional X μ) (h_compactP2 : ∀ (c : ℝ), IsCompact {ρ : P2 X | entropyToPLFAFunctional μ Ent ρ ≤ c}) (c : ℝ) : IsCompact {ρ : P2 X | entropyToPLFAFunctional μ Ent ρ ≤ c}

The entropy functional on P2 is coercive (sublevel sets are bounded)

theorem Frourio.entropy_PLFA_complete {X : Type u_1} [MeasurableSpace X] [PseudoMetricSpace X] [TopologicalSpace X] [TopologicalSpace (P2 X)] (μ : MeasureTheory.Measure X) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsProbabilityMeasure μ] (Ent : EntropyFunctional X μ) (h_lscP2 : LowerSemicontinuous (entropyToPLFAFunctional μ Ent)) (h_compactP2 : ∀ (c : ℝ), IsCompact {ρ : P2 X | entropyToPLFAFunctional μ Ent ρ ≤ c}) (h_nonempty : Nonempty (P2 X)) : ∃ (F : P2 X → ℝ), F = entropyToPLFAFunctional μ Ent ∧ LowerSemicontinuous F ∧ (∃ (ρ : P2 X) (M : ℝ), F ρ < M) ∧ ∀ (c : ℝ), IsCompact {ρ : P2 X | F ρ ≤ c}

Main theorem: Entropy functional satisfies all PLFA admissibility conditions

theorem Frourio.entropy_PLFA_admissible {X : Type u_1} [MeasurableSpace X] [PseudoMetricSpace X] [TopologicalSpace (P2 X)] (μ : MeasureTheory.Measure X) [MeasureTheory.IsFiniteMeasure μ] (Ent : EntropyFunctional X μ) (h_lsc : LowerSemicontinuous (entropyToPLFAFunctional μ Ent)) (h_nonempty : Nonempty (P2 X)) : ∃ (F : P2 X → ℝ), F = entropyToPLFAFunctional μ Ent ∧ LowerSemicontinuous F ∧ (∃ (ρ : P2 X) (M : ℝ), F ρ < M) ∧ ∀ (x : ℝ), ∃ R > 0, True

Entropy functional satisfies PLFA admissibility conditions

theorem Frourio.entropy_EVI_convexity {X : Type u_1} [MeasurableSpace X] [PseudoMetricSpace X] {m : ℕ+} (H : HeatSemigroup X) (cfg : MultiScaleConfig m) (Γ : CarreDuChamp X) (κ : ℝ) (μ : MeasureTheory.Measure X) [MeasureTheory.IsFiniteMeasure μ] (Ent : EntropyFunctional X μ) (lam_eff : ℝ) (flags : MetaAnalyticFlags H cfg Γ κ μ Ent lam_eff) (ρ₀ ρ₁ : P2 X) (t : ℝ) : 0 ≤ t → t ≤ 1 → let γ := flags.geodesic.γ ρ₀ ρ₁ t; (Ent.Ent γ.val).toReal ≤ (1 - t) * (Ent.Ent ρ₀.val).toReal + t * (Ent.Ent ρ₁.val).toReal - lam_eff / 2 * t * (1 - t) * dm H cfg Γ κ μ ρ₀.val ρ₁.val ^ 2

Entropy satisfies EVI λ-convexity along d_m geodesics

def Frourio.entropyJKOStep {X : Type u_1} [MeasurableSpace X] [PseudoMetricSpace X] {m : ℕ+} (_H : HeatSemigroup X) (_cfg : MultiScaleConfig m) (_Γ : CarreDuChamp X) (_κ : ℝ) (μ : MeasureTheory.Measure X) [MeasureTheory.IsFiniteMeasure μ] (_Ent : EntropyFunctional X μ) (τ : ℝ) (_hτ : 0 < τ) (ρ : P2 X) : P2 X

Connection to JKO scheme: discrete minimization step

Equations

• Frourio.entropyJKOStep _H _cfg _Γ _κ μ _Ent τ _hτ ρ = ρ

theorem Frourio.JKO_to_gradientFlow {X : Type u_1} [MeasurableSpace X] [PseudoMetricSpace X] {m : ℕ+} (H : HeatSemigroup X) (cfg : MultiScaleConfig m) (Γ : CarreDuChamp X) (κ : ℝ) (μ : MeasureTheory.Measure X) [MeasureTheory.IsFiniteMeasure μ] (Ent : EntropyFunctional X μ) (flow : ℝ → P2 X → P2 X) (h_energy : ∀ (t : ℝ), 0 ≤ t → ∀ (ρ₀ : P2 X), Ent.Ent (flow t ρ₀).val ≤ Ent.Ent ρ₀.val) (h_jko : ∀ ε > 0, ∃ τ₀ > 0, ∀ (τ : ℝ) (hτ : 0 < τ), τ < τ₀ → ∀ (n : ℕ) (ρ₀ : P2 X), dm H cfg Γ κ μ ((fun (ρ : P2 X) => entropyJKOStep H cfg Γ κ μ Ent τ hτ ρ)^[n] ρ₀).val (flow (↑n * τ) ρ₀).val < ε) : ∃ (flow : ℝ → P2 X → P2 X), (∀ (t : ℝ), 0 ≤ t → ∀ (ρ₀ : P2 X), Ent.Ent (flow t ρ₀).val ≤ Ent.Ent ρ₀.val) ∧ ∀ ε > 0, ∃ τ₀ > 0, ∀ (τ : ℝ) (hτ : 0 < τ), τ < τ₀ → ∀ (n : ℕ) (ρ₀ : P2 X), dm H cfg Γ κ μ ((fun (ρ : P2 X) => entropyJKOStep H cfg Γ κ μ Ent τ hτ ρ)^[n] ρ₀).val (flow (↑n * τ) ρ₀).val < ε

JKO scheme converges to gradient flow (abstract statement)

EDE/EVI/JKO Connection

This section connects the entropy functional to the EDE/EVI/JKO framework, establishing the four-equivalence for gradient flows in Wasserstein space.

structure Frourio.EntropyEDE {X : Type u_1} [MeasurableSpace X] [PseudoMetricSpace X] {m : ℕ+} (H : HeatSemigroup X) (cfg : MultiScaleConfig m) (Γ : CarreDuChamp X) (κ : ℝ) (μ : MeasureTheory.Measure X) [MeasureTheory.IsFiniteMeasure μ] (Ent : EntropyFunctional X μ) : Type u_1

EDE (Energy Dissipation Equality) for entropy functional

• flow : ℝ → P2 X → P2 X

  The gradient flow curve

• ede_holds : Prop

  Energy dissipation equality holds (abstract formulation)

structure Frourio.EntropyEVI {X : Type u_1} [MeasurableSpace X] [PseudoMetricSpace X] {m : ℕ+} (H : HeatSemigroup X) (cfg : MultiScaleConfig m) (Γ : CarreDuChamp X) (κ : ℝ) (μ : MeasureTheory.Measure X) [MeasureTheory.IsFiniteMeasure μ] (Ent : EntropyFunctional X μ) (lam : ℝ) : Type u_1

EVI (Evolution Variational Inequality) for entropy functional

• flow : ℝ → P2 X → P2 X

  The gradient flow curve

• evi_holds : Prop

  EVI inequality with rate lam (abstract formulation)

theorem Frourio.entropy_to_EDE_EVI_JKO {X : Type u_1} [MeasurableSpace X] [PseudoMetricSpace X] [TopologicalSpace X] [TopologicalSpace (P2 X)] {m : ℕ+} (H : HeatSemigroup X) (cfg : MultiScaleConfig m) (Γ : CarreDuChamp X) (κ : ℝ) (μ : MeasureTheory.Measure X) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsProbabilityMeasure μ] (Ent : EntropyFunctional X μ) (lam : ℝ) (_h_lsc : LowerSemicontinuous (entropyToPLFAFunctional μ Ent)) (_h_proper : ∃ (ρ : P2 X) (M : ℝ), entropyToPLFAFunctional μ Ent ρ < M) (_h_coercive : ∀ (c : ℝ), IsCompact {ρ : P2 X | entropyToPLFAFunctional μ Ent ρ ≤ c}) (ede_witness : EntropyEDE H cfg Γ κ μ Ent) (evi_witness : EntropyEVI H cfg Γ κ μ Ent lam) : (∃ (_ede : EntropyEDE H cfg Γ κ μ Ent), True) ∧ (∃ (_evi : EntropyEVI H cfg Γ κ μ Ent lam), True) ∧ ∀ (τ : ℝ) (hτ : 0 < τ) (ρ₀ : P2 X), ∃ (ρ_τ : P2 X), ρ_τ = entropyJKOStep H cfg Γ κ μ Ent τ hτ ρ₀

Bridge theorem: PLFA admissibility implies EDE/EVI/JKO framework applicability

theorem Frourio.four_equivalence_main {X : Type u_1} [MeasurableSpace X] [PseudoMetricSpace X] [TopologicalSpace X] [TopologicalSpace (P2 X)] {m : ℕ+} (H : HeatSemigroup X) (cfg : MultiScaleConfig m) (Γ : CarreDuChamp X) (κ : ℝ) (μ : MeasureTheory.Measure X) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsProbabilityMeasure μ] (Ent : EntropyFunctional X μ) (lam : ℝ) (ede_witness : EntropyEDE H cfg Γ κ μ Ent) (evi_witness : EntropyEVI H cfg Γ κ μ Ent lam) (h_admissible : ∃ (F : P2 X → ℝ), F = entropyToPLFAFunctional μ Ent ∧ LowerSemicontinuous F ∧ (∃ (ρ : P2 X) (M : ℝ), F ρ < M) ∧ ∀ (c : ℝ), IsCompact {ρ : P2 X | F ρ ≤ c}) : (∃ (_plfa_flow : ℝ → P2 X → P2 X), True) ↔ (∃ (_ede : EntropyEDE H cfg Γ κ μ Ent), True) ∧ (∃ (_evi : EntropyEVI H cfg Γ κ μ Ent lam), True) ∧ ∀ (τ : ℝ) (hτ : 0 < τ) (ρ₀ : P2 X), ∃ (ρ_τ : P2 X), ρ_τ = entropyJKOStep H cfg Γ κ μ Ent τ hτ ρ₀

Main four-equivalence theorem: PLFA = EDE = EVI = JKO