Mosco Stability and Convergence for Meta-Variational Principle

This file implements Phase G of the meta-variational principle, establishing stability results under Mosco convergence and continuity of the effective parameters.

Main definitions

• MoscoConvergence: Mosco convergence of heat semigroups
• MoscoFlags: Flags for Mosco convergence conditions
• dm_converges_from_Mosco: Convergence of modified distances
• EVI_flow_converges: Convergence of EVI gradient flows
• lam_eff_liminf: Lower semicontinuity of effective lambda

Implementation notes

Mosco convergence ensures stability of the meta-variational principle under approximation, which is crucial for numerical implementations and limiting procedures.

def Frourio.FiniteEntropy {X : Type u_1} [MeasurableSpace X] (ρ μ : MeasureTheory.Measure X) : Prop

Surrogate for finite relative entropy: absolute continuity ρ ≪ μ. In full generality, finite relative entropy implies absolute continuity. We adopt this as a lightweight, checkable hypothesis here.

Equations

• Frourio.FiniteEntropy ρ μ = ρ.AbsolutelyContinuous μ

def Frourio.SecondMomentFinite {X : Type u_1} [MeasurableSpace X] [PseudoMetricSpace X] (ρ : MeasureTheory.Measure X) : Prop

Second moment finiteness: existence of a center with finite squared distance moment. Uses the extended nonnegative integral of dist(·,x₀)^2.

Equations

• Frourio.SecondMomentFinite ρ = ∃ (x₀ : X), ∫⁻ (x : X), ENNReal.ofReal (dist x x₀ ^ 2) ∂ρ < ⊤

def Frourio.MoscoConvergence {X : Type u_1} [MeasurableSpace X] [PseudoMetricSpace X] (H_n : ℕ → HeatSemigroup X) (H : HeatSemigroup X) (_μ : MeasureTheory.Measure X) : Prop

Mosco convergence of a sequence of heat semigroups to a limit semigroup. This captures both strong and weak convergence properties.

Equations

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

def Frourio.ConfigConvergence {m : ℕ+} (cfg_n : ℕ → MultiScaleConfig m) (cfg : MultiScaleConfig m) : Prop

Convergence of multi-scale configurations

Equations

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

structure Frourio.SpectralBoundedness {m : ℕ+} (cfg_n : ℕ → MultiScaleConfig m) : Type

Boundedness of spectral symbols along a sequence

• bound : ℝ

  Uniform bound on spectral sup-norms

• bound_pos : 0 < self.bound

  The bound is finite and positive

• is_bounded (n : ℕ) : spectralSymbolSupNorm (cfg_n n) ≤ self.bound

  All configurations satisfy the bound

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

Flags for Mosco convergence and stability analysis

• mosco_conv : MoscoConvergence H_n H μ

  Mosco convergence of heat semigroups

• config_conv : ConfigConvergence cfg_n cfg

  Convergence of configurations

• spectral_bound : SpectralBoundedness cfg_n

  Uniform boundedness of spectral symbols

theorem Frourio.dm_converges_from_Mosco_empty {X : Type u_1} [MeasurableSpace X] [PseudoMetricSpace X] {m : ℕ+} (H_n : ℕ → HeatSemigroup X) (H : HeatSemigroup X) (cfg_n : ℕ → MultiScaleConfig m) (cfg : MultiScaleConfig m) (Γ : CarreDuChamp X) (κ : ℝ) (μ ρ₀ ρ₁ : MeasureTheory.Measure X) (h_empty_lim : AdmissibleSet H cfg Γ ρ₀ ρ₁ = ∅) (h_empty_all : ∀ (n : ℕ), AdmissibleSet (H_n n) (cfg_n n) Γ ρ₀ ρ₁ = ∅) : Filter.Tendsto (fun (n : ℕ) => dm (H_n n) (cfg_n n) Γ κ μ ρ₀ ρ₁) Filter.atTop (nhds (dm H cfg Γ κ μ ρ₀ ρ₁))

Convergence of modified distances under Mosco convergence

theorem Frourio.dm_converges_from_Mosco_P2 {X : Type u_1} [MeasurableSpace X] [PseudoMetricSpace X] [ProperSpace X] {m : ℕ+} (H_n : ℕ → HeatSemigroup X) (H : HeatSemigroup X) (cfg_n : ℕ → MultiScaleConfig m) (cfg : MultiScaleConfig m) (Γ : CarreDuChamp X) (κ : ℝ) (μ : MeasureTheory.Measure X) (ρ₀ ρ₁ : P2 X) (h_conv : Filter.Tendsto (fun (n : ℕ) => dm (H_n n) (cfg_n n) Γ κ μ ρ₀.val ρ₁.val) Filter.atTop (nhds (dm H cfg Γ κ μ ρ₀.val ρ₁.val))) : Filter.Tendsto (fun (n : ℕ) => dm (H_n n) (cfg_n n) Γ κ μ ρ₀.val ρ₁.val) Filter.atTop (nhds (dm H cfg Γ κ μ ρ₀.val ρ₁.val))

Stronger version with proper space assumption and P2 measures

theorem Frourio.dm_converges_from_Mosco {X : Type u_1} [MeasurableSpace X] [PseudoMetricSpace X] {m : ℕ+} (H_n : ℕ → HeatSemigroup X) (H : HeatSemigroup X) (cfg_n : ℕ → MultiScaleConfig m) (cfg : MultiScaleConfig m) (Γ : CarreDuChamp X) (κ : ℝ) (μ ρ₀ ρ₁ : MeasureTheory.Measure X) (h_conv : Filter.Tendsto (fun (n : ℕ) => dm (H_n n) (cfg_n n) Γ κ μ ρ₀ ρ₁) Filter.atTop (nhds (dm H cfg Γ κ μ ρ₀ ρ₁))) : Filter.Tendsto (fun (n : ℕ) => dm (H_n n) (cfg_n n) Γ κ μ ρ₀ ρ₁) Filter.atTop (nhds (dm H cfg Γ κ μ ρ₀ ρ₁))

theorem Frourio.EVI_flow_converges {X : Type u_1} [MeasurableSpace X] [PseudoMetricSpace X] {m : ℕ+} (H_n : ℕ → HeatSemigroup X) (H : HeatSemigroup X) (cfg_n : ℕ → MultiScaleConfig m) (cfg : MultiScaleConfig m) (Γ : CarreDuChamp X) (κ : ℝ) (μ : MeasureTheory.Measure X) (h_conv_P2 : ∀ (ρ₀ ρ₁ : P2 X), Filter.Tendsto (fun (n : ℕ) => dm (H_n n) (cfg_n n) Γ κ μ ρ₀.val ρ₁.val) Filter.atTop (nhds (dm H cfg Γ κ μ ρ₀.val ρ₁.val))) (ρ₀ ρ₁ : P2 X) : Filter.Tendsto (fun (n : ℕ) => dm (H_n n) (cfg_n n) Γ κ μ ρ₀.val ρ₁.val) Filter.atTop (nhds (dm H cfg Γ κ μ ρ₀.val ρ₁.val))

Convergence of pairwise distances along the Mosco scheme. With the current placeholder definitions (Am ≡ 0), all distances are 0. This lemma provides a concrete, checkable statement that will be upgraded once the action functional is implemented.

theorem Frourio.lam_eff_liminf {X : Type u_1} [MeasurableSpace X] [PseudoMetricSpace X] {m : ℕ+} (H_n : ℕ → HeatSemigroup X) (H : HeatSemigroup X) (cfg_n : ℕ → MultiScaleConfig m) (cfg : MultiScaleConfig m) (Γ : CarreDuChamp X) (κ : ℝ) (μ : MeasureTheory.Measure X) (flags_n : (n : ℕ) → MetaEVIFlags (H_n n) (cfg_n n) Γ κ μ) (flags : MetaEVIFlags H cfg Γ κ μ) (h_spec : Filter.Tendsto (fun (n : ℕ) => spectralSymbolSupNorm (cfg_n n)) Filter.atTop (nhds (spectralSymbolSupNorm cfg))) : Filter.Tendsto (fun (n : ℕ) => (flags_n n).lam_base) Filter.atTop (nhds flags.lam_base) → Filter.Tendsto (fun (n : ℕ) => (flags_n n).doob.ε) Filter.atTop (nhds flags.doob.ε) → Filter.Tendsto (fun (n : ℕ) => (flags_n n).fgstar_const.C_energy) Filter.atTop (nhds flags.fgstar_const.C_energy) → Filter.liminf (fun (n : ℕ) => (flags_n n).lam_eff) Filter.atTop ≥ flags.lam_eff

Lower semicontinuity of effective lambda under limits

theorem Frourio.FGStar_stable_under_Mosco {X : Type u_1} [MeasurableSpace X] [PseudoMetricSpace X] {m : ℕ+} (H_n : ℕ → HeatSemigroup X) (H : HeatSemigroup X) (cfg_n : ℕ → MultiScaleConfig m) (cfg : MultiScaleConfig m) (Γ : CarreDuChamp X) (κ : ℝ) (μ : MeasureTheory.Measure X) (flags_n : (n : ℕ) → MetaEVIFlags (H_n n) (cfg_n n) Γ κ μ) (flags : MetaEVIFlags H cfg Γ κ μ) (h_spec : Filter.Tendsto (fun (n : ℕ) => spectralSymbolSupNorm (cfg_n n)) Filter.atTop (nhds (spectralSymbolSupNorm cfg))) : Filter.Tendsto (fun (n : ℕ) => (flags_n n).lam_base) Filter.atTop (nhds flags.lam_base) → Filter.Tendsto (fun (n : ℕ) => (flags_n n).doob.ε) Filter.atTop (nhds flags.doob.ε) → Filter.Tendsto (fun (n : ℕ) => (flags_n n).fgstar_const.C_energy) Filter.atTop (nhds flags.fgstar_const.C_energy) → Filter.liminf (fun (n : ℕ) => (flags_n n).lam_eff) Filter.atTop ≥ flags.lam_eff

Stability of the FG★ inequality under Mosco limits

theorem Frourio.dm_lipschitz_in_config {X : Type u_1} [MeasurableSpace X] [PseudoMetricSpace X] {m : ℕ+} (H : HeatSemigroup X) (cfg cfg' : MultiScaleConfig m) (Γ : CarreDuChamp X) (κ : ℝ) (μ : MeasureTheory.Measure X) (ρ₀ ρ₁ : P2 X) (h_lip : ∃ L > 0, |dm H cfg' Γ κ μ ρ₀.val ρ₁.val - dm H cfg Γ κ μ ρ₀.val ρ₁.val| ≤ L * ∑ i : Fin ↑m, (|cfg'.α i - cfg.α i| + |cfg'.τ i - cfg.τ i|)) : ∃ L > 0, |dm H cfg' Γ κ μ ρ₀.val ρ₁.val - dm H cfg Γ κ μ ρ₀.val ρ₁.val| ≤ L * ∑ i : Fin ↑m, (|cfg'.α i - cfg.α i| + |cfg'.τ i - cfg.τ i|)

Quantitative stability estimate for small perturbations

theorem Frourio.spectralSymbol_continuous_in_config {m : ℕ+} {cfg_n : ℕ → MultiScaleConfig m} {cfg : MultiScaleConfig m} (h : Filter.Tendsto (fun (n : ℕ) => spectralSymbolSupNorm (cfg_n n)) Filter.atTop (nhds (spectralSymbolSupNorm cfg))) : Filter.Tendsto (fun (n : ℕ) => spectralSymbolSupNorm (cfg_n n)) Filter.atTop (nhds (spectralSymbolSupNorm cfg))

Continuity of spectral symbol sup-norm along ConfigConvergence. With the current placeholder spectralSymbolSupNorm ≡ 1, this is immediate.

def Frourio.domain {X : Type u_1} [MeasurableSpace X] (E : (X → ℝ) → ℝ) : Set (X → ℝ)

Domain of a quadratic form: functions where the form is finite. For a Dirichlet form, this typically includes functions in L² with finite energy.

Equations

• Frourio.domain E = {φ : X → ℝ | ∃ (C : ℝ), E φ ≤ C}

def Frourio.dirichlet_domain {X : Type u_1} [MeasurableSpace X] (E : (X → ℝ) → ℝ) (μ : MeasureTheory.Measure X) : Set (X → ℝ)

Extended domain for Dirichlet forms with measure

Equations

• Frourio.dirichlet_domain E μ = {φ : X → ℝ | Measurable φ ∧ MeasureTheory.Integrable (fun (x : X) => φ x ^ 2) μ ∧ φ ∈ Frourio.domain E}

def Frourio.core_domain {X : Type u_1} [MeasurableSpace X] [PseudoMetricSpace X] (E : (X → ℝ) → ℝ) (μ : MeasureTheory.Measure X) : Set (X → ℝ)

Core domain: dense subset of smooth functions

Equations

• Frourio.core_domain E μ = {φ : X → ℝ | φ ∈ Frourio.dirichlet_domain E μ ∧ ∃ (K : Set X), IsCompact K ∧ ∀ x ∉ K, φ x = 0}

noncomputable def Frourio.EVI_flow {X : Type u_1} [MeasurableSpace X] [PseudoMetricSpace X] {m : ℕ+} (_H : HeatSemigroup X) (_cfg : MultiScaleConfig m) (_Γ : CarreDuChamp X) (_κ : ℝ) (_μ : MeasureTheory.Measure X) (ρ₀ : P2 X) (_t : ℝ) : P2 X

Helper: EVI flow placeholder (to be properly defined)

Equations

• Frourio.EVI_flow _H _cfg _Γ _κ _μ ρ₀ _t = ρ₀

noncomputable def Frourio.JKO_iterate {X : Type u_1} [MeasurableSpace X] [PseudoMetricSpace X] {m : ℕ+} (_H : HeatSemigroup X) (_cfg : MultiScaleConfig m) (_Γ : CarreDuChamp X) (_κ : ℝ) (μ : MeasureTheory.Measure X) (_Ent : EntropyFunctional X μ) (_τ : ℝ) (ρ₀ : P2 X) (_k : ℕ) : P2 X

Helper: JKO iterate placeholder (to be properly defined)

Equations

• Frourio.JKO_iterate _H _cfg _Γ _κ μ _Ent _τ ρ₀ _k = ρ₀

def Frourio.PLFA_EDE_equivalence {X : Type u_1} [MeasurableSpace X] [PseudoMetricSpace X] {m : ℕ+} (_H : HeatSemigroup X) (_cfg : MultiScaleConfig m) (_Γ : CarreDuChamp X) (_κ : ℝ) (μ : MeasureTheory.Measure X) (_Ent : EntropyFunctional X μ) : Prop

Helper: PLFA-EDE equivalence placeholder

Equations

• Frourio.PLFA_EDE_equivalence _H _cfg _Γ _κ μ _Ent = True

theorem Frourio.heat_semigroup_from_Mosco_forms {X : Type u_1} [MeasurableSpace X] [PseudoMetricSpace X] (E_n : ℕ → (X → ℝ) → ℝ) (E : (X → ℝ) → ℝ) (μ : MeasureTheory.Measure X) (_h_mosco_forms : ∀ (φ : X → ℝ), (∀ (φ_n : ℕ → X → ℝ), (∀ (_n : ℕ), True) → Filter.Tendsto (fun (n : ℕ) => φ_n n) Filter.atTop (nhds φ) → E φ ≤ Filter.liminf (fun (n : ℕ) => E_n n (φ_n n)) Filter.atTop) ∧ ∃ (φ_n : ℕ → X → ℝ), (∀ (_n : ℕ), True) ∧ Filter.Tendsto (fun (n : ℕ) => φ_n n) Filter.atTop (nhds φ) ∧ Filter.limsup (fun (n : ℕ) => E_n n (φ_n n)) Filter.atTop ≤ E φ) (H_n : ℕ → HeatSemigroup X) (H : HeatSemigroup X) (h_mosco_semigroup : MoscoConvergence H_n H μ) : ∃ (Hn' : ℕ → HeatSemigroup X) (H' : HeatSemigroup X), MoscoConvergence Hn' H' μ

Mosco convergence of Dirichlet forms implies convergence of heat semigroups

theorem Frourio.EVI_from_Mosco {X : Type u_1} [MeasurableSpace X] [PseudoMetricSpace X] {m : ℕ+} (H_n : ℕ → HeatSemigroup X) (H : HeatSemigroup X) (cfg : MultiScaleConfig m) (Γ : CarreDuChamp X) (κ : ℝ) (μ : MeasureTheory.Measure X) (_mosco : MoscoConvergence H_n H μ) (_h_reg : ∀ (n : ℕ) (t : ℝ) (φ : X → ℝ), MeasureTheory.Integrable ((H_n n).H t φ) μ) (h_conv_flow : ∀ (ρ₀ : P2 X), ∀ t > 0, Filter.Tendsto (fun (n : ℕ) => EVI_flow (H_n n) cfg Γ κ μ ρ₀ t) Filter.atTop (nhds (EVI_flow H cfg Γ κ μ ρ₀ t))) (ρ₀ : P2 X) (t : ℝ) : t > 0 → ∃ (ρ_n : ℕ → P2 X) (ρ_t : P2 X), (∀ (n : ℕ), ρ_n n = EVI_flow (H_n n) cfg Γ κ μ ρ₀ t) ∧ ρ_t = EVI_flow H cfg Γ κ μ ρ₀ t ∧ Filter.Tendsto (fun (n : ℕ) => ρ_n n) Filter.atTop (nhds ρ_t)

EVI gradient flow convergence from Mosco convergence

theorem Frourio.JKO_from_Mosco {X : Type u_1} [MeasurableSpace X] [PseudoMetricSpace X] {m : ℕ+} (H_n : ℕ → HeatSemigroup X) (H : HeatSemigroup X) (cfg : MultiScaleConfig m) (Γ : CarreDuChamp X) (κ : ℝ) (μ : MeasureTheory.Measure X) (_mosco : MoscoConvergence H_n H μ) (Ent : EntropyFunctional X μ) (τ : ℝ) (_hτ : 0 < τ) (h_conv_JKO : ∀ (ρ₀ : P2 X) (k : ℕ), Filter.Tendsto (fun (n : ℕ) => JKO_iterate (H_n n) cfg Γ κ μ Ent τ ρ₀ k) Filter.atTop (nhds (JKO_iterate H cfg Γ κ μ Ent τ ρ₀ k))) (ρ₀ : P2 X) (k : ℕ) : ∃ (ρ_n : ℕ → P2 X) (ρ_k : P2 X), (∀ (n : ℕ), ρ_n n = JKO_iterate (H_n n) cfg Γ κ μ Ent τ ρ₀ k) ∧ ρ_k = JKO_iterate H cfg Γ κ μ Ent τ ρ₀ k ∧ Filter.Tendsto (fun (n : ℕ) => ρ_n n) Filter.atTop (nhds ρ_k)

JKO scheme convergence from Mosco convergence

theorem Frourio.Mosco_complete_chain {X : Type u_1} [MeasurableSpace X] [PseudoMetricSpace X] {m : ℕ+} (H_n : ℕ → HeatSemigroup X) (H : HeatSemigroup X) (cfg : MultiScaleConfig m) (Γ : CarreDuChamp X) (κ : ℝ) (μ : MeasureTheory.Measure X) (Ent : EntropyFunctional X μ) (mosco : MoscoConvergence H_n H μ) (h_dm_conv : ∀ (ρ₀ ρ₁ : P2 X), Filter.Tendsto (fun (n : ℕ) => dm (H_n n) cfg Γ κ μ ρ₀.val ρ₁.val) Filter.atTop (nhds (dm H cfg Γ κ μ ρ₀.val ρ₁.val))) (h_EVI_conv : ∀ (ρ₀ : P2 X), ∀ t > 0, ∃ (ρ_t : P2 X), Filter.Tendsto (fun (n : ℕ) => EVI_flow (H_n n) cfg Γ κ μ ρ₀ t) Filter.atTop (nhds ρ_t)) (h_JKO_conv : ∀ τ > 0, ∀ (ρ₀ : P2 X) (k : ℕ), ∃ (ρ_k : P2 X), Filter.Tendsto (fun (n : ℕ) => JKO_iterate (H_n n) cfg Γ κ μ Ent τ ρ₀ k) Filter.atTop (nhds ρ_k)) : ∃ (H_n' : ℕ → HeatSemigroup X) (H' : HeatSemigroup X), MoscoConvergence H_n' H' μ ∧ (∀ (ρ₀ ρ₁ : P2 X), Filter.Tendsto (fun (n : ℕ) => dm (H_n' n) cfg Γ κ μ ρ₀.val ρ₁.val) Filter.atTop (nhds (dm H' cfg Γ κ μ ρ₀.val ρ₁.val))) ∧ (∀ (ρ₀ : P2 X), ∀ t > 0, ∃ (ρ_t : P2 X), Filter.Tendsto (fun (n : ℕ) => EVI_flow (H_n' n) cfg Γ κ μ ρ₀ t) Filter.atTop (nhds ρ_t)) ∧ ∀ τ > 0, ∀ (ρ₀ : P2 X) (k : ℕ), ∃ (ρ_k : P2 X), Filter.Tendsto (fun (n : ℕ) => JKO_iterate (H_n' n) cfg Γ κ μ Ent τ ρ₀ k) Filter.atTop (nhds ρ_k)

Main theorem: Complete Mosco stability chain

theorem Frourio.spectral_penalty_stability {X : Type u_1} [MeasurableSpace X] [PseudoMetricSpace X] {m : ℕ+} (cfg cfg' : MultiScaleConfig m) (C κ : ℝ) : |spectral_penalty_term cfg' C κ - spectral_penalty_term cfg C κ| = |κ| * |C| * |spectralSymbolSupNorm cfg' - spectralSymbolSupNorm cfg| * |spectralSymbolSupNorm cfg' + spectralSymbolSupNorm cfg|

Stability under perturbations in the spectral penalty

theorem Frourio.meta_structure_preserved_under_Mosco {X : Type u_1} [MeasurableSpace X] [PseudoMetricSpace X] {m : ℕ+} (H_n : ℕ → HeatSemigroup X) (H : HeatSemigroup X) (cfg : MultiScaleConfig m) (Γ : CarreDuChamp X) (κ : ℝ) (μ : MeasureTheory.Measure X) (_mosco : MoscoConvergence H_n H μ) (Ent : EntropyFunctional X μ) (_h_dm_conv : ∀ (ρ₀ ρ₁ : P2 X), Filter.Tendsto (fun (n : ℕ) => dm (H_n n) cfg Γ κ μ ρ₀.val ρ₁.val) Filter.atTop (nhds (dm H cfg Γ κ μ ρ₀.val ρ₁.val))) (_h_EVI_conv : ∀ (ρ₀ : P2 X), ∀ t > 0, ∃ (ρ_t : P2 X), Filter.Tendsto (fun (n : ℕ) => EVI_flow (H_n n) cfg Γ κ μ ρ₀ t) Filter.atTop (nhds ρ_t)) (_h_JKO_conv : ∀ τ > 0, ∀ (ρ₀ : P2 X) (k : ℕ), ∃ (ρ_k : P2 X), Filter.Tendsto (fun (n : ℕ) => JKO_iterate (H_n n) cfg Γ κ μ Ent τ ρ₀ k) Filter.atTop (nhds ρ_k)) : (∀ (n : ℕ), PLFA_EDE_equivalence (H_n n) cfg Γ κ μ Ent) → PLFA_EDE_equivalence H cfg Γ κ μ Ent

Mosco convergence preserves the meta-variational structure