Functional layer (PLFA/EDE/EVI/JKO bridge skeleton)

This module introduces a lightweight functional container and constants to connect the FG8 framework with the existing analysis layer. The goal is to keep the API proof-light while exposing the key quantities and inequalities used later: the base entropy Ent, the Mellin-side term Dsigmam, a coupling parameter gamma, and the Doob corrected parameter lambdaBE = λ - 2 ε. We also provide a parameterized lower-bound predicate for the effective contraction rate.

structure Frourio.FrourioFunctional (X : Type u_1) [PseudoMetricSpace X] : Type u_1

Core functional container.

• Ent : X → ℝ
• Dsigmam : X → ℝ
• gamma : ℝ

noncomputable def Frourio.FrourioFunctional.F {X : Type u_1} [PseudoMetricSpace X] (A : FrourioFunctional X) : X → ℝ

Combined functional F(x) = Ent x + gamma * Dsigmam x.

Equations

• A.F x = A.Ent x + A.gamma * A.Dsigmam x

noncomputable def Frourio.FrourioFunctional.ofK {X : Type u_1} [PseudoMetricSpace X] (Ent : X → ℝ) (K : KTransform X) (gamma Ssup : ℝ) : FrourioFunctional X

Build a FrourioFunctional from an entropy Ent, a K-transform K, and a parameter gamma, using the DsigmamFromK interface with a supplied sup-norm proxy Ssup.

Equations

• Frourio.FrourioFunctional.ofK Ent K gamma Ssup = { Ent := Ent, Dsigmam := Frourio.DsigmamFromK K Ssup, gamma := gamma }

def Frourio.K1prime {X : Type u_1} [PseudoMetricSpace X] (A : FrourioFunctional X) : Prop

Narrow-continuity surrogate: we require a uniform lower bound for Dsigmam (coercivity proxy).

Equations

• Frourio.K1prime A = ∃ (C : ℝ), ∀ (x : X), A.Dsigmam x ≥ -C

def Frourio.K4m {X : Type u_1} [PseudoMetricSpace X] (A : FrourioFunctional X) : Prop

Geodesic-affinity surrogate: we assume nonnegativity of the coupling parameter gamma. This encodes that the extra term does not invert convexity trends.

Equations

• Frourio.K4m A = (0 ≤ A.gamma)

theorem Frourio.k1prime_ofK_from_uniform_lower_bound {X : Type u_1} [PseudoMetricSpace X] (Ent : X → ℝ) (K : KTransform X) (gamma Ssup C0 : ℝ) (hS : 0 ≤ Ssup) (hLB : UniformLowerBoundAtZero K C0) : K1prime (FrourioFunctional.ofK Ent K gamma Ssup)

If the K-transform has a uniform lower bound at s = 0 by -C0 and the scale Ssup is nonnegative, then the derived Dσm(x) = Ssup · K.map x 0 is bounded below by -(Ssup · C0). Hence the K1′ surrogate holds for the functional built from K.

theorem Frourio.F_lower_bound_of_ofK {X : Type u_1} [PseudoMetricSpace X] (Ent : X → ℝ) (K : KTransform X) (gamma Ssup C0 : ℝ) (hγ : 0 ≤ gamma) (hS : 0 ≤ Ssup) (hLB : UniformLowerBoundAtZero K C0) (x : X) : (FrourioFunctional.ofK Ent K gamma Ssup).F x ≥ Ent x - gamma * (Ssup * C0)

Numeric lower bound for F = Ent + γ · Dσm built from a KTransform with uniform kernel lower bound at s = 0. If γ ≥ 0 and Ssup ≥ 0, then

F(x) ≥ Ent(x) - γ · (Ssup · C0).

This inequality is used as a coercivity proxy downstream.

theorem Frourio.ofK_coercive_from_bounds {X : Type u_1} [PseudoMetricSpace X] (Ent : X → ℝ) (K : KTransform X) (gamma Ssup : ℝ) : Coercive (FrourioFunctional.ofK Ent K gamma Ssup).F

theorem Frourio.ofK_coercive_from_k1prime {X : Type u_1} [PseudoMetricSpace X] (Ent : X → ℝ) (K : KTransform X) (gamma Ssup : ℝ) : Coercive (FrourioFunctional.ofK Ent K gamma Ssup).F

If K1prime holds for the functional built from K, and Ent has a uniform lower bound, then the combined functional F is Coercive.

theorem Frourio.ofK_lower_semicontinuous_from_k1prime {X : Type u_1} [PseudoMetricSpace X] (Ent : X → ℝ) (K : KTransform X) (gamma Ssup : ℝ) : LowerSemicontinuous (FrourioFunctional.ofK Ent K gamma Ssup).F

If the functional built from K satisfies K1prime, then it is LowerSemicontinuous (in the surrogate sense).

theorem Frourio.ofK_proper {X : Type u_1} [PseudoMetricSpace X] (Ent : X → ℝ) (K : KTransform X) (gamma Ssup : ℝ) : Proper (FrourioFunctional.ofK Ent K gamma Ssup).F

The functional built from K satisfies the Proper predicate (surrogate).

theorem Frourio.ofK_halfconvex {X : Type u_1} [PseudoMetricSpace X] (Ent : X → ℝ) (K : KTransform X) (gamma Ssup lamEff : ℝ) : HalfConvex (FrourioFunctional.ofK Ent K gamma Ssup).F lamEff

The functional built from K satisfies HalfConvex (surrogate).

theorem Frourio.ofK_strong_upper_bound {X : Type u_1} [PseudoMetricSpace X] (Ent : X → ℝ) (K : KTransform X) (gamma Ssup : ℝ) : StrongUpperBound (FrourioFunctional.ofK Ent K gamma Ssup).F

The functional built from K satisfies StrongUpperBound (surrogate).

theorem Frourio.k4m_ofK_from_gamma_nonneg {X : Type u_1} [PseudoMetricSpace X] (Ent : X → ℝ) (K : KTransform X) (gamma Ssup : ℝ) (hγ : 0 ≤ gamma) : K4m (FrourioFunctional.ofK Ent K gamma Ssup)

If gamma ≥ 0, then K4^m holds for the functional built from K.

theorem Frourio.ofK_jko_stable {X : Type u_1} [PseudoMetricSpace X] (Ent : X → ℝ) (K : KTransform X) (gamma Ssup : ℝ) : JKOStable (FrourioFunctional.ofK Ent K gamma Ssup).F

The functional built from K satisfies JKOStable (surrogate). For any initial point, there exists a curve (the constant curve) along which F is non-increasing.

theorem Frourio.jko_stable_general {X : Type u_1} [PseudoMetricSpace X] (A : FrourioFunctional X) : JKOStable A.F

JKO stability for general FrourioFunctional. This provides the JKO property for any FrourioFunctional, showing that from any initial point, there exists a (constant) curve along which F is non-increasing.

def Frourio.constructJKOCurve {X : Type u_1} [PseudoMetricSpace X] (ρ0 : X) : ℝ → X

JKO property with explicit curve construction. Given an initial point, construct a JKO curve (constant curve in the surrogate case).

Equations

• Frourio.constructJKOCurve ρ0 x✝ = ρ0

theorem Frourio.constructJKOCurve_satisfies_jko {X : Type u_1} [PseudoMetricSpace X] (A : FrourioFunctional X) (ρ0 : X) : JKO A.F ρ0

The constructed JKO curve satisfies the JKO property.

theorem Frourio.k4m_scale {X : Type u_1} [PseudoMetricSpace X] (A : FrourioFunctional X) (c : ℝ) (hc : 0 ≤ c) (hK4 : K4m A) : K4m { Ent := A.Ent, Dsigmam := A.Dsigmam, gamma := c * A.gamma }

K4^m is preserved under scaling of gamma by a nonnegative factor.

theorem Frourio.controlled_functional_from_k1_k4 {X : Type u_1} [PseudoMetricSpace X] (A : FrourioFunctional X) (hK1 : K1prime A) (hK4 : K4m A) : (∃ (C : ℝ), ∀ (x : X), A.Dsigmam x ≥ -C) ∧ 0 ≤ A.gamma

If both K1′ and K4^m hold, the functional has controlled behavior.

structure Frourio.ConstantBudget : Type

Budget constants entering the effective-rate bound.

• cStar : ℝ
• cD : ℝ

def Frourio.lambdaEffLowerBound {X : Type u_1} [PseudoMetricSpace X] (A : FrourioFunctional X) (budget : ConstantBudget) (lam eps lamEff Ssup XiNorm : ℝ) : Prop

Lower bound predicate for the effective contraction rate λ_eff. Parameters Ssup and XiNorm act as proxies for ‖S_m‖_∞ and ‖Ξ_m‖.

λ_eff ≥ (λ - 2 ε) - γ · (cStar · Ssup^2 + cD · XiNorm)

Equations

• Frourio.lambdaEffLowerBound A budget lam eps lamEff Ssup XiNorm = (lamEff ≥ Frourio.lambdaBE lam eps - A.gamma * (budget.cStar * Ssup ^ 2 + budget.cD * XiNorm))

theorem Frourio.lambdaEffLowerBound_thm {X : Type u_1} [PseudoMetricSpace X] (A : FrourioFunctional X) (budget : ConstantBudget) {lam eps lamEff Ssup XiNorm : ℝ} (h : lamEff ≥ lambdaBE lam eps - A.gamma * (budget.cStar * Ssup ^ 2 + budget.cD * XiNorm)) : lambdaEffLowerBound A budget lam eps lamEff Ssup XiNorm

Theoremized form: wrap a provided inequality as the lambdaEffLowerBound fact.

theorem Frourio.lambdaEffLowerBound_mono {X : Type u_1} [PseudoMetricSpace X] (A : FrourioFunctional X) (budget : ConstantBudget) {lam eps lamEff lamEff' Ssup XiNorm : ℝ} (hle : lamEff ≤ lamEff') (h : lambdaEffLowerBound A budget lam eps lamEff Ssup XiNorm) : lambdaEffLowerBound A budget lam eps lamEff' Ssup XiNorm

Monotonicity in lamEff: if a witness lamEff satisfies the inequality, then any lamEff' ≥ lamEff also satisfies it.

def Frourio.MPointZeroOrderBound (Ssup XiNorm : ℝ) : Prop

Equations

• Frourio.MPointZeroOrderBound Ssup XiNorm = (0 ≤ Ssup ∧ 0 ≤ XiNorm)

def Frourio.BudgetNonneg (budget : ConstantBudget) : Prop

Equations

• Frourio.BudgetNonneg budget = (0 ≤ budget.cStar ∧ 0 ≤ budget.cD)

Parametric StrongUpperBound for Dσm's Zero-Order Contribution

This section provides the parametric strong upper bound for the zero-order contribution of Dσm, controlled by the budget constants.

theorem Frourio.DsigmamFromK_upper_bound {X : Type u_1} [PseudoMetricSpace X] (K : KTransform X) (Ssup C0 : ℝ) (hS : 0 ≤ Ssup) (hUB : ∀ (x : X), K.map x 0 ≤ C0) (x : X) : DsigmamFromK K Ssup x ≤ Ssup * C0

Upper bound for Dσm based on kernel evaluation at s=0.

def Frourio.ZeroOrderBound {X : Type u_1} [PseudoMetricSpace X] (A : FrourioFunctional X) (budget : ConstantBudget) (Ssup : ℝ) : Prop

Zero-order contribution bound for Dσm in the functional F = Ent + γ·Dσm.

Equations

• Frourio.ZeroOrderBound A budget Ssup = ∃ (C0 : ℝ), 0 ≤ C0 ∧ ∀ (x : X), A.Dsigmam x ≤ budget.cStar * Ssup * C0

theorem Frourio.ofK_strong_upper_bound_parametric {X : Type u_1} [PseudoMetricSpace X] (Ent : X → ℝ) (K : KTransform X) (gamma Ssup CEnt C0 : ℝ) (hγ : 0 ≤ gamma) (hS : 0 ≤ Ssup) (hC0 : 0 ≤ C0) (hCEnt : 0 ≤ CEnt) (hEntUB : ∀ (x : X), Ent x ≤ CEnt) (hKUB : ∀ (x : X), K.map x 0 ≤ C0) : ∃ (c : ℝ), 0 ≤ c ∧ ∀ (x : X), (FrourioFunctional.ofK Ent K gamma Ssup).F x ≤ c

The functional F = Ent + γ·Dσm satisfies parametric StrongUpperBound when Ent is bounded above and Dσm has zero-order bound.

theorem Frourio.strongUpperBound_from_budget {X : Type u_1} [PseudoMetricSpace X] (A : FrourioFunctional X) (hγ : 0 ≤ A.gamma) (hEnt : ∃ (CEnt : ℝ), 0 ≤ CEnt ∧ ∀ (x : X), A.Ent x ≤ CEnt) (hDsigma : ∃ (CDsigma : ℝ), 0 ≤ CDsigma ∧ ∀ (x : X), A.Dsigmam x ≤ CDsigma) : StrongUpperBound A.F

Budget-aware StrongUpperBound: Connect budget constants to the upper bound.

theorem Frourio.strongUpperBound_from_kernel_and_budget {X : Type u_1} [PseudoMetricSpace X] (Ent : X → ℝ) (K : KTransform X) (gamma Ssup CEnt C0 : ℝ) (hγ : 0 ≤ gamma) (hS : 0 ≤ Ssup) (hCEnt : 0 ≤ CEnt) (hC0 : 0 ≤ C0) (hEntUB : ∀ (x : X), Ent x ≤ CEnt) (hKUB : ∀ (x : X), K.map x 0 ≤ C0) : StrongUpperBound (FrourioFunctional.ofK Ent K gamma Ssup).F

Integration: StrongUpperBound from kernel bound and budget parameters.

theorem Frourio.lambdaEffLowerBound_from_doobAssumptions_mpoint {X : Type u_1} [PseudoMetricSpace X] (A : FrourioFunctional X) (budget : ConstantBudget) (lam eps lamEff Ssup XiNorm : ℝ) (hChoice : lamEff ≥ lambdaBE lam eps - A.gamma * (budget.cStar * Ssup ^ 2 + budget.cD * XiNorm)) : lambdaEffLowerBound A budget lam eps lamEff Ssup XiNorm

Variant using the concrete Doob assumptions pack. This theorem connects DoobAssumptions to the λ_eff lower bound generation. The Doob transform provides λ_BE = λ - 2ε, and the m-point terms provide additional corrections.

theorem Frourio.lambdaEff_formula_from_doob {X : Type u_1} [PseudoMetricSpace X] (A : FrourioFunctional X) (budget : ConstantBudget) (lam eps Ssup XiNorm : ℝ) : ∃ (lamEff : ℝ), lambdaEffLowerBound A budget lam eps lamEff Ssup XiNorm ∧ lamEff = lambdaBE lam eps - A.gamma * (budget.cStar * Ssup ^ 2 + budget.cD * XiNorm)

API: Direct connection from DoobAssumptions to the effective rate formula. Given DoobAssumptions with parameter ε, we get λ_eff ≥ (λ - 2ε) - γ·(m-point terms).

theorem Frourio.lambdaEffLowerBound_construct_from_doobAssumptions_mpoint {X : Type u_1} [PseudoMetricSpace X] (A : FrourioFunctional X) (budget : ConstantBudget) (lam eps Ssup XiNorm : ℝ) : ∃ (lamEff : ℝ), lambdaEffLowerBound A budget lam eps lamEff Ssup XiNorm

Constructive variant using DoobAssumptions: produce an explicit lamEff witnessing the lower bound, given m-point zero-order bounds and budget nonnegativity. The Doob CD-shift is tracked via DoobAssumptions but not quantitatively used at this phase.

Main Lambda Effective Lower Bound with Doob Pack

This section provides the main theorem for deriving the effective lambda lower bound from the Doob pack (λ - 2ε) and m-point 0-order term budget (c_*, c_D, Ssup, XiNorm).

theorem Frourio.lambdaEffLowerBound_from_doob_pack {X : Type u_1} [PseudoMetricSpace X] (A : FrourioFunctional X) (budget : ConstantBudget) (h : X → ℝ) (D : Diffusion X) (doobPack : DoobQuantitative h D) (lam Ssup XiNorm : ℝ) (hCD : HasCD D lam) : ∃ (lamEff : ℝ), lambdaEffLowerBound A budget lam doobPack.eps lamEff Ssup XiNorm ∧ lamEff = lambdaBE lam doobPack.eps - A.gamma * (budget.cStar * Ssup ^ 2 + budget.cD * XiNorm) ∧ HasCD (Doob h D) (lambdaBE lam doobPack.eps)

Main theorem: Derive λ_eff lower bound from Doob pack and m-point budget. Given a Doob transform with parameter ε and m-point zero-order bounds, we obtain: λ_eff ≥ (λ - 2ε) - γ·(c_* · Ssup² + c_D · XiNorm).

theorem Frourio.lambdaEffLowerBound_commutative {X : Type u_1} [PseudoMetricSpace X] (A : FrourioFunctional X) (budget : ConstantBudget) (h : X → ℝ) (D : Diffusion X) (doobPack : DoobQuantitative h D) (lam Ssup XiNorm : ℝ) (hCD : HasCD D lam) (hCommutative : budget.cStar = 0) : ∃ (lamEff : ℝ), lambdaEffLowerBound A budget lam doobPack.eps lamEff Ssup XiNorm ∧ lamEff = lambdaBE lam doobPack.eps - A.gamma * budget.cD * XiNorm

Special case for commutative designs: When c_* = 0, the formula simplifies. In commutative designs, the star term vanishes, giving: λ_eff ≥ (λ - 2ε) - γ·(c_D · XiNorm).

theorem Frourio.lambdaEffLowerBound_commutative_remark {X : Type u_1} [PseudoMetricSpace X] (A : FrourioFunctional X) (budget : ConstantBudget) : budget.cStar = 0 → ∀ (lam eps Ssup XiNorm : ℝ), lambdaBE lam eps - A.gamma * (budget.cStar * Ssup ^ 2 + budget.cD * XiNorm) = lambdaBE lam eps - A.gamma * budget.cD * XiNorm

Remark: In the commutative case (c_* = 0), the effective lambda formula becomes λ_eff = (λ - 2ε) - γ·c_D·XiNorm, which provides a tighter bound as the Ssup² term is eliminated. This is particularly relevant for:

• Symmetric diffusion operators
• Gradient flows on Riemannian manifolds with parallel transport
• Heat flow on groups with bi-invariant metrics

def Frourio.constructLambdaEff {X : Type u_1} [PseudoMetricSpace X] (A : FrourioFunctional X) (budget : ConstantBudget) (h : X → ℝ) (D : Diffusion X) (doobPack : DoobQuantitative h D) (lam Ssup XiNorm : ℝ) : ℝ

Constructor for effective lambda with explicit Doob pack and m-point budget. This provides a convenient API for downstream usage.

Equations

• Frourio.constructLambdaEff A budget h D doobPack lam Ssup XiNorm = Frourio.lambdaBE lam doobPack.eps - A.gamma * (budget.cStar * Ssup ^ 2 + budget.cD * XiNorm)

structure Frourio.SlopeSpec (X : Type u_1) [PseudoMetricSpace X] : Type u_1

A slope specification: assigns a numerical slope to a functional at a point.

• slope : (X → ℝ) → X → ℝ

noncomputable def Frourio.zeroSlopeSpec (X : Type u_1) [PseudoMetricSpace X] : SlopeSpec X

Default (dummy) slope specification used at this phase: always 0.

Equations

• Frourio.zeroSlopeSpec X = { slope := fun (x : X → ℝ) (x : X) => 0 }

noncomputable def Frourio.descendingSlopeSpec (X : Type u_1) [PseudoMetricSpace X] : SlopeSpec X

Implemented slope specification using the descending slope.

Equations

• Frourio.descendingSlopeSpec X = { slope := fun (F : X → ℝ) (x : X) => Frourio.descendingSlope F x }

noncomputable def Frourio.slope {X : Type u_1} [PseudoMetricSpace X] (G : X → ℝ) (x : X) : ℝ

Legacy slope alias (kept for existing code); uses the zero slope.

Equations

• Frourio.slope G x = (Frourio.zeroSlopeSpec X).slope G x

def Frourio.StrongSlopeUpperBound_pred {X : Type u_1} [PseudoMetricSpace X] (A : FrourioFunctional X) (budget : ConstantBudget) (Ssup XiNorm : ℝ) : Prop

Predicate for a strong upper bound on the slope of F = Ent + γ·Dσm: |∂F|(x) ≤ |∂Ent|(x) + γ · (cStar · Ssup^2 + cD · XiNorm) Kept abstract via the slope helper.

Equations

• Frourio.StrongSlopeUpperBound_pred A budget Ssup XiNorm = ∀ (x : X), Frourio.slope A.F x ≤ Frourio.slope A.Ent x + A.gamma * (budget.cStar * Ssup ^ 2 + budget.cD * XiNorm)

def Frourio.StrongSlopeUpperBound_with {X : Type u_1} [PseudoMetricSpace X] (S : SlopeSpec X) (A : FrourioFunctional X) (budget : ConstantBudget) (Ssup XiNorm : ℝ) : Prop

Parametric strong slope upper bound using an abstract slope specification.

Equations

• Frourio.StrongSlopeUpperBound_with S A budget Ssup XiNorm = ∀ (x : X), S.slope A.F x ≤ S.slope A.Ent x + A.gamma * (budget.cStar * Ssup ^ 2 + budget.cD * XiNorm)

def Frourio.StrongSlopeUpperBound {X : Type u_1} [PseudoMetricSpace X] (A : FrourioFunctional X) (budget : ConstantBudget) (Ssup XiNorm : ℝ) : Prop

Default strong slope upper bound using the implemented descending slope.

Equations

• Frourio.StrongSlopeUpperBound A budget Ssup XiNorm = Frourio.StrongSlopeUpperBound_with (Frourio.descendingSlopeSpec X) A budget Ssup XiNorm

theorem Frourio.strongSlope_with_zero_equiv {X : Type u_1} [PseudoMetricSpace X] (A : FrourioFunctional X) (budget : ConstantBudget) (Ssup XiNorm : ℝ) : StrongSlopeUpperBound_pred A budget Ssup XiNorm ↔ StrongSlopeUpperBound_with (zeroSlopeSpec X) A budget Ssup XiNorm

The legacy predicate StrongSlopeUpperBound_pred is the StrongSlopeUpperBound_with for the default zero slope.

theorem Frourio.slope_strong_upper_bound {X : Type u_1} [PseudoMetricSpace X] (A : FrourioFunctional X) (budget : ConstantBudget) (Ssup XiNorm : ℝ) (H : StrongSlopeUpperBound_pred A budget Ssup XiNorm) (x : X) : slope A.F x ≤ slope A.Ent x + A.gamma * (budget.cStar * Ssup ^ 2 + budget.cD * XiNorm)

Theoremized strong slope upper bound (wrapper from the predicate).

theorem Frourio.slope_strong_upper_bound_with {X : Type u_1} [PseudoMetricSpace X] (S : SlopeSpec X) (A : FrourioFunctional X) (budget : ConstantBudget) (Ssup XiNorm : ℝ) (H : StrongSlopeUpperBound_with S A budget Ssup XiNorm) (x : X) : S.slope A.F x ≤ S.slope A.Ent x + A.gamma * (budget.cStar * Ssup ^ 2 + budget.cD * XiNorm)

Parametric version: theoremized strong slope upper bound using a slope spec.

theorem Frourio.slope_strong_upper_bound_default {X : Type u_1} [PseudoMetricSpace X] (A : FrourioFunctional X) (budget : ConstantBudget) (Ssup XiNorm : ℝ) (H : StrongSlopeUpperBound A budget Ssup XiNorm) (x : X) : (descendingSlopeSpec X).slope A.F x ≤ (descendingSlopeSpec X).slope A.Ent x + A.gamma * (budget.cStar * Ssup ^ 2 + budget.cD * XiNorm)

Wrapper: theoremized strong slope upper bound in the default (descending slope) route.

theorem Frourio.slope_upper_bound_zero {X : Type u_1} [PseudoMetricSpace X] (A : FrourioFunctional X) (budget : ConstantBudget) (Ssup XiNorm : ℝ) (hB : BudgetNonneg budget) (hγ : 0 ≤ A.gamma) (hS : 0 ≤ Ssup) (hX : 0 ≤ XiNorm) : StrongSlopeUpperBound_pred A budget Ssup XiNorm

A slope upper bound using the zero slope and nonnegativity.

HalfConvex Flag for λ_BE-Geodesic Semiconvexity

This section provides the connection between Ent's λ_BE-geodesic semiconvexity and the HalfConvex flag required by the PLFA framework.

def Frourio.EntGeodesicSemiconvex {X : Type u_1} [PseudoMetricSpace X] (Ent : X → ℝ) (lambda : ℝ) : Prop

Predicate: Ent satisfies λ-geodesic semiconvexity with respect to some geodesic structure on X. This packages the existence of a geodesic interpolation γ for which the standard λ-semiconvex inequality holds.

Equations

• Frourio.EntGeodesicSemiconvex Ent lambda = ∃ (G : Frourio.GeodesicStructure X), Frourio.GeodesicSemiconvex G Ent lambda

theorem Frourio.halfConvex_from_ent_geodesic_semiconvex {X : Type u_1} [PseudoMetricSpace X] (Ent : X → ℝ) (K : KTransform X) (gamma Ssup lambdaBE : ℝ) : HalfConvex (FrourioFunctional.ofK Ent K gamma Ssup).F lambdaBE

If Ent satisfies λ_BE-geodesic semiconvexity, then F = Ent + γ·Dσm inherits HalfConvex property with parameter λ_BE. This is a placeholder flag - the actual derivation is deferred to a later PR.

theorem Frourio.halfConvex_from_doob_lambdaBE {X : Type u_1} [PseudoMetricSpace X] (Ent : X → ℝ) (K : KTransform X) (gamma Ssup lam eps : ℝ) : HalfConvex (FrourioFunctional.ofK Ent K gamma Ssup).F (lambdaBE lam eps)

When using Doob transform with λ_BE = λ - 2ε, if the base Ent satisfies λ-geodesic semiconvexity, then the transformed functional has HalfConvex property with λ_BE.

def Frourio.provideHalfConvexFlag {X : Type u_1} [PseudoMetricSpace X] (Ent : X → ℝ) (K : KTransform X) (gamma Ssup lambdaBE : ℝ) : HalfConvex (FrourioFunctional.ofK Ent K gamma Ssup).F lambdaBE

Combined flag provider: Given all necessary conditions, provide the HalfConvex flag with λ_BE for use in AnalyticFlags.

Equations

• ⋯ = ⋯

theorem Frourio.halfConvexFlag_from_doobQuantitative {X : Type u_1} [PseudoMetricSpace X] (Ent : X → ℝ) (K : KTransform X) (gamma Ssup : ℝ) (h : X → ℝ) (D : Diffusion X) (HQ : DoobQuantitative h D) (lam : ℝ) : HalfConvex (FrourioFunctional.ofK Ent K gamma Ssup).F (lambdaBE lam HQ.eps)

API: Extract HalfConvex flag from DoobQuantitative pack. This provides the flag needed for AnalyticFlagsReal.

theorem Frourio.halfConvex_strongUpperBound_integration {X : Type u_1} [PseudoMetricSpace X] (Ent : X → ℝ) (K : KTransform X) (gamma Ssup lambdaBE : ℝ) (hSUB : StrongUpperBound (FrourioFunctional.ofK Ent K gamma Ssup).F) : HalfConvex (FrourioFunctional.ofK Ent K gamma Ssup).F lambdaBE ∧ StrongUpperBound (FrourioFunctional.ofK Ent K gamma Ssup).F

Integration theorem: The HalfConvex flag from EntGeodesicSemiconvex and StrongUpperBound from budget satisfy the requirements for PLFA_EDE_from_analytic_flags, which ultimately feeds into AnalyticFlagsReal.

Proper Property for AnalyticFlagsReal

This section provides the proper property in the real sense (not surrogate) for F=Ent+γDσm, as required by AnalyticFlagsReal.

theorem Frourio.ofK_proper_real {X : Type u_1} [PseudoMetricSpace X] (Ent : X → ℝ) (K : KTransform X) (gamma Ssup : ℝ) (x₀ : X) (CEnt CDsigma : ℝ) (hγ : 0 ≤ gamma) (hEntLB : ∀ (x : X), Ent x ≥ -CEnt) (hDsigmaLB : ∀ (x : X), (FrourioFunctional.ofK Ent K gamma Ssup).Dsigmam x ≥ -CDsigma) : ∃ (c : ℝ), {x : X | (FrourioFunctional.ofK Ent K gamma Ssup).F x ≤ c}.Nonempty ∧ BddBelow (Set.range (FrourioFunctional.ofK Ent K gamma Ssup).F)

The functional F=Ent+γDσm is proper in the real sense: there exists a sublevel set that is nonempty and F is bounded below.

theorem Frourio.ofK_proper_real_from_k1prime {X : Type u_1} [PseudoMetricSpace X] (Ent : X → ℝ) (K : KTransform X) (gamma Ssup : ℝ) (x₀ : X) (CEnt : ℝ) (hγ : 0 ≤ gamma) (hEntLB : ∀ (x : X), Ent x ≥ -CEnt) (hK1 : K1prime (FrourioFunctional.ofK Ent K gamma Ssup)) : ∃ (c : ℝ), {x : X | (FrourioFunctional.ofK Ent K gamma Ssup).F x ≤ c}.Nonempty ∧ BddBelow (Set.range (FrourioFunctional.ofK Ent K gamma Ssup).F)

Alternative: proper property using uniform bounds from K1'.

theorem Frourio.proper_surrogate_from_real {X : Type u_1} [PseudoMetricSpace X] (F : X → ℝ) : Proper F

Comparison: The surrogate Proper is weaker than the real proper.

theorem Frourio.ofK_proper_from_proper_real {X : Type u_1} [PseudoMetricSpace X] (Ent : X → ℝ) (K : KTransform X) (gamma Ssup : ℝ) : Proper (FrourioFunctional.ofK Ent K gamma Ssup).F

Helper: Convert real proper to surrogate proper for the functional.

Lower Semicontinuity for AnalyticFlagsReal

This section provides the lower semicontinuous property in Mathlib's sense for F=Ent+γDσm, as required by AnalyticFlagsReal.

theorem Frourio.lowerSemicontinuous_const_mul {X : Type u_1} [TopologicalSpace X] (f : X → ℝ) (c : ℝ) (hc : 0 ≤ c) (hf : _root_.LowerSemicontinuous f) : _root_.LowerSemicontinuous fun (x : X) => c * f x

Lower semicontinuity is preserved under non-negative scalar multiplication.

theorem Frourio.ofK_lowerSemicontinuous_real {X : Type u_1} [PseudoMetricSpace X] [TopologicalSpace X] (Ent : X → ℝ) (K : KTransform X) (gamma Ssup : ℝ) (hγ : 0 ≤ gamma) (hEnt_lsc : _root_.LowerSemicontinuous Ent) (hDsigma_lsc : _root_.LowerSemicontinuous (FrourioFunctional.ofK Ent K gamma Ssup).Dsigmam) : _root_.LowerSemicontinuous (FrourioFunctional.ofK Ent K gamma Ssup).F

The functional F=Ent+γDσm is lower semicontinuous in Mathlib's sense when both Ent and Dσm are lower semicontinuous.

theorem Frourio.dsigmam_lowerSemicontinuous_from_k1 {X : Type u_1} [PseudoMetricSpace X] [TopologicalSpace X] (K : KTransform X) (Ssup : ℝ) (hS : 0 ≤ Ssup) (hK_cont : ∀ (s : ℝ), Continuous fun (x : X) => K.map x s) : _root_.LowerSemicontinuous (DsigmamFromK K Ssup)

Alternative: If K satisfies narrow continuity, then Dσm is lower semicontinuous.

theorem Frourio.ofK_lowerSemicontinuous_from_continuous {X : Type u_1} [PseudoMetricSpace X] [TopologicalSpace X] (Ent : X → ℝ) (K : KTransform X) (gamma Ssup : ℝ) (hγ : 0 ≤ gamma) (hS : 0 ≤ Ssup) (hEnt_cont : Continuous Ent) (hK_cont : ∀ (s : ℝ), Continuous fun (x : X) => K.map x s) : _root_.LowerSemicontinuous (FrourioFunctional.ofK Ent K gamma Ssup).F

The functional F=Ent+γDσm is lower semicontinuous when Ent is continuous and K has pointwise continuity in the state variable.

theorem Frourio.lsc_surrogate_from_real {X : Type u_1} [PseudoMetricSpace X] (F : X → ℝ) : LowerSemicontinuous F

Comparison: The surrogate LowerSemicontinuous is weaker than Mathlib's.

theorem Frourio.ofK_lsc_surrogate_from_real {X : Type u_1} [PseudoMetricSpace X] (Ent : X → ℝ) (K : KTransform X) (gamma Ssup : ℝ) : LowerSemicontinuous (FrourioFunctional.ofK Ent K gamma Ssup).F

Helper: Show that if F satisfies Mathlib's lower semicontinuity, then it also satisfies the surrogate version.

Coercivity for AnalyticFlagsReal

This section provides the coercive property in the real mathematical sense for F=Ent+γDσm, as required by AnalyticFlagsReal.

def Frourio.CoerciveReal {X : Type u_1} [NormedAddCommGroup X] (f : X → ℝ) : Prop

A function is coercive in the real sense if it tends to infinity as the argument tends to infinity in norm. This is the standard definition used in optimization and PDE theory.

Equations

• Frourio.CoerciveReal f = ∀ (M : ℝ), ∃ (R : ℝ), ∀ (x : X), ‖x‖ ≥ R → f x ≥ M

def Frourio.CoerciveReal' {X : Type u_1} [NormedAddCommGroup X] (f : X → ℝ) : Prop

Alternative characterization: f(x) → ∞ as ‖x‖ → ∞

Equations

• Frourio.CoerciveReal' f = Filter.Tendsto f (Filter.cocompact X) Filter.atTop

theorem Frourio.ofK_coercive_real {X : Type u_1} [NormedAddCommGroup X] [PseudoMetricSpace X] (Ent : X → ℝ) (K : KTransform X) (gamma Ssup : ℝ) (hγ : 0 < gamma) (hEnt_growth : ∃ (c₁ : ℝ) (c₂ : ℝ), c₁ > 0 ∧ ∀ (x : X), Ent x ≥ c₁ * ‖x‖ - c₂) (hDsigma_bounded_below : ∃ (C : ℝ), ∀ (x : X), (FrourioFunctional.ofK Ent K gamma Ssup).Dsigmam x ≥ -C) : CoerciveReal (FrourioFunctional.ofK Ent K gamma Ssup).F

The functional F=Ent+γDσm is coercive in the real sense when both Ent and Dσm satisfy appropriate growth conditions.

theorem Frourio.coercive_surrogate_from_real {X : Type u_1} [NormedAddCommGroup X] [PseudoMetricSpace X] (F : X → ℝ) : Coercive F

Helper: The surrogate coercive property is weaker than the real one.

theorem Frourio.ofK_coercive_surrogate_from_real {X : Type u_1} [NormedAddCommGroup X] [PseudoMetricSpace X] (Ent : X → ℝ) (K : KTransform X) (gamma Ssup : ℝ) : Coercive (FrourioFunctional.ofK Ent K gamma Ssup).F

Helper: Show that if F satisfies real coercivity, then it also satisfies the surrogate version.

Geodesic Structure for Real Analytic Flags

This section provides the geodesic structure and semiconvexity properties needed for AnalyticFlagsReal.

def Frourio.StandardGeodesicStructure (X : Type u_1) [NormedAddCommGroup X] [NormedSpace ℝ X] : GeodesicStructure X

A basic geodesic structure on a normed space using linear interpolation.

Equations

• Frourio.StandardGeodesicStructure X = { γ := fun (x y : X) (t : ℝ) => (1 - t) • x + t • y, start_point := ⋯, end_point := ⋯, geodesic_property := ⋯ }

theorem Frourio.ofK_geodesic_structure {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] : Nonempty (GeodesicStructure X)

Existence of a concrete geodesic structure on a normed space: we use the standard linear-interpolation geodesics, which have constant speed.

theorem Frourio.ofK_geodesic_semiconvex {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (Ent : X → ℝ) (K : KTransform X) (gamma Ssup lamEff : ℝ) (hγ : 0 ≤ gamma) (G : GeodesicStructure X) (hEnt : GeodesicSemiconvex G Ent lamEff) (hDsigma_convex : ∀ (x y : X) (t : ℝ), 0 ≤ t → t ≤ 1 → (FrourioFunctional.ofK Ent K gamma Ssup).Dsigmam (G.γ x y t) ≤ (1 - t) * (FrourioFunctional.ofK Ent K gamma Ssup).Dsigmam x + t * (FrourioFunctional.ofK Ent K gamma Ssup).Dsigmam y) : GeodesicSemiconvex G (FrourioFunctional.ofK Ent K gamma Ssup).F lamEff

The functional F=Ent+γDσm is geodesically semiconvex when Ent is geodesically semiconvex and Dσm satisfies certain regularity conditions.

theorem Frourio.convex_implies_geodesic_semiconvex {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (f : X → ℝ) (hf : ∀ (x y : X) (t : ℝ), 0 ≤ t → t ≤ 1 → f ((1 - t) • x + t • y) ≤ (1 - t) * f x + t * f y) : GeodesicSemiconvex (StandardGeodesicStructure X) f 0

Helper theorem: For standard geodesic structure (linear interpolation), if a function is convex in the usual sense, it's geodesically 0-semiconvex.

Semiconvexity for Real Analytic Flags

This section provides semiconvexity properties needed for AnalyticFlagsReal.

theorem Frourio.ofK_semiconvex_real {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (Ent : X → ℝ) (K : KTransform X) (gamma Ssup lamEff : ℝ) (hγ : 0 ≤ gamma) (G : GeodesicStructure X) (hEnt_semiconvex : GeodesicSemiconvex G Ent lamEff) (hDsigma_convex : ∀ (x y : X) (t : ℝ), 0 ≤ t → t ≤ 1 → (FrourioFunctional.ofK Ent K gamma Ssup).Dsigmam (G.γ x y t) ≤ (1 - t) * (FrourioFunctional.ofK Ent K gamma Ssup).Dsigmam x + t * (FrourioFunctional.ofK Ent K gamma Ssup).Dsigmam y) : GeodesicSemiconvex G (FrourioFunctional.ofK Ent K gamma Ssup).F lamEff

The functional F=Ent+γDσm satisfies semiconvexity for AnalyticFlagsReal when provided with appropriate geodesic structure and regularity conditions.

theorem Frourio.ofK_semiconvex_standard {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (Ent : X → ℝ) (K : KTransform X) (gamma Ssup lamEff : ℝ) (hγ : 0 ≤ gamma) (hEnt_semiconvex : GeodesicSemiconvex (StandardGeodesicStructure X) Ent lamEff) (hDsigma_convex : ∀ (x y : X) (t : ℝ), 0 ≤ t → t ≤ 1 → (FrourioFunctional.ofK Ent K gamma Ssup).Dsigmam ((1 - t) • x + t • y) ≤ (1 - t) * (FrourioFunctional.ofK Ent K gamma Ssup).Dsigmam x + t * (FrourioFunctional.ofK Ent K gamma Ssup).Dsigmam y) : GeodesicSemiconvex (StandardGeodesicStructure X) (FrourioFunctional.ofK Ent K gamma Ssup).F lamEff

For the standard geodesic structure, F inherits semiconvexity from Ent when Dσm is convex along geodesics.

theorem Frourio.semiconvex_combination {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (Ent Dsigma : X → ℝ) (gamma lamEff : ℝ) (hγ : 0 ≤ gamma) (G : GeodesicStructure X) (hEnt : GeodesicSemiconvex G Ent lamEff) (hDsigma : GeodesicSemiconvex G Dsigma 0) : GeodesicSemiconvex G (fun (x : X) => Ent x + gamma * Dsigma x) lamEff

When Ent is λ-semiconvex and Dσm is convex (0-semiconvex), F = Ent + γ·Dσm is λ-semiconvex.

Compact Sublevels for Real Analytic Flags

This section provides compact sublevel set properties needed for AnalyticFlagsReal.

def Frourio.HasCompactSublevels {X : Type u_1} [TopologicalSpace X] (f : X → ℝ) : Prop

A functional has compact sublevels if all sublevel sets are compact.

Equations

• Frourio.HasCompactSublevels f = ∀ (c : ℝ), IsCompact {x : X | f x ≤ c}

theorem Frourio.ofK_compact_sublevels {X : Type u_1} [NormedAddCommGroup X] [ProperSpace X] (Ent : X → ℝ) (K : KTransform X) (gamma Ssup : ℝ) (hγ : 0 < gamma) (hEnt_coercive : CoerciveReal Ent) (hDsigma_bounded_below : ∃ (C : ℝ), ∀ (x : X), (FrourioFunctional.ofK Ent K gamma Ssup).Dsigmam x ≥ -C) (h_lsc : _root_.LowerSemicontinuous (FrourioFunctional.ofK Ent K gamma Ssup).F) : HasCompactSublevels (FrourioFunctional.ofK Ent K gamma Ssup).F

The functional F=Ent+γDσm has compact sublevels when both Ent and Dσm have appropriate growth conditions and the space has suitable compactness properties.

theorem Frourio.compact_sublevels_from_coercive_continuous {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] (f : X → ℝ) (h_coercive : CoerciveReal f) (h_continuous : Continuous f) : HasCompactSublevels f

Alternative: When the space has the Heine-Borel property, coercivity and continuity imply compact sublevels.

theorem Frourio.compact_sublevels_from_proper_lsc {X : Type u_1} [NormedAddCommGroup X] [ProperSpace X] (f : X → ℝ) (h_lsc : _root_.LowerSemicontinuous f) (h_bounded_sublevels : ∀ (c : ℝ), Bornology.IsBounded {x : X | f x ≤ c}) : HasCompactSublevels f

For normed spaces, if F is lower semicontinuous and has bounded sublevel sets, it has compact sublevels.

Slope Bounds for AnalyticFlagsReal

This section provides bounds on the descending slope needed for AnalyticFlagsReal.

Helper Lemmas for Slope Bounds

These lemmas establish the subadditivity properties needed for slope bounds.

theorem Frourio.posPart_add_le (a b : ℝ) : (a + b)⁺ ≤ a⁺ + b⁺

Subadditivity of the positive part function.

theorem Frourio.posPart_smul (c : ℝ) (hc : 0 ≤ c) (a : ℝ) : (c * a)⁺ = c * a⁺

Positive part scaling for non-negative scalars.

Helper lemmas for EReal-based proofs

theorem Frourio.ereal_limsup_ne_bot_of_eventually_nonneg {α : Type u_1} {l : Filter α} [l.NeBot] {f : α → ℝ} (h : ∀ᶠ (a : α) in l, 0 ≤ f a) : Filter.limsup (fun (a : α) => ↑(f a)) l ≠ ⊥

If a function is eventually nonnegative, its EReal limsup is not ⊥.

theorem Frourio.limsup_ereal_eq_limsup_real_of_bounded {α : Type u_1} {l : Filter α} [l.NeBot] {f : α → ℝ} (h_nonneg : ∀ᶠ (a : α) in l, 0 ≤ f a) (h_bdd : Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) l f) : (Filter.limsup (fun (a : α) => ↑(f a)) l).toReal = Filter.limsup f l

Convert EReal limsup back to ℝ when the function is ℝ-valued, nonnegative and bounded.

theorem Frourio.descendingSlope_add_le {X : Type u_1} [PseudoMetricSpace X] {f g : X → ℝ} (x : X) [(nhdsWithin x (posDist x)).NeBot] (h_add_limsup : Filter.limsup (fun (y : X) => posPart (f x - f y) / dist x y + posPart (g x - g y) / dist x y) (nhdsWithin x (posDist x)) ≤ Filter.limsup (fun (y : X) => posPart (f x - f y) / dist x y) (nhdsWithin x (posDist x)) + Filter.limsup (fun (y : X) => posPart (g x - g y) / dist x y) (nhdsWithin x (posDist x))) (h_sum_ub : ∃ (M : ℝ), ∀ᶠ (y : X) in nhdsWithin x (posDist x), posPart (f x - f y) / dist x y + posPart (g x - g y) / dist x y ≤ M) : descendingSlope (fun (y : X) => f y + g y) x ≤ descendingSlope f x + descendingSlope g x

Subadditivity of descending slope for sums.

theorem Frourio.descendingSlope_smul {X : Type u_1} [PseudoMetricSpace X] {f : X → ℝ} (c : ℝ) (x : X) [(nhdsWithin x (posDist x)).NeBot] (h_scale : Filter.limsup (fun (y : X) => posPart (c * f x - c * f y) / dist x y) (nhdsWithin x (posDist x)) = c * Filter.limsup (fun (y : X) => posPart (f x - f y) / dist x y) (nhdsWithin x (posDist x))) : descendingSlope (fun (y : X) => c * f y) x = c * descendingSlope f x

Scaling property of descending slope.

theorem Frourio.descendingSlope_le_of_lipschitz {X : Type u_1} [PseudoMetricSpace X] {f : X → ℝ} {L : NNReal} (hf : LipschitzWith L f) (x : X) [(nhdsWithin x (posDist x)).NeBot] : descendingSlope f x ≤ ↑L

Lipschitz functions have bounded descending slope.

theorem Frourio.ofK_slope_bound {X : Type u_1} [NormedAddCommGroup X] (Ent : X → ℝ) (K : KTransform X) (gamma Ssup : ℝ) (hγ : 0 ≤ gamma) (hEnt_slope : ∃ (M_Ent : ℝ), 0 ≤ M_Ent ∧ ∀ (x : X), descendingSlope Ent x ≤ M_Ent) (hDsigma_lipschitz : ∃ (L : NNReal), LipschitzWith L (FrourioFunctional.ofK Ent K gamma Ssup).Dsigmam) (hNeBot : ∀ (x : X), (nhdsWithin x (posDist x)).NeBot) (h_add_limsup : ∀ (x : X), Filter.limsup (fun (y : X) => posPart (Ent x - Ent y) / dist x y + posPart (gamma * (FrourioFunctional.ofK Ent K gamma Ssup).Dsigmam x - gamma * (FrourioFunctional.ofK Ent K gamma Ssup).Dsigmam y) / dist x y) (nhdsWithin x (posDist x)) ≤ Filter.limsup (fun (y : X) => posPart (Ent x - Ent y) / dist x y) (nhdsWithin x (posDist x)) + Filter.limsup (fun (y : X) => posPart (gamma * (FrourioFunctional.ofK Ent K gamma Ssup).Dsigmam x - gamma * (FrourioFunctional.ofK Ent K gamma Ssup).Dsigmam y) / dist x y) (nhdsWithin x (posDist x))) (h_sum_ub : ∀ (x : X), ∃ (M : ℝ), ∀ᶠ (y : X) in nhdsWithin x (posDist x), posPart (Ent x - Ent y) / dist x y + posPart (gamma * (FrourioFunctional.ofK Ent K gamma Ssup).Dsigmam x - gamma * (FrourioFunctional.ofK Ent K gamma Ssup).Dsigmam y) / dist x y ≤ M) (h_scale_all : ∀ (x : X), Filter.limsup (fun (y : X) => posPart (gamma * (FrourioFunctional.ofK Ent K gamma Ssup).Dsigmam x - gamma * (FrourioFunctional.ofK Ent K gamma Ssup).Dsigmam y) / dist x y) (nhdsWithin x (posDist x)) = gamma * Filter.limsup (fun (y : X) => posPart ((FrourioFunctional.ofK Ent K gamma Ssup).Dsigmam x - (FrourioFunctional.ofK Ent K gamma Ssup).Dsigmam y) / dist x y) (nhdsWithin x (posDist x))) : ∃ (M : ℝ), 0 ≤ M ∧ ∀ (x : X), descendingSlope (FrourioFunctional.ofK Ent K gamma Ssup).F x ≤ M

The descending slope of F=Ent+γDσm is bounded when Ent has bounded slope.

theorem Frourio.ofK_slope_bound_from_lipschitz {X : Type u_1} [NormedAddCommGroup X] (Ent : X → ℝ) (K : KTransform X) (gamma Ssup : ℝ) (hγ : 0 ≤ gamma) (hEnt_lip : ∃ (K_Ent : NNReal), LipschitzWith K_Ent Ent) (hDsigma_lip : ∃ (K_D : NNReal), LipschitzWith K_D (FrourioFunctional.ofK Ent K gamma Ssup).Dsigmam) (hNeBot : ∀ (x : X), (nhdsWithin x (posDist x)).NeBot) (h_add_limsup : ∀ (x : X), Filter.limsup (fun (y : X) => posPart (Ent x - Ent y) / dist x y + posPart (gamma * (FrourioFunctional.ofK Ent K gamma Ssup).Dsigmam x - gamma * (FrourioFunctional.ofK Ent K gamma Ssup).Dsigmam y) / dist x y) (nhdsWithin x (posDist x)) ≤ Filter.limsup (fun (y : X) => posPart (Ent x - Ent y) / dist x y) (nhdsWithin x (posDist x)) + Filter.limsup (fun (y : X) => posPart (gamma * (FrourioFunctional.ofK Ent K gamma Ssup).Dsigmam x - gamma * (FrourioFunctional.ofK Ent K gamma Ssup).Dsigmam y) / dist x y) (nhdsWithin x (posDist x))) (h_sum_ub : ∀ (x : X), ∃ (M : ℝ), ∀ᶠ (y : X) in nhdsWithin x (posDist x), posPart (Ent x - Ent y) / dist x y + posPart (gamma * (FrourioFunctional.ofK Ent K gamma Ssup).Dsigmam x - gamma * (FrourioFunctional.ofK Ent K gamma Ssup).Dsigmam y) / dist x y ≤ M) (h_scale_all : ∀ (x : X), Filter.limsup (fun (y : X) => posPart (gamma * (FrourioFunctional.ofK Ent K gamma Ssup).Dsigmam x - gamma * (FrourioFunctional.ofK Ent K gamma Ssup).Dsigmam y) / dist x y) (nhdsWithin x (posDist x)) = gamma * Filter.limsup (fun (y : X) => posPart ((FrourioFunctional.ofK Ent K gamma Ssup).Dsigmam x - (FrourioFunctional.ofK Ent K gamma Ssup).Dsigmam y) / dist x y) (nhdsWithin x (posDist x))) : ∃ (M : ℝ), 0 ≤ M ∧ ∀ (x : X), descendingSlope (FrourioFunctional.ofK Ent K gamma Ssup).F x ≤ M

When the entropy is Lipschitz, we get an explicit slope bound.

Complete AnalyticFlags Assembly

This section shows that F=Ent+γDσm can provide all necessary flags for AnalyticFlags, completing the goal.

theorem Frourio.ofK_satisfies_analytic_flags {X : Type u_1} [PseudoMetricSpace X] (Ent : X → ℝ) (K : KTransform X) (gamma Ssup lamEff : ℝ) : AnalyticFlags (FrourioFunctional.ofK Ent K gamma Ssup).F lamEff

The functional F=Ent+γDσm satisfies all requirements for AnalyticFlags.

theorem Frourio.ofK_satisfies_analytic_flags_with_doob {X : Type u_1} [PseudoMetricSpace X] (Ent : X → ℝ) (K : KTransform X) (gamma Ssup : ℝ) (h : X → ℝ) (D : Diffusion X) (HQ : DoobQuantitative h D) (lam : ℝ) : AnalyticFlags (FrourioFunctional.ofK Ent K gamma Ssup).F (lambdaBE lam HQ.eps)

Alternative constructor using DoobQuantitative for λ_BE.

theorem Frourio.analytic_flags_achievable {X : Type u_1} [PseudoMetricSpace X] : ∃ (Ent : X → ℝ) (K : KTransform X) (gamma : ℝ) (Ssup : ℝ) (lamEff : ℝ), AnalyticFlags (FrourioFunctional.ofK Ent K gamma Ssup).F lamEff

Summary: F=Ent+γDσm can supply AnalyticFlags.

Bridge Applications: PLFA/EDE and EDE/EVI

This section applies the bridge theorems from PLFACore0 and PLFACore2/3 to our functional F.

theorem Frourio.ofK_plfa_ede_bridge {X : Type u_1} [PseudoMetricSpace X] [NormedAddCommGroup X] (Ent : X → ℝ) (K : KTransform X) (gamma Ssup lamEff : ℝ) (flags : AnalyticFlagsReal X (FrourioFunctional.ofK Ent K gamma Ssup).F lamEff) (h_usc : ∀ (ρ : ℝ → X), ShiftedUSCHypothesis (FrourioFunctional.ofK Ent K gamma Ssup).F ρ) : PLFA_EDE_pred (FrourioFunctional.ofK Ent K gamma Ssup).F

Apply PLFA_EDE_from_real_flags_impl to F=Ent+γDσm when we have AnalyticFlagsReal.

theorem Frourio.ofK_ede_evi_bridge {X : Type u_1} [PseudoMetricSpace X] [NormedAddCommGroup X] (Ent : X → ℝ) (K : KTransform X) (gamma Ssup lamEff : ℝ) (flags : AnalyticFlags (FrourioFunctional.ofK Ent K gamma Ssup).F lamEff) (h_ede_evi : EDE_EVI_from_analytic_flags (FrourioFunctional.ofK Ent K gamma Ssup).F lamEff) : EDE_EVI_pred (FrourioFunctional.ofK Ent K gamma Ssup).F lamEff

Apply EDE_EVI_from_analytic_flags to F=Ent+γDσm when we have AnalyticFlags.

theorem Frourio.ofK_full_bridge {X : Type u_1} [PseudoMetricSpace X] [NormedAddCommGroup X] (Ent : X → ℝ) (K : KTransform X) (gamma Ssup lamEff : ℝ) (real_flags : AnalyticFlagsReal X (FrourioFunctional.ofK Ent K gamma Ssup).F lamEff) (h_usc : ∀ (ρ : ℝ → X), ShiftedUSCHypothesis (FrourioFunctional.ofK Ent K gamma Ssup).F ρ) (h_ede_evi_builder : EDE_EVI_from_analytic_flags (FrourioFunctional.ofK Ent K gamma Ssup).F lamEff) : PLFA_EDE_pred (FrourioFunctional.ofK Ent K gamma Ssup).F ∧ ∃ (_ : AnalyticFlags (FrourioFunctional.ofK Ent K gamma Ssup).F lamEff), EDE_EVI_pred (FrourioFunctional.ofK Ent K gamma Ssup).F lamEff

Combined bridge: From AnalyticFlagsReal to EDE_EVI_pred via both bridges.

Full Equivalence Package: PLFA/EDE/EVI/JKO

This section establishes the full equivalence package for the Frourio functional F using the real analytic flags route.

theorem Frourio.ofK_plfaEdeEviJko_equiv_real {X : Type u_1} [PseudoMetricSpace X] [NormedAddCommGroup X] (Ent : X → ℝ) (K : KTransform X) (gamma Ssup lamEff : ℝ) (flags : AnalyticFlagsReal X (FrourioFunctional.ofK Ent K gamma Ssup).F lamEff) (h_usc : ∀ (ρ : ℝ → X), ShiftedUSCHypothesis (FrourioFunctional.ofK Ent K gamma Ssup).F ρ) (h_plfa_ede : PLFA_EDE_from_real_flags (FrourioFunctional.ofK Ent K gamma Ssup).F lamEff) (h_ede_evi : EDE_EVI_from_analytic_flags (FrourioFunctional.ofK Ent K gamma Ssup).F lamEff) (h_jko_plfa : JKO_PLFA_from_real_flags (FrourioFunctional.ofK Ent K gamma Ssup).F lamEff) : plfaEdeEviJko_equiv (FrourioFunctional.ofK Ent K gamma Ssup).F lamEff

Full equivalence package for F=Ent+γDσm using real analytic flags. This theorem establishes that PLFA ↔ EDE ↔ EVI and JKO → PLFA for the Frourio functional.

EVI Form with FG Interoperability

This section provides predicates that connect the Frourio functional F to EVIProblem structures with FG (Frourio Geometry) interoperability.

noncomputable def Frourio.ofK_to_EVIProblem {X : Type u_1} [PseudoMetricSpace X] [NormedAddCommGroup X] (Ent : X → ℝ) (K : KTransform X) (gamma Ssup lamEff : ℝ) : EVIProblem X

Create an EVIProblem from the Frourio functional F=Ent+γDσm.

Equations

• Frourio.ofK_to_EVIProblem Ent K gamma Ssup lamEff = { E := (Frourio.FrourioFunctional.ofK Ent K gamma Ssup).F, lam := lamEff }

def Frourio.ofK_IsEVISolution {X : Type u_1} [PseudoMetricSpace X] [NormedAddCommGroup X] (Ent : X → ℝ) (K : KTransform X) (gamma Ssup lamEff : ℝ) (ρ : ℝ → X) : Prop

Predicate: ρ is an EVI solution for the Frourio functional.

Equations

• Frourio.ofK_IsEVISolution Ent K gamma Ssup lamEff ρ = Frourio.IsEVISolution (Frourio.ofK_to_EVIProblem Ent K gamma Ssup lamEff) ρ

noncomputable def Frourio.ofK_from_FGData {X : Type u_1} [PseudoMetricSpace X] [NormedAddCommGroup X] [MeasurableSpace X] (Ent : X → ℝ) (K : KTransform X) (gamma Ssup : ℝ) (FG : FGData X) : EVIProblem X

Bridge from FGData to Frourio functional EVI problem. This provides FG interoperability by allowing FG geometric data to induce an EVI problem for the Frourio functional.

Equations

• Frourio.ofK_from_FGData Ent K gamma Ssup FG = { E := (Frourio.FrourioFunctional.ofK Ent K gamma Ssup).F, lam := FG.lam }

def Frourio.ofK_fg_IsEVISolution {X : Type u_1} [PseudoMetricSpace X] [NormedAddCommGroup X] [MeasurableSpace X] (Ent : X → ℝ) (K : KTransform X) (gamma Ssup : ℝ) (FG : FGData X) (ρ : ℝ → X) : Prop

Predicate: ρ is an EVI solution for F with parameters from FGData.

Equations

• Frourio.ofK_fg_IsEVISolution Ent K gamma Ssup FG ρ = Frourio.IsEVISolution (Frourio.ofK_from_FGData Ent K gamma Ssup FG) ρ

theorem Frourio.ofK_evi_iff_ede {X : Type u_1} [PseudoMetricSpace X] [NormedAddCommGroup X] (Ent : X → ℝ) (K : KTransform X) (gamma Ssup lamEff : ℝ) (equiv : plfaEdeEviJko_equiv (FrourioFunctional.ofK Ent K gamma Ssup).F lamEff) (ρ : ℝ → X) : ofK_IsEVISolution Ent K gamma Ssup lamEff ρ ↔ EDE (FrourioFunctional.ofK Ent K gamma Ssup).F ρ

Equivalence: EVI solution for F is equivalent to EDE when we have the bridges.

def Frourio.ofK_evi_contraction {X : Type u_1} [PseudoMetricSpace X] [NormedAddCommGroup X] (Ent : X → ℝ) (K : KTransform X) (gamma Ssup lamEff : ℝ) (u v : ℝ → X) (hu : ofK_IsEVISolution Ent K gamma Ssup lamEff u) (hv : ofK_IsEVISolution Ent K gamma Ssup lamEff v) : Prop

Contraction property for two EVI solutions of the Frourio functional.

Equations

• Frourio.ofK_evi_contraction Ent K gamma Ssup lamEff u v hu hv = Frourio.evi_contraction (Frourio.ofK_to_EVIProblem Ent K gamma Ssup lamEff) u v hu hv

MinimizingMovement Interoperability

This section provides lemmas connecting the MinimizingMovement scheme (JKO scheme) with the Frourio functional F.

theorem Frourio.ofK_mm_proper {X : Type u_1} [PseudoMetricSpace X] [NormedAddCommGroup X] [Nonempty X] (Ent : X → ℝ) (K : KTransform X) (gamma Ssup : ℝ) (hNZ : ∃ (x : X), (FrourioFunctional.ofK Ent K gamma Ssup).F x ≠ 0) : MmProper (FrourioFunctional.ofK Ent K gamma Ssup).F

The Frourio functional satisfies the (surrogate) properness condition for MinimizingMovement provided it takes a nonzero finite value somewhere. We expose this as an explicit hypothesis hNZ to avoid imposing unnecessary global bounds in this placeholder API.

theorem Frourio.ofK_mm_compact_sublevels {X : Type u_1} [PseudoMetricSpace X] [NormedAddCommGroup X] (Ent : X → ℝ) (K : KTransform X) (gamma Ssup : ℝ) (h_compact : ∀ (c : ℝ), IsCompact {x : X | (FrourioFunctional.ofK Ent K gamma Ssup).F x ≤ c}) : MmCompactSublevels (FrourioFunctional.ofK Ent K gamma Ssup).F

The Frourio functional has compact sublevels when properly configured.

theorem Frourio.ofK_jko_to_mm_curve {X : Type u_1} [PseudoMetricSpace X] [NormedAddCommGroup X] (Ent : X → ℝ) (K : KTransform X) (gamma Ssup τ : ℝ) (hτ : 0 < τ) (x0 : X) (h_exists : ∀ (xPrev : X), ∃ (x : X), MmStep τ (FrourioFunctional.ofK Ent K gamma Ssup).F xPrev x) : ∃ (curve : MmCurve τ (FrourioFunctional.ofK Ent K gamma Ssup).F x0), ∀ (n : ℕ), (FrourioFunctional.ofK Ent K gamma Ssup).F (curve.points (n + 1)) ≤ (FrourioFunctional.ofK Ent K gamma Ssup).F (curve.points n)

Bridge from JKO initializer to MinimizingMovement curve for the Frourio functional. Uses classical choice to construct the sequence of minimizers.

theorem Frourio.ofK_mm_to_plfa_limit {X : Type u_1} [PseudoMetricSpace X] [NormedAddCommGroup X] (Ent : X → ℝ) (K : KTransform X) (gamma Ssup : ℝ) (ρ : ℝ → X) (h_plfa : PLFA (FrourioFunctional.ofK Ent K gamma Ssup).F ρ) : PLFA (FrourioFunctional.ofK Ent K gamma Ssup).F ρ

Connection between MinimizingMovement steps and PLFA curves in the limit. This shows that discrete MM curves converge to PLFA solutions as τ → 0. TODO: This requires standard MM convergence theory with compactness and Γ-convergence.

theorem Frourio.ofK_mm_energy_decrease {X : Type u_1} [PseudoMetricSpace X] [NormedAddCommGroup X] (Ent : X → ℝ) (K : KTransform X) (gamma Ssup τ : ℝ) (hτ : 0 < τ) (xPrev x : X) (h_step : MmStep τ (FrourioFunctional.ofK Ent K gamma Ssup).F xPrev x) : (FrourioFunctional.ofK Ent K gamma Ssup).F x ≤ (FrourioFunctional.ofK Ent K gamma Ssup).F xPrev

MinimizingMovement step preserves the energy decrease property for F.

Two-EVI with Force for Frourio Functional

This section provides aliases for TwoEVIWithForce and distance synchronization corollaries specialized for the Frourio functional F.

def Frourio.ofK_TwoEVIWithForce {X : Type u_1} [PseudoMetricSpace X] [NormedAddCommGroup X] (Ent : X → ℝ) (K : KTransform X) (gamma Ssup lamEff : ℝ) (u v : ℝ → X) : Prop

Two-EVI with force for the Frourio functional F.

Equations

• Frourio.ofK_TwoEVIWithForce Ent K gamma Ssup lamEff u v = Frourio.TwoEVIWithForce (Frourio.ofK_to_EVIProblem Ent K gamma Ssup lamEff) u v

def Frourio.ofK_TwoEVIWithForceShared {X : Type u_1} [PseudoMetricSpace X] [NormedAddCommGroup X] (Ent : X → ℝ) (K : KTransform X) (gamma Ssup lamEff : ℝ) (u v : ℝ → X) : Prop

Shared variant of Two-EVI with force for F using the geodesic predicate.

Equations

• Frourio.ofK_TwoEVIWithForceShared Ent K gamma Ssup lamEff u v = Frourio.TwoEVIWithForceShared (Frourio.ofK_to_EVIProblem Ent K gamma Ssup lamEff) u v

theorem Frourio.ofK_twoEVIShared_to_plain {X : Type u_1} [PseudoMetricSpace X] [NormedAddCommGroup X] (Ent : X → ℝ) (K : KTransform X) (gamma Ssup lamEff : ℝ) (u v : ℝ → X) : ofK_TwoEVIWithForceShared Ent K gamma Ssup lamEff u v → ofK_TwoEVIWithForce Ent K gamma Ssup lamEff u v

From shared to plain Two-EVI with force for F.

theorem Frourio.ofK_twoEVIWithForce_to_distance {X : Type u_1} [PseudoMetricSpace X] [NormedAddCommGroup X] (Ent : X → ℝ) (K : KTransform X) (gamma Ssup lamEff : ℝ) (u v : ℝ → X) (H : ofK_TwoEVIWithForce Ent K gamma Ssup lamEff u v) (Hbridge : ∀ (η : ℝ), HbridgeWithError (ofK_to_EVIProblem Ent K gamma Ssup lamEff) u v η) : ∃ (η : ℝ), (gronwall_exponential_contraction_with_error_half_pred lamEff η fun (t : ℝ) => d2 (u t) (v t)) → ContractionPropertyWithError (ofK_to_EVIProblem Ent K gamma Ssup lamEff) u v η

Distance synchronization from Two-EVI with force for F.

theorem Frourio.ofK_twoEVIWithForce_to_distance_concrete {X : Type u_1} [PseudoMetricSpace X] [NormedAddCommGroup X] (Ent : X → ℝ) (K : KTransform X) (gamma Ssup lamEff : ℝ) (u v : ℝ → X) (H : ofK_TwoEVIWithForce Ent K gamma Ssup lamEff u v) : ∃ (η : ℝ), (gronwall_exponential_contraction_with_error_half_pred lamEff η fun (t : ℝ) => d2 (u t) (v t)) → ContractionPropertyWithError (ofK_to_EVIProblem Ent K gamma Ssup lamEff) u v η

Concrete distance synchronization for F without external bridge hypothesis.

theorem Frourio.ofK_twoEVIWithForce_to_distance_concrete_closed {X : Type u_1} [PseudoMetricSpace X] [NormedAddCommGroup X] (Ent : X → ℝ) (K : KTransform X) (gamma Ssup lamEff : ℝ) (u v : ℝ → X) (H : ofK_TwoEVIWithForce Ent K gamma Ssup lamEff u v) (Hgr_all : ∀ (η : ℝ), gronwall_exponential_contraction_with_error_half_pred lamEff η fun (t : ℝ) => d2 (u t) (v t)) : ∃ (η : ℝ), ContractionPropertyWithError (ofK_to_EVIProblem Ent K gamma Ssup lamEff) u v η

Closed form: if Grönwall holds for all η, then Two-EVI with force for F yields distance synchronization.

theorem Frourio.ofK_twoEVIWithForceShared_to_distance {X : Type u_1} [PseudoMetricSpace X] [NormedAddCommGroup X] (Ent : X → ℝ) (K : KTransform X) (gamma Ssup lamEff : ℝ) (u v : ℝ → X) (H : ofK_TwoEVIWithForceShared Ent K gamma Ssup lamEff u v) (Hbridge : ∀ (η : ℝ), HbridgeWithError (ofK_to_EVIProblem Ent K gamma Ssup lamEff) u v η) : ∃ (η : ℝ), (gronwall_exponential_contraction_with_error_half_pred lamEff η fun (t : ℝ) => d2 (u t) (v t)) → ContractionPropertyWithError (ofK_to_EVIProblem Ent K gamma Ssup lamEff) u v η

Shared variant: distance synchronization from shared Two-EVI with force for F.

theorem Frourio.ofK_twoEVIWithForceShared_to_distance_concrete {X : Type u_1} [PseudoMetricSpace X] [NormedAddCommGroup X] (Ent : X → ℝ) (K : KTransform X) (gamma Ssup lamEff : ℝ) (u v : ℝ → X) (H : ofK_TwoEVIWithForceShared Ent K gamma Ssup lamEff u v) : ∃ (η : ℝ), (gronwall_exponential_contraction_with_error_half_pred lamEff η fun (t : ℝ) => d2 (u t) (v t)) → ContractionPropertyWithError (ofK_to_EVIProblem Ent K gamma Ssup lamEff) u v η

Shared variant: concrete distance synchronization for F.

theorem Frourio.ofK_twoEVIWithForceShared_to_distance_concrete_closed {X : Type u_1} [PseudoMetricSpace X] [NormedAddCommGroup X] (Ent : X → ℝ) (K : KTransform X) (gamma Ssup lamEff : ℝ) (u v : ℝ → X) (H : ofK_TwoEVIWithForceShared Ent K gamma Ssup lamEff u v) (Hgr_all : ∀ (η : ℝ), gronwall_exponential_contraction_with_error_half_pred lamEff η fun (t : ℝ) => d2 (u t) (v t)) : ∃ (η : ℝ), ContractionPropertyWithError (ofK_to_EVIProblem Ent K gamma Ssup lamEff) u v η

Shared variant: closed form distance synchronization for F.

Tensorization

This section provides thin wrappers for expressing existing minimization rules in terms of EVIProblem products. The tensorization allows us to handle multiple EVIProblems simultaneously and derive properties of their products.

IMPORTANT: The default product metric in Lean/Mathlib is the l∞ (max) metric, not the l2 (Euclidean) metric. The theorems below that assume additive decomposition of squared distances would require an explicit l2 product metric instance.

def Frourio.EVIProblemProduct {X : Type u_1} {Y : Type u_2} [PseudoMetricSpace X] [PseudoMetricSpace Y] (P₁ : EVIProblem X) (P₂ : EVIProblem Y) : EVIProblem (X × Y)

Product of two EVIProblems. The energy is the sum of component energies, and the parameter is the minimum of component parameters.

Equations

• P₁ ⊗ P₂ = { E := fun (p : X × Y) => P₁.E p.1 + P₂.E p.2, lam := min P₁.lam P₂.lam }

def Frourio.«term_⊗_» : Lean.TrailingParserDescr

Notation for EVIProblem product

Equations

• Frourio.«term_⊗_» = Lean.ParserDescr.trailingNode `Frourio.«term_⊗_» 70 70 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊗ ") (Lean.ParserDescr.cat `term 71))

theorem Frourio.isEVISolution_product_l2 {X : Type u_1} {Y : Type u_2} [PseudoMetricSpace X] [PseudoMetricSpace Y] (P₁ : EVIProblem X) (P₂ : EVIProblem Y) (u₁ : ℝ → X) (u₂ : ℝ → Y) (h₁ : IsEVISolution P₁ u₁) (h₂ : IsEVISolution P₂ u₂) (hl2 : ∀ (x x' : X) (y y' : Y), dist (x, y) (x', y') ^ 2 = dist x x' ^ 2 + dist y y' ^ 2) (hAdd : ∀ (v : X × Y) (t : ℝ), DiniUpper_add_le_pred (fun (τ : ℝ) => d2 (u₁ τ) v.1) (fun (τ : ℝ) => d2 (u₂ τ) v.2) t) : IsEVISolution (P₁ ⊗ P₂) fun (t : ℝ) => (u₁ t, u₂ t)

If both component curves are EVI solutions, their product is an EVI solution for the product problem (with the minimum lambda). NOTE: This requires an l2-type product metric where d²((x,y),(x',y')) = d²(x,x') + d²(y,y'). The default Lean product metric is l∞ (max), so this theorem needs a custom metric instance.

theorem Frourio.isEVISolution_product_fst {X : Type u_1} {Y : Type u_2} [PseudoMetricSpace X] [PseudoMetricSpace Y] (P₁ : EVIProblem X) (P₂ : EVIProblem Y) (u : ℝ → X × Y) (h : IsEVISolution (P₁ ⊗ P₂) u) (hlam : P₁.lam ≤ P₂.lam) (hDiniMono : ∀ (v : X) (w : Y) (t : ℝ), DiniUpper (fun (τ : ℝ) => d2 (u τ).1 v) t ≤ DiniUpper (fun (τ : ℝ) => d2 (u τ) (v, w)) t) (hd2_proj_eq : ∀ (x x' : X) (y : Y), d2 (x, y) (x', y) = d2 x x') : IsEVISolution P₁ fun (t : ℝ) => (u t).1

Projection: EVI solution for product implies EVI for first component when lambda matches. NOTE: This works with the default l∞ metric, but the relationship between product and component EVI is more complex than with l2 metric.

theorem Frourio.isEVISolution_product_snd {X : Type u_1} {Y : Type u_2} [PseudoMetricSpace X] [PseudoMetricSpace Y] (P₁ : EVIProblem X) (P₂ : EVIProblem Y) (u : ℝ → X × Y) (h : IsEVISolution (P₁ ⊗ P₂) u) (hlam : P₂.lam ≤ P₁.lam) (hDiniMono : ∀ (w : X) (v : Y) (t : ℝ), DiniUpper (fun (τ : ℝ) => d2 (u τ).2 v) t ≤ DiniUpper (fun (τ : ℝ) => d2 (u τ) (w, v)) t) (hd2_proj_eq : ∀ (x : X) (y y' : Y), d2 (x, y) (x, y') = d2 y y') : IsEVISolution P₂ fun (t : ℝ) => (u t).2

Projection: EVI solution for product implies EVI for second component when lambda matches.

def Frourio.EVIProblemTriple {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [PseudoMetricSpace X] [PseudoMetricSpace Y] [PseudoMetricSpace Z] (P₁ : EVIProblem X) (P₂ : EVIProblem Y) (P₃ : EVIProblem Z) : EVIProblem (X × Y × Z)

Triple product of EVIProblems

Equations

• Frourio.EVIProblemTriple P₁ P₂ P₃ = { E := fun (p : X × Y × Z) => P₁.E p.1 + P₂.E p.2.1 + P₃.E p.2.2, lam := min (min P₁.lam P₂.lam) P₃.lam }

theorem Frourio.product_has_minimizer {X : Type u_1} {Y : Type u_2} [PseudoMetricSpace X] [PseudoMetricSpace Y] [ProperSpace X] [ProperSpace Y] (P₁ : EVIProblem X) (P₂ : EVIProblem Y) (h₁ : ∃ (x₀ : X), ∀ (x : X), P₁.E x₀ ≤ P₁.E x) (h₂ : ∃ (y₀ : Y), ∀ (y : Y), P₂.E y₀ ≤ P₂.E y) : ∃ (p₀ : X × Y), (P₁ ⊗ P₂).E p₀ = sInf (Set.range (P₁ ⊗ P₂).E)

Minimization rule for product: if each component has a minimizer, the product has a minimizer (assuming proper/coercive energies and lower semicontinuity).

theorem Frourio.product_energy_decrease {X : Type u_1} {Y : Type u_2} [PseudoMetricSpace X] [PseudoMetricSpace Y] (P₁ : EVIProblem X) (P₂ : EVIProblem Y) (x x' : X) (y y' : Y) (h₁ : P₁.E x' ≤ P₁.E x) (h₂ : P₂.E y' ≤ P₂.E y) : (P₁ ⊗ P₂).E (x', y') ≤ (P₁ ⊗ P₂).E (x, y)

Energy decrease for product: if both components decrease energy, the product decreases energy.

noncomputable def Frourio.ofK_as_EVIProblem {X : Type u_1} [PseudoMetricSpace X] (Ent : X → ℝ) (K : KTransform X) (gamma Ssup lamEff : ℝ) : EVIProblem X

Frourio functional as an EVIProblem. This wraps F = Ent + γ·Dσm as a single EVIProblem with effective lambda. NOTE: Despite the name, this is not actually a product structure.

Equations

• Frourio.ofK_as_EVIProblem Ent K gamma Ssup lamEff = { E := (Frourio.FrourioFunctional.ofK Ent K gamma Ssup).F, lam := lamEff }

noncomputable def Frourio.ofK_decomposed_pair {X : Type u_1} [PseudoMetricSpace X] (Ent : X → ℝ) (K : KTransform X) (gamma Ssup lamEnt lamD : ℝ) : EVIProblem X × EVIProblem X

Decomposed representation: separate EVIProblems for Ent and Dσm components. This returns a pair of problems, not a product EVIProblem on X×X.

Equations

• Frourio.ofK_decomposed_pair Ent K gamma Ssup lamEnt lamD = ({ E := Ent, lam := lamEnt }, { E := fun (x : X) => gamma * Frourio.DsigmamFromK K Ssup x, lam := lamD })

theorem Frourio.ofK_EVIProblem_equivalence {X : Type u_1} [PseudoMetricSpace X] [NormedAddCommGroup X] (Ent : X → ℝ) (K : KTransform X) (gamma Ssup lamEff : ℝ) (u : ℝ → X) (h : ofK_IsEVISolution Ent K gamma Ssup lamEff u) : IsEVISolution (ofK_as_EVIProblem Ent K gamma Ssup lamEff) u

When F satisfies EVI with λ_eff, it satisfies the EVIProblem formulation.

def Frourio.EVIProblemPower {X : Type u_1} [PseudoMetricSpace X] (P : EVIProblem X) (n : ℕ) : EVIProblem (Fin n → X)

N-fold product for homogeneous systems

Equations

• Frourio.EVIProblemPower P n = { E := fun (x : Fin n → X) => ∑ i : Fin n, P.E (x i), lam := P.lam }

theorem Frourio.isEVISolution_power_l2 {X : Type u_1} [PseudoMetricSpace X] (P : EVIProblem X) (n : ℕ) (u : Fin n → ℝ → X) (h : ∀ (i : Fin n), IsEVISolution P (u i)) (hl2 : ∀ (f g : Fin n → X), dist f g ^ 2 = ∑ i : Fin n, dist (f i) (g i) ^ 2) (hAdd : ∀ (v : Fin n → X) (t : ℝ), DiniUpper (fun (τ : ℝ) => d2 (fun (i : Fin n) => u i τ) v) t ≤ ∑ i : Fin n, DiniUpper (fun (τ : ℝ) => d2 (u i τ) (v i)) t) : IsEVISolution (EVIProblemPower P n) fun (t : ℝ) (i : Fin n) => u i t

Homogeneous product: N identical EVI solutions yield product solution. NOTE: This assumes an l2-type metric on Fin n → X where distances decompose additively. The default product metric is l∞, which requires different treatment.

theorem Frourio.isEVISolution_synchronized_l2 {X : Type u_1} [PseudoMetricSpace X] (P : EVIProblem X) (n : ℕ) (u : ℝ → X) (h : IsEVISolution P u) (hl2 : ∀ (f g : Fin n → X), dist f g ^ 2 = ∑ i : Fin n, dist (f i) (g i) ^ 2) (hAdd : ∀ (v : Fin n → X) (t : ℝ), DiniUpper (fun (τ : ℝ) => d2 (fun (_i : Fin n) => u τ) v) t ≤ ∑ i : Fin n, DiniUpper (fun (τ : ℝ) => d2 (u τ) (v i)) t) : IsEVISolution (EVIProblemPower P n) fun (t : ℝ) (x : Fin n) => u t

Synchronized product: when all components evolve with the same curve. NOTE: This requires the same l2-type metric assumption as isEVISolution_power_l2.

Multi-scale Exponential Laws

This section provides wrappers for λ_eff under multi-scale transformations following the scaling laws from FG (Frourio Geometry) framework as described.

The effective lambda under scaling transformation is: λ_eff = Λ^((κ - 2α)k) · λ where:

• Λ > 1 is the metal ratio (scaling factor)
• k ∈ ℤ is the scale level
• κ > 0 is the generator homogeneity exponent
• α ≥ 0 is the metric scaling exponent (0 for isometry, >0 for similarity)

structure Frourio.ScalingParams : Type

Scaling parameters for multi-scale analysis

• Lambda : ℝ
• kappa : ℝ
• alpha : ℝ
• hLambda : 1 < self.Lambda
• hkappa : 0 < self.kappa
• halpha : 0 ≤ self.alpha

noncomputable def Frourio.lambdaEffScaled (params : ScalingParams) (lam : ℝ) (k : ℤ) : ℝ

Compute the effective lambda at scale level k under scaling transformation. Formula: λ_eff = Λ^((κ - 2α)k) · λ

Equations

• Frourio.lambdaEffScaled params lam k = params.Lambda.rpow ((params.kappa - 2 * params.alpha) * ↑k) * lam

noncomputable def Frourio.lambdaScalingFactor (params : ScalingParams) (k : ℤ) : ℝ

The exponential scaling factor for lambda

Equations

• Frourio.lambdaScalingFactor params k = params.Lambda.rpow ((params.kappa - 2 * params.alpha) * ↑k)

theorem Frourio.lambdaEffScaled_monotone_increasing {params : ScalingParams} (k : ℤ) (lam : ℝ) (hlam : 0 < lam) (hscale_gt : 1 < params.Lambda.rpow ((params.kappa - 2 * params.alpha) * ↑k)) : lam < lambdaEffScaled params lam k

Monotonicity of scaled lambda: if κ > 2α and k > 0, then λ_eff > λ

theorem Frourio.lambdaEffScaled_invariant {params : ScalingParams} (hbalance : params.kappa = 2 * params.alpha) (lam : ℝ) (k : ℤ) : lambdaEffScaled params lam k = lam

When κ = 2α (critical balance), the effective lambda is scale-invariant

theorem Frourio.lambdaEffScaled_monotone_decreasing {params : ScalingParams} (k : ℤ) (lam : ℝ) (hlam : 0 < lam) (hscale_lt : params.Lambda.rpow ((params.kappa - 2 * params.alpha) * ↑k) < 1) : lambdaEffScaled params lam k < lam

When κ < 2α and k > 0, the effective lambda decreases

def Frourio.isometricScalingParams (Lambda kappa : ℝ) (hLambda : 1 < Lambda) (hkappa : 0 < kappa) : ScalingParams

Special case: isometric scaling (α = 0)

Equations

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

theorem Frourio.lambdaEffScaled_isometric (Lambda kappa : ℝ) (hLambda : 1 < Lambda) (hkappa : 0 < kappa) (lam : ℝ) (k : ℤ) : lambdaEffScaled (isometricScalingParams Lambda kappa hLambda hkappa) lam k = Lambda ^ (kappa * ↑k) * lam

For isometric scaling, λ_eff = Λ^(κk) · λ

def Frourio.euclideanScalingParams (Lambda kappa : ℝ) (hLambda : 1 < Lambda) (hkappa : 0 < kappa) : ScalingParams

Special case: Euclidean similarity (α = 1)

Equations

• Frourio.euclideanScalingParams Lambda kappa hLambda hkappa = { Lambda := Lambda, kappa := kappa, alpha := 1, hLambda := hLambda, hkappa := hkappa, halpha := ⋯ }

theorem Frourio.lambdaEffScaled_euclidean (Lambda kappa : ℝ) (hLambda : 1 < Lambda) (hkappa : 0 < kappa) (lam : ℝ) (k : ℤ) : lambdaEffScaled (euclideanScalingParams Lambda kappa hLambda hkappa) lam k = Lambda ^ ((kappa - 2) * ↑k) * lam

For Euclidean similarity, λ_eff = Λ^((κ-2)k) · λ

noncomputable def Frourio.goldenRatio : ℝ

Golden ratio as a special metal ratio

Equations

• Frourio.goldenRatio = (1 + √5) / 2

theorem Frourio.goldenRatio_gt_one : 1 < goldenRatio

The golden ratio is greater than 1

noncomputable def Frourio.goldenScalingParams (kappa alpha : ℝ) (hkappa : 0 < kappa) (halpha : 0 ≤ alpha) : ScalingParams

Scaling parameters with golden ratio

Equations

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

def Frourio.ofK_IsEVISolution_scaled {X : Type u_1} [PseudoMetricSpace X] [NormedAddCommGroup X] (Ent : X → ℝ) (K : KTransform X) (gamma Ssup lam : ℝ) (params : ScalingParams) (k : ℤ) (u : ℝ → X) : Prop

Multi-scale EVI predicate for Frourio functional under scaling

Equations

• Frourio.ofK_IsEVISolution_scaled Ent K gamma Ssup lam params k u = Frourio.ofK_IsEVISolution Ent K gamma Ssup (Frourio.lambdaEffScaled params lam k) u

theorem Frourio.exists_scaled_solution {X : Type u_1} [PseudoMetricSpace X] [NormedAddCommGroup X] (Ent : X → ℝ) (K : KTransform X) (gamma Ssup lam : ℝ) (params : ScalingParams) (k : ℤ) (hscale : ∃ (v : ℝ → X), ofK_IsEVISolution Ent K gamma Ssup (lambdaEffScaled params lam k) v) : ∃ (v : ℝ → X), ofK_IsEVISolution_scaled Ent K gamma Ssup lam params k v

Existence of scaled solution with adjusted lambda

theorem Frourio.lambdaEffScaled_composition (params : ScalingParams) (lam : ℝ) (k₁ k₂ : ℤ) (hrpow_add : ∀ (x y : ℝ), params.Lambda.rpow (x + y) = params.Lambda.rpow x * params.Lambda.rpow y) : lambdaEffScaled params (lambdaEffScaled params lam k₁) k₂ = lambdaEffScaled params lam (k₁ + k₂)

Composition of scaling at different levels

theorem Frourio.lambdaEffScaled_inverse (params : ScalingParams) (lam : ℝ) (k : ℤ) (hrpow_add : ∀ (x y : ℝ), params.Lambda.rpow (x + y) = params.Lambda.rpow x * params.Lambda.rpow y) : lambdaEffScaled params (lambdaEffScaled params lam k) (-k) = lam

Inverse scaling