@[reducible, inline]

abbrev Frourio.Rge0 : Type

Equations

• Frourio.Rge0 = { t : ℝ // 0 ≤ t }

def Frourio.toRge0 (t : ℝ) : Rge0

Equations

• Frourio.toRge0 t = ⟨max t 0, ⋯⟩

def Frourio.restrictNonneg {X : Type u_1} (u : Rge0 → X) : ℝ → X

Equations

• Frourio.restrictNonneg u t = u (Frourio.toRge0 t)

def Frourio.IsEVISolutionNonneg {X : Type u_1} [PseudoMetricSpace X] (P : EVIProblem X) (u : Rge0 → X) : Prop

EVI predicate on nonnegative time curves via the restrictNonneg wrapper.

Equations

• Frourio.IsEVISolutionNonneg P u = Frourio.IsEVISolution P (Frourio.restrictNonneg u)

def Frourio.evi_contraction_nonneg {X : Type u_1} [PseudoMetricSpace X] (P : EVIProblem X) (u v : Rge0 → X) (_hu : IsEVISolutionNonneg P u) (_hv : IsEVISolutionNonneg P v) : Prop

Contraction statement for nonnegative-time curves (wrapper version).

Equations

• Frourio.evi_contraction_nonneg P u v _hu _hv = Frourio.ContractionProperty P (Frourio.restrictNonneg u) (Frourio.restrictNonneg v)

structure Frourio.MoscoSystem (ι : Type u_1) : Type (max (max u_1 (u_2 + 1)) (u_3 + 1))

• Xh : ι → Type u_2
• X : Type u_3
• hx (h : ι) : PseudoMetricSpace (self.Xh h)
• x : PseudoMetricSpace self.X
• Th (h : ι) : self.Xh h → self.X
• Eh (h : ι) : self.Xh h → ℝ
• E : self.X → ℝ

def Frourio.MoscoGeodesicComplete {ι : Type u_1} (S : MoscoSystem ι) : Prop

Equations

• Frourio.MoscoGeodesicComplete S = Nonempty S.X

def Frourio.MoscoTight {ι : Type u_1} (S : MoscoSystem ι) : Prop

Equations

• Frourio.MoscoTight S = ∃ (C : ℝ), ∀ (h : ι) (x : S.Xh h), S.Eh h x ≥ -C

def Frourio.MoscoM1 {ι : Type u_1} (S : MoscoSystem ι) : Prop

Equations

• Frourio.MoscoM1 S = ∀ (h : ι) (x : S.Xh h), S.E (S.Th h x) ≤ S.Eh h x

def Frourio.MoscoM2 {ι : Type u_1} (S : MoscoSystem ι) : Prop

Equations

• Frourio.MoscoM2 S = ∀ (x : S.X), ∃ (h : ι) (xh : S.Xh h), S.Th h xh = x ∧ S.Eh h xh ≤ S.E x

def Frourio.LowerSemicontinuousSeq {X : Type u_1} [PseudoMetricSpace X] (E : X → ℝ) : Prop

Equations

• Frourio.LowerSemicontinuousSeq E = ∀ (x : X) (s : ℕ → X), Filter.Tendsto s Filter.atTop (nhds x) → E x ≤ Filter.liminf (fun (n : ℕ) => E (s n)) Filter.atTop

structure Frourio.MoscoAssumptions {ι : Type u_1} (S : MoscoSystem ι) : Prop

Assumption pack using the minimal Mosco predicates, with a concrete sequential lower semicontinuity requirement for the limit energy.

• geodesic_complete : MoscoGeodesicComplete S
• tightness : MoscoTight S
• lsc_Ent : LowerSemicontinuousSeq S.E
• M1 : MoscoM1 S
• M2 : MoscoM2 S

def Frourio.EVILimitHolds {ι : Type u_1} (S : MoscoSystem ι) : Prop

Limit EVI property under Mosco convergence. We record that the liminf/recovery/tightness and geodesic completeness conditions are available at the limit. This predicate is deliberately lightweight and will be strengthened to true EVI statements in later phases.

Equations

• Frourio.EVILimitHolds S = (Frourio.MoscoM1 S ∧ Frourio.MoscoM2 S ∧ Frourio.MoscoTight S ∧ Frourio.MoscoGeodesicComplete S)

theorem Frourio.eviInheritance {ι : Type u_1} (S : MoscoSystem ι) (H : MoscoAssumptions S) : EVILimitHolds S

EVI inheritance under Mosco assumptions (theoremized skeleton). Proof sketch: Under geodesic completeness, tightness, l.s.c., and M1/M2, JKO-type minimizing movement schemes are tight, and limit curves satisfy the EVI inequality for the Γ-limit functional. Here we provide a placeholder result that will be refined in later phases.

Sufficient conditions tailored to an “Entropy + Dirichlet form” setting.

We introduce lightweight predicates named after the intended analytic assumptions and show how they imply the minimal Mosco predicates used by this file (Tight/M1/M2). These remain Prop‑valued and proof‑light.

def Frourio.EntropyUniformLowerBound {ι : Type u_1} (S : MoscoSystem ι) : Prop

Uniform entropy lower bound (coercivity surrogate) across the prelimit family: ∃ C, ∀ h x, E_h(x) ≥ -C.

Equations

• Frourio.EntropyUniformLowerBound S = ∃ (C : ℝ), ∀ (h : ι) (x : S.Xh h), S.Eh h x ≥ -C

def Frourio.DirichletFormLiminf {ι : Type u_1} (S : MoscoSystem ι) : Prop

Dirichlet‑form liminf inequality along the identification maps.

Equations

• Frourio.DirichletFormLiminf S = ∀ (h : ι) (x : S.Xh h), S.E (S.Th h x) ≤ S.Eh h x

def Frourio.DirichletFormRecovery {ι : Type u_1} (S : MoscoSystem ι) : Prop

Dirichlet‑form recovery inequality (no energy inflation at a preimage).

Equations

• Frourio.DirichletFormRecovery S = ∀ (x : S.X), ∃ (h : ι) (xh : S.Xh h), S.Th h xh = x ∧ S.Eh h xh ≤ S.E x

theorem Frourio.MoscoTight_from_entropy {ι : Type u_1} (S : MoscoSystem ι) (H : EntropyUniformLowerBound S) : MoscoTight S

Entropy lower bound implies MoscoTight.

theorem Frourio.MoscoM1_from_dirichlet_liminf {ι : Type u_1} (S : MoscoSystem ι) (H : DirichletFormLiminf S) : MoscoM1 S

Dirichlet liminf implies MoscoM1.

theorem Frourio.MoscoM2_from_dirichlet_recovery {ι : Type u_1} (S : MoscoSystem ι) (H : DirichletFormRecovery S) : MoscoM2 S

Dirichlet recovery implies MoscoM2.

theorem Frourio.build_MoscoAssumptions_from_entropy_dirichlet {ι : Type u_1} (S : MoscoSystem ι) (Hg : MoscoGeodesicComplete S) (Hent : EntropyUniformLowerBound S) (Hlim : DirichletFormLiminf S) (Hrec : DirichletFormRecovery S) (Hlsc : LowerSemicontinuousSeq S.E) : MoscoAssumptions S

Build MoscoAssumptions from entropy lower bound and Dirichlet liminf/recovery statements, plus geodesic completeness (nonemptiness of the limit space).

theorem Frourio.EVILimit_from_entropy_dirichlet {ι : Type u_1} (S : MoscoSystem ι) (Hg : MoscoGeodesicComplete S) (Hent : EntropyUniformLowerBound S) (Hlim : DirichletFormLiminf S) (Hrec : DirichletFormRecovery S) (Hlsc : LowerSemicontinuousSeq S.E) : EVILimitHolds S

From the entropy/Dirichlet sufficient conditions, obtain the minimal EVILimitHolds predicate used in this file.

theorem Frourio.MoscoTight_of_uniform_lower_bound {ι : Type u_1} (S : MoscoSystem ι) (C : ℝ) (h : ∀ (h' : ι) (x : S.Xh h'), S.Eh h' x ≥ -C) : MoscoTight S

A uniform lower bound on all prelimit energies implies MoscoTight.

theorem Frourio.MoscoM1_of_liminf_along_Th {ι : Type u_1} (S : MoscoSystem ι) (h : ∀ (h' : ι) (x : S.Xh h'), S.E (S.Th h' x) ≤ S.Eh h' x) : MoscoM1 S

Pointwise liminf inequality along Th is exactly MoscoM1.

theorem Frourio.MoscoM2_of_recovery_no_inflation {ι : Type u_1} (S : MoscoSystem ι) (h : ∀ (x : S.X), ∃ (h' : ι) (xh : S.Xh h'), S.Th h' xh = x ∧ S.Eh h' xh ≤ S.E x) : MoscoM2 S

Existence of recovery points with no energy inflation is exactly MoscoM2.

structure Frourio.MoscoSufficientConditions {ι : Type u_1} (S : MoscoSystem ι) : Prop

Pack of sufficient conditions (uniform bound, liminf, recovery, nonempty limit).

• uniform_lower : ∃ (C : ℝ), ∀ (h : ι) (x : S.Xh h), S.Eh h x ≥ -C
• liminf_along_Th (h : ι) (x : S.Xh h) : S.E (S.Th h x) ≤ S.Eh h x
• recovery_no_inflation (x : S.X) : ∃ (h : ι) (xh : S.Xh h), S.Th h xh = x ∧ S.Eh h xh ≤ S.E x
• geodesic_complete : Nonempty S.X
• lsc_Ent : LowerSemicontinuousSeq S.E

theorem Frourio.build_MoscoAssumptions_from_sufficient {ι : Type u_1} (S : MoscoSystem ι) (H : MoscoSufficientConditions S) : MoscoAssumptions S

Build MoscoAssumptions from sufficient conditions.

theorem Frourio.EVILimit_from_sufficient {ι : Type u_1} (S : MoscoSystem ι) (H : MoscoSufficientConditions S) : EVILimitHolds S

From sufficient conditions, obtain the minimal EVILimitHolds predicate.