theorem Frourio.golden_ratio_property : φ ^ 2 = φ + 1

黄金比の基本性質

theorem Frourio.phi_pos : 0 < φ

黄金比は正

theorem Frourio.phi_inv : φ⁻¹ = φ - 1

黄金比の逆数：φ⁻¹ = φ - 1

theorem Frourio.S_phi_two : S φ 2 = 2 * φ - 1

具体例：S_2(φ) = φ

noncomputable def Frourio.goldenMellinSymbol (s : ℂ) : ℂ

黄金Frourio作用素のMellin記号

Equations

• Frourio.goldenMellinSymbol s = Frourio.mellinSymbol Frourio.GoldenFrourioOperator s

noncomputable def Frourio.ThreePointExample (δ : ℝ) (hδ : 0 < δ) : FrourioOperator 3

3点Frourio作用素の例

Equations

• Frourio.ThreePointExample δ hδ = { α := fun (x : Fin 3) => 1, χ := fun (x : Fin 3) => Frourio.Sign.pos, Λ := fun (i : Fin 3) => δ ^ (↑i + 1), Λ_pos := ⋯ }

Basic 1D example: from an initial value to JKO, then to EDE and EVI. We take X := ℝ, the energy F := fun _ => 0, and λ_eff := 0.

noncomputable def FrourioExamples.F : ℝ → ℝ

Equations

• FrourioExamples.F x✝ = 0

noncomputable def FrourioExamples.lamEff : ℝ

Equations

• FrourioExamples.lamEff = 0

noncomputable def FrourioExamples.rho (ρ0 : ℝ) : ℝ → ℝ

Equations

• FrourioExamples.rho ρ0 _t = ρ0

theorem FrourioExamples.basic1D_JKO (ρ0 : ℝ) : Frourio.JKO F ρ0

JKO witness: the constant curve at ρ0.

theorem FrourioExamples.basic1D_EDE (ρ0 : ℝ) : Frourio.EDE F (rho ρ0)

EDE holds for the constant curve and constant energy.

theorem FrourioExamples.basic1D_EVI (ρ0 : ℝ) : Frourio.IsEVISolution { E := F, lam := lamEff } (rho ρ0)

EVI holds for the constant curve when λ_eff = 0.

theorem FrourioExamples.basic1D_chain (ρ0 : ℝ) : ∃ (ρ : ℝ → ℝ), ρ 0 = ρ0 ∧ Frourio.JKO F ρ0 ∧ Frourio.EDE F ρ ∧ Frourio.IsEVISolution { E := F, lam := lamEff } ρ

Integrated existence: from ρ0, there exists a curve realizing JKO, EDE, EVI.

Quadratic energy example on ℝ: closed‑form MM step and a chain to EVI via a package equivalence. This showcases the MM functional with F(x) = (1/2) x^2.

noncomputable def FrourioExamplesQuadratic.Fq : ℝ → ℝ

Quadratic energy F(x) = (1/2) x^2.

Equations

• FrourioExamplesQuadratic.Fq x = 1 / 2 * x ^ 2

theorem FrourioExamplesQuadratic.quadratic_mm_step_closed_form (τ xPrev : ℝ) (hτ : 0 < τ) : Frourio.MmStep τ Fq xPrev (xPrev / (1 + τ))

Closed‑form MM minimizer for the quadratic energy on ℝ: x* = xPrev / (1 + τ) minimizes F(x) + (1/(2τ))‖x − xPrev‖^2 when τ > 0.

theorem FrourioExamplesQuadratic.quadratic_JKO (x0 : ℝ) : Frourio.JKO Fq x0

Trivial JKO witness for the quadratic energy: the constant curve.

theorem FrourioExamplesQuadratic.chain_quadratic_to_EVI (lamEff : ℝ) (G : Frourio.plfaEdeEviJko_equiv Fq lamEff) (x0 : ℝ) : ∃ (ρ : ℝ → ℝ), ρ 0 = x0 ∧ Frourio.IsEVISolution { E := Fq, lam := lamEff } ρ

With a packaged PLFA = EDE = EVI = JKO equivalence for Fq, a JKO initializer produces an EVI solution (example chain).

FG8-style examples: demonstrate how to apply the integrated suite, effective-λ lower bound, and two‑EVI with force wrappers added in FGTheorems. These are statement-level demos parameterized by the corresponding assumptions.

theorem FrourioExamplesFG8.demo_flow_suite_real_auto {X : Type u_1} [PseudoMetricSpace X] [MeasurableSpace X] (S : Frourio.GradientFlowSystem X) (flags : Frourio.AnalyticFlagsReal X S.func.F (Frourio.lambdaBE S.base.lam S.eps)) (h_usc : ∀ (ρ : ℝ → X), Frourio.ShiftedUSCHypothesis S.func.F ρ) (HedeEvi_builder : Frourio.EDE_EVI_from_analytic_flags S.func.F (Frourio.lambdaBE S.base.lam S.eps)) (hLam : Frourio.lambdaEffLowerBound S.func S.budget S.base.lam S.eps (Frourio.lambdaBE S.base.lam S.eps) S.Ssup S.XiNorm) (Htwo : ∀ (u v : ℝ → X), Frourio.TwoEVIWithForce { E := S.func.F, lam := S.base.lam } u v) : Frourio.gradient_flow_equiv S ∧ Frourio.lambda_eff_lower_bound S ∧ Frourio.two_evi_with_force S

Demo: Run the integrated gradient-flow suite via the real-route auto wrapper. Supply real analytic flags for F := Ent + γ·Dσm, an EDE⇔EVI builder on analytic flags, an effective-λ lower-bound witness, and a two‑EVI with force hypothesis.

theorem FrourioExamplesFG8.demo_lambda_eff_from_doob {X : Type u_1} [PseudoMetricSpace X] [MeasurableSpace X] (S : Frourio.GradientFlowSystem X) : Frourio.lambda_eff_lower S

Demo: Construct λ_eff lower bound from Doob+m‑point hypotheses using the FG-level convenience wrapper.

theorem FrourioExamplesFG8.demo_twoEVI_concrete {X : Type u_1} [PseudoMetricSpace X] [MeasurableSpace X] (S : Frourio.GradientFlowSystem X) (Htwo : Frourio.two_evi_with_force S) (u v : ℝ → X) : ∃ (η : ℝ), (Frourio.gronwall_exponential_contraction_with_error_half_pred S.base.lam η fun (t : ℝ) => Frourio.d2 (u t) (v t)) → Frourio.ContractionPropertyWithError { E := S.func.F, lam := S.base.lam } u v η

Demo: From two_evi_with_force S, obtain a distance synchronization with error for any pair of curves u, v via the concrete Grönwall route.

theorem FrourioExamplesFG8.demo_twoEVI_concrete_closed {X : Type u_1} [PseudoMetricSpace X] [MeasurableSpace X] (S : Frourio.GradientFlowSystem X) (Htwo : Frourio.two_evi_with_force S) (u v : ℝ → X) (Hgr_all : ∀ (η : ℝ), Frourio.gronwall_exponential_contraction_with_error_half_pred S.base.lam η fun (t : ℝ) => Frourio.d2 (u t) (v t)) : ∃ (η : ℝ), Frourio.ContractionPropertyWithError { E := S.func.F, lam := S.base.lam } u v η

Demo (closed form): if the Grönwall predicate holds for all η, then obtain an error parameter with a distance synchronization bound.