Gradient-Flow Framework: statements and data glue

This module bundles FG core data with the functional layer and exposes statement-level predicates for the FG8 equivalences and bounds: PLFA = EDE = EVI = JKO, effective lambda lower bounds, two-EVI with force, tensorization (min rule placeholder), and a multi-scale effective lambda.

The goal here is to fix API shapes that connect existing components; heavy analytic proofs will be added in later phases.

structure Frourio.GradientFlowSystem (X : Type u_2) [PseudoMetricSpace X] [MeasurableSpace X] : Type u_2

FG8 data pack: core FG data, a functional with coupling, external budget constants and parameters controlling Doob degradation and symbol sizes.

• base : FGData X
• func : FrourioFunctional X
• Ssup : ℝ
• XiNorm : ℝ
• budget : ConstantBudget
• eps : ℝ

def Frourio.gradient_flow_equiv {X : Type u_1} [PseudoMetricSpace X] [MeasurableSpace X] (S : GradientFlowSystem X) : Prop

Equivalence packaging (PLFA = EDE = EVI = JKO) at statement level using the functional F = Ent + γ·Dσm and effective parameter λ_BE = λ - 2ε.

Equations

• Frourio.gradient_flow_equiv S = Frourio.plfaEdeEviJko_equiv S.func.F (Frourio.lambdaBE S.base.lam S.eps)

theorem Frourio.gradient_flow_equiv_of_pack {X : Type u_1} [PseudoMetricSpace X] [MeasurableSpace X] (S : GradientFlowSystem X) (G : plfaEdeEviJko_equiv S.func.F (lambdaBE S.base.lam S.eps)) : gradient_flow_equiv S

Equivalence theorem (wrapper): if the packaged equivalence holds for F := Ent + γ·Dσm and λ_BE := λ - 2ε, then the gradient-flow equivalence holds.

def Frourio.lambda_eff_lower_bound {X : Type u_1} [PseudoMetricSpace X] [MeasurableSpace X] (S : GradientFlowSystem X) : Prop

Effective lambda lower bound statement: there exists λ_eff satisfying the budgeted inequality with Doob-corrected parameter.

Equations

• Frourio.lambda_eff_lower_bound S = ∃ (lamEff : ℝ), Frourio.lambdaEffLowerBound S.func S.budget S.base.lam S.eps lamEff S.Ssup S.XiNorm

theorem Frourio.lambda_eff_lower_bound_of {X : Type u_1} [PseudoMetricSpace X] [MeasurableSpace X] (S : GradientFlowSystem X) {lamEff : ℝ} (h : lambdaEffLowerBound S.func S.budget S.base.lam S.eps lamEff S.Ssup S.XiNorm) : lambda_eff_lower_bound S

Lower bound theorem (wrapper): a provided inequality instantiates the lambda_eff_lower_bound statement.

theorem Frourio.lambda_eff_lower_bound_strengthen_with_flags {X : Type u_1} [PseudoMetricSpace X] [MeasurableSpace X] (S : GradientFlowSystem X) (flags : AnalyticFlagsReal X S.func.F (lambdaBE S.base.lam S.eps)) (h : lambda_eff_lower_bound S) : ∃ (lamEff' : ℝ), lambdaEffLowerBound S.func S.budget S.base.lam S.eps lamEff' S.Ssup S.XiNorm ∧ lamEff' ≥ lamLowerFromRealFlags flags

Strengthen a provided lambda_eff_lower_bound using the explicit lower bound encoded in real analytic flags by choosing lamEff' = max(lamEff, L_flags).

theorem Frourio.lambda_eff_lower_bound_from_doob {X : Type u_1} [PseudoMetricSpace X] [MeasurableSpace X] (S : GradientFlowSystem X) : lambda_eff_lower_bound S

Effective lambda lower bound derived from Doob assumptions and m-point zero-order bounds. Uses the constructive inequality from the analysis layer.

def Frourio.two_evi_with_force {X : Type u_1} [PseudoMetricSpace X] [MeasurableSpace X] (S : GradientFlowSystem X) : Prop

Two-EVI with external forcing: packaged via the analysis-layer predicate.

Equations

• Frourio.two_evi_with_force S = ∀ (u v : ℝ → X), Frourio.TwoEVIWithForce { E := S.func.F, lam := S.base.lam } u v

theorem Frourio.two_evi_with_force_of {X : Type u_1} [PseudoMetricSpace X] [MeasurableSpace X] (S : GradientFlowSystem X) (H : ∀ (u v : ℝ → X), TwoEVIWithForce { E := S.func.F, lam := S.base.lam } u v) : two_evi_with_force S

two-EVI with force theorem (wrapper): pass through an analysis-layer result.

theorem Frourio.gradient_flow_suite {X : Type u_1} [PseudoMetricSpace X] [MeasurableSpace X] (S : GradientFlowSystem X) (G : plfaEdeEviJko_equiv S.func.F (lambdaBE S.base.lam S.eps)) (lamEff : ℝ) (hLam : lambdaEffLowerBound S.func S.budget S.base.lam S.eps lamEff S.Ssup S.XiNorm) (Htwo : ∀ (u v : ℝ → X), TwoEVIWithForce { E := S.func.F, lam := S.base.lam } u v) : gradient_flow_equiv S ∧ lambda_eff_lower_bound S ∧ two_evi_with_force S

Integrated gradient-flow suite: bundles the equivalence package, the lambda_eff lower bound, and the two-EVI with force into a single statement.

theorem Frourio.gradient_flow_suite_from_flags_and_ede_evi_pack {X : Type u_1} [PseudoMetricSpace X] [MeasurableSpace X] (S : GradientFlowSystem X) (A : AnalyticFlags S.func.F (lambdaBE S.base.lam S.eps)) (HplfaEde : PLFA_EDE_from_analytic_flags S.func.F (lambdaBE S.base.lam S.eps)) (P : EDEEVIAssumptions S.func.F (lambdaBE S.base.lam S.eps)) (HjkoPlfa : JKO_PLFA_from_analytic_flags S.func.F) (lamEff : ℝ) (hLam : lambdaEffLowerBound S.func S.budget S.base.lam S.eps lamEff S.Ssup S.XiNorm) (Htwo : ∀ (u v : ℝ → X), TwoEVIWithForce { E := S.func.F, lam := S.base.lam } u v) : gradient_flow_equiv S ∧ lambda_eff_lower_bound S ∧ two_evi_with_force S

Proof-backed variant: build the equivalence package from analytic flags and an EDEEVIAssumptions pack (EDE ⇔ EVI), then assemble the integrated suite.

def Frourio.tensorization_min_rule {X : Type u_1} {Y : Type u_2} [PseudoMetricSpace X] [MeasurableSpace X] [PseudoMetricSpace Y] [MeasurableSpace Y] (S₁ : GradientFlowSystem X) (S₂ : GradientFlowSystem Y) : Prop

Minimal tensorization predicate: requires coercivity surrogates and nonnegative coupling for both factors.

Equations

• Frourio.tensorization_min_rule S₁ S₂ = (Frourio.K1prime S₁.func ∧ Frourio.K1prime S₂.func ∧ 0 ≤ S₁.func.gamma ∧ 0 ≤ S₂.func.gamma)

noncomputable def Frourio.effective_lambda_multiscale {m : ℕ} (α κ Λ : Fin m → ℝ) (k : Fin m → ℤ) (lam : ℝ) : ℝ

Multi-scale effective lambda helper: product of single-scale factors over j : Fin m.

Equations

• Frourio.effective_lambda_multiscale α κ Λ k lam = lam * ∏ j : Fin m, Real.exp ((κ j - 2 * α j) * ↑(k j) * Real.log (Λ j))

@[reducible, inline]

noncomputable abbrev Frourio.effectiveLambdaVec {m : ℕ} (α κ Λ : Fin m → ℝ) (k : Fin m → ℤ) (lam : ℝ) : ℝ

Alias used in the design notes.

Equations

• Frourio.effectiveLambdaVec α κ Λ k lam = Frourio.effective_lambda_multiscale α κ Λ k lam

def Frourio.multiscale_lambda_rule {m : ℕ} (Λ α κ : Fin m → ℝ) (k : Fin m → ℤ) : Prop

Multi-scale rule statement: for any base parameter λ, there exists an effective parameter obtained by the product formula.

Equations

• Frourio.multiscale_lambda_rule Λ α κ k = ∀ (lam : ℝ), ∃ (lamEff : ℝ), lamEff = Frourio.effective_lambda_multiscale α κ Λ k lam

theorem Frourio.multiscale_lambda_rule_thm {m : ℕ} (Λ α κ : Fin m → ℝ) (k : Fin m → ℤ) : multiscale_lambda_rule Λ α κ k

Trivial constructor for the multiscale effective-λ rule: choose the right-hand side as the witness.

theorem Frourio.effective_lambda_multiscale_rpow {m : ℕ} (α κ Λ : Fin m → ℝ) (k : Fin m → ℤ) (lam : ℝ) (hΛ : ∀ (j : Fin m), 0 < Λ j) : effective_lambda_multiscale α κ Λ k lam = lam * ∏ j : Fin m, (Λ j).rpow ((κ j - 2 * α j) * ↑(k j))

Arithmetic form: multiscale effective λ as a product of real powers when each Λ j > 0.