Core part of PLFA/EDE/JKO: definitions and non-metric theorems. This file avoids placing a [PseudoMetricSpace X] instance in scope, so section-variable linter warnings are minimized.

def Frourio.PLFA {X : Type u_1} (F : X → ℝ) (ρ : ℝ → X) : Prop

Equations

• Frourio.PLFA F ρ = ∀ ⦃s t : ℝ⦄, s ≤ t → F (ρ t) ≤ F (ρ s)

def Frourio.Action {X : Type u_1} (F : X → ℝ) (ρ : ℝ → X) : Prop

Equations

• Frourio.Action F ρ = Frourio.PLFA F ρ

def Frourio.EDE {X : Type u_1} (F : X → ℝ) (ρ : ℝ → X) : Prop

Equations

• Frourio.EDE F ρ = ∀ (t : ℝ), Frourio.DiniUpperE (fun (τ : ℝ) => F (ρ τ)) t ≤ 0

def Frourio.JKO {X : Type u_1} (F : X → ℝ) (ρ0 : X) : Prop

Equations

• Frourio.JKO F ρ0 = ∃ (ρ : ℝ → X), ρ 0 = ρ0 ∧ ∀ (t : ℝ), F (ρ t) ≤ F ρ0

def Frourio.HalfConvex {X : Type u_1} (F : X → ℝ) (_lamEff : ℝ) : Prop

Equations

• Frourio.HalfConvex F _lamEff = ∃ (c : ℝ), 0 ≤ c ∧ ∀ (x : X), F x ≤ F x + c

def Frourio.StrongUpperBound {X : Type u_1} (F : X → ℝ) : Prop

Equations

• Frourio.StrongUpperBound F = ∃ (c : ℝ), 0 ≤ c ∧ ∀ (x : X), F x ≤ F x + c

def Frourio.Proper {X : Type u_1} (F : X → ℝ) : Prop

Equations

• Frourio.Proper F = ∃ (C : ℝ), ∀ (x : X), F x ≥ F x - C

def Frourio.LowerSemicontinuous {X : Type u_1} (F : X → ℝ) : Prop

Equations

• Frourio.LowerSemicontinuous F = ∀ (x : X), ∃ (c : ℝ), 0 ≤ c ∧ F x ≤ F x + c

def Frourio.Coercive {X : Type u_1} (F : X → ℝ) : Prop

Equations

• Frourio.Coercive F = ∀ (x : X), ∃ (c : ℝ), 0 ≤ c ∧ F x ≥ F x - c

def Frourio.JKOStable {X : Type u_1} (F : X → ℝ) : Prop

Equations

• Frourio.JKOStable F = ∀ (ρ0 : X), Frourio.JKO F ρ0

def Frourio.PLFA_EDE_pred {X : Type u_1} (F : X → ℝ) : Prop

Equations

• Frourio.PLFA_EDE_pred F = ∀ (ρ : ℝ → X), Frourio.PLFA F ρ ↔ Frourio.EDE F ρ

def Frourio.JKO_to_PLFA_pred {X : Type u_1} (F : X → ℝ) : Prop

Equations

• Frourio.JKO_to_PLFA_pred F = ∀ (ρ0 : X), Frourio.JKO F ρ0 → ∃ (ρ : ℝ → X), ρ 0 = ρ0 ∧ Frourio.PLFA F ρ

theorem Frourio.plfa_implies_ede {X : Type u_1} (F : X → ℝ) (ρ : ℝ → X) (h : PLFA F ρ) : EDE F ρ

def Frourio.EDE_to_PLFA_bridge {X : Type u_1} (F : X → ℝ) : Prop

Equations

• Frourio.EDE_to_PLFA_bridge F = ∀ (ρ : ℝ → X), Frourio.EDE F ρ → Frourio.PLFA F ρ

theorem Frourio.plfa_ede_equiv_from_bridge {X : Type u_1} (F : X → ℝ) (HB : EDE_to_PLFA_bridge F) : PLFA_EDE_pred F

structure Frourio.PLFAEDEAssumptions {X : Type u_1} (F : X → ℝ) : Prop

• plfa_iff_ede (ρ : ℝ → X) : PLFA F ρ ↔ EDE F ρ

structure Frourio.JKOPLFAAssumptions {X : Type u_1} (F : X → ℝ) : Prop

• jko_to_plfa (ρ0 : X) : JKO F ρ0 → ∃ (ρ : ℝ → X), ρ 0 = ρ0 ∧ PLFA F ρ

theorem Frourio.plfa_ede_from_pack {X : Type u_1} (F : X → ℝ) (H : PLFAEDEAssumptions F) : PLFA_EDE_pred F

theorem Frourio.jko_plfa_from_pack {X : Type u_1} (F : X → ℝ) (H : JKOPLFAAssumptions F) : JKO_to_PLFA_pred F

def Frourio.PLFA_EDE_from_analytic_flags {X : Type u_1} (F : X → ℝ) (lamEff : ℝ) : Prop

Equations

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

def Frourio.JKO_PLFA_from_analytic_flags {X : Type u_1} (F : X → ℝ) : Prop

Equations

• Frourio.JKO_PLFA_from_analytic_flags F = (Frourio.Proper F ∧ Frourio.LowerSemicontinuous F ∧ Frourio.Coercive F ∧ Frourio.JKOStable F → Frourio.JKO_to_PLFA_pred F)

theorem Frourio.plfa_ede_bridge_from_pack {X : Type u_1} (F : X → ℝ) (lamEff : ℝ) (H : PLFAEDEAssumptions F) : PLFA_EDE_from_analytic_flags F lamEff

theorem Frourio.jko_plfa_bridge_from_pack {X : Type u_1} (F : X → ℝ) (_lamEff : ℝ) (H : JKOPLFAAssumptions F) : JKO_PLFA_from_analytic_flags F

theorem Frourio.action_iff_plfa {X : Type u_1} (F : X → ℝ) (ρ : ℝ → X) : Action F ρ ↔ PLFA F ρ

structure Frourio.AnalyticFlags {X : Type u_1} (F : X → ℝ) (lamEff : ℝ) : Prop

• proper : Proper F
• lsc : LowerSemicontinuous F
• coercive : Coercive F
• HC : HalfConvex F lamEff
• SUB : StrongUpperBound F
• jkoStable : JKOStable F

theorem Frourio.EDE_shift {X : Type u_1} (F : X → ℝ) (ρ : ℝ → X) (hEDE : EDE F ρ) (s t : ℝ) : DiniUpperE (fun (τ : ℝ) => F (ρ (s + τ))) t ≤ 0

theorem Frourio.EDE_forwardDiff_nonpos {X : Type u_1} (F : X → ℝ) (ρ : ℝ → X) (hEDE : EDE F ρ) (s t : ℝ) : DiniUpperE (fun (τ : ℝ) => F (ρ (s + τ)) - F (ρ s)) t ≤ 0

theorem Frourio.ede_to_plfa_with_gronwall_zero {X : Type u_1} (F : X → ℝ) (ρ : ℝ → X) (hEDE : EDE F ρ) (G0 : ∀ (s : ℝ), (∀ (t : ℝ), DiniUpperE (fun (τ : ℝ) => F (ρ (s + τ)) - F (ρ s)) t ≤ 0) → ∀ (t : ℝ), 0 ≤ t → F (ρ (s + t)) - F (ρ s) ≤ F (ρ (s + 0)) - F (ρ s)) : PLFA F ρ

theorem Frourio.G0_from_DiniUpper_nonpos {X : Type u_1} (F : X → ℝ) (ρ : ℝ → X) (h_usc_F : ∀ (s s' t' : ℝ), s' < t' → ∀ w ∈ Set.Icc 0 (t' - s'), ∀ y₀ ∈ Set.Icc 0 (t' - s'), |y₀ - w| < (t' - s') / 4 → upper_semicontinuous_at_zero (fun (τ : ℝ) => F (ρ (s + τ)) - F (ρ s)) s' y₀) (s : ℝ) : (∀ (t : ℝ), DiniUpperE (fun (τ : ℝ) => F (ρ (s + τ)) - F (ρ s)) t ≤ 0) → ∀ (t : ℝ), 0 ≤ t → F (ρ (s + t)) - F (ρ s) ≤ F (ρ (s + 0)) - F (ρ s)

Helper: Provides the G0 condition for Gronwall (nonnegative times). Now requires upper semicontinuity hypothesis for the shifted function.

theorem Frourio.plfa_ede_equiv_from_flags {X : Type u_1} (F : X → ℝ) (lamEff : ℝ) (hP : Proper F) (hL : LowerSemicontinuous F) (hC : Coercive F) (HC : HalfConvex F lamEff) (SUB : StrongUpperBound F) (H : PLFA_EDE_from_analytic_flags F lamEff) (ρ : ℝ → X) : PLFA F ρ ↔ EDE F ρ

theorem Frourio.build_PLFAEDE_pack_from_flags {X : Type u_1} (F : X → ℝ) (lamEff : ℝ) (hP : Proper F) (hL : LowerSemicontinuous F) (hC : Coercive F) (HC : HalfConvex F lamEff) (SUB : StrongUpperBound F) (H : PLFA_EDE_from_analytic_flags F lamEff) : PLFAEDEAssumptions F

def Frourio.JKO_to_EDE_pred {X : Type u_1} (F : X → ℝ) : Prop

Predicate: from a JKO initializer, produce an EDE evolution.

Equations

• Frourio.JKO_to_EDE_pred F = ∀ (ρ0 : X), Frourio.JKO F ρ0 → ∃ (ρ : ℝ → X), ρ 0 = ρ0 ∧ Frourio.EDE F ρ

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

A geodesic structure provides geodesic interpolation between points. For any two points x and y, and t ∈ [0,1], γ(x,y,t) is a point on the geodesic.

• γ : X → X → ℝ → X
• start_point (x y : X) : self.γ x y 0 = x
• end_point (x y : X) : self.γ x y 1 = y
• geodesic_property (x y : X) (s t : ℝ) : 0 ≤ s → s ≤ 1 → 0 ≤ t → t ≤ 1 → dist (self.γ x y s) (self.γ x y t) = |t - s| * dist x y

def Frourio.GeodesicSemiconvex {X : Type u_2} [PseudoMetricSpace X] (G : GeodesicStructure X) (F : X → ℝ) (lam : ℝ) : Prop

A function F is geodesically λ-semiconvex if it satisfies the semiconvexity inequality along geodesics.

Equations

• Frourio.GeodesicSemiconvex G F lam = ∀ (x y : X) (t : ℝ), 0 ≤ t → t ≤ 1 → F (G.γ x y t) ≤ (1 - t) * F x + t * F y - lam / 2 * t * (1 - t) * dist x y ^ 2

structure Frourio.AnalyticFlagsReal (X : Type u_2) [PseudoMetricSpace X] (F : X → ℝ) (lamEff : ℝ) : Type u_2

Real analytic flags with actual mathematical content (not just placeholders).

• proper : ∃ (c : ℝ), {x : X | F x ≤ c}.Nonempty ∧ BddBelow (Set.range F)
• lsc : LowerSemicontinuous F
• coercive (C : ℝ) : ∃ (R : ℝ), ∀ (x : X), (∃ (x₀ : X), dist x x₀ > R) → F x > C
• geodesic : GeodesicStructure X
• semiconvex : GeodesicSemiconvex self.geodesic F lamEff
• compact_sublevels (c : ℝ) : IsCompact {x : X | F x ≤ c}
• slope_bound : ∃ (M : ℝ), 0 ≤ M ∧ ∀ (x : X), descendingSlope F x ≤ M
• lamLowerBound : ℝ
• lamEff_ge : lamEff ≥ self.lamLowerBound

def Frourio.lamLowerFromRealFlags {X : Type u_2} [PseudoMetricSpace X] {F : X → ℝ} {lamEff : ℝ} (flags : AnalyticFlagsReal X F lamEff) : ℝ

Extract the explicit lower bound on lamEff encoded in real flags.

Equations

• Frourio.lamLowerFromRealFlags flags = flags.lamLowerBound

theorem Frourio.lamEff_ge_fromRealFlags {X : Type u_2} [PseudoMetricSpace X] {F : X → ℝ} {lamEff : ℝ} (flags : AnalyticFlagsReal X F lamEff) : lamEff ≥ lamLowerFromRealFlags flags

The inequality lamEff ≥ lamLowerBound carried by real flags.

def Frourio.ShiftedUSCHypothesis {X : Type u_2} [PseudoMetricSpace X] (F : X → ℝ) (ρ : ℝ → X) : Prop

Helper: USC hypothesis for shifted functions needed in the pipeline

Equations

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

def Frourio.PLFA_EDE_from_real_flags {X : Type u_2} [PseudoMetricSpace X] (F : X → ℝ) (lamEff : ℝ) : Prop

Predicate for converting real analytic flags to PLFA/EDE equivalence. Note: This now requires an additional USC hypothesis

Equations

• Frourio.PLFA_EDE_from_real_flags F lamEff = ∀ (a : Frourio.AnalyticFlagsReal X F lamEff), (∀ (ρ : ℝ → X), Frourio.ShiftedUSCHypothesis F ρ) → Frourio.PLFA_EDE_pred F

def Frourio.JKO_PLFA_from_real_flags {X : Type u_2} [PseudoMetricSpace X] (F : X → ℝ) (lamEff : ℝ) : Prop

Predicate for converting real analytic flags to JKO→PLFA implication.

Equations

• Frourio.JKO_PLFA_from_real_flags F lamEff = ∀ (a : Frourio.AnalyticFlagsReal X F lamEff), Frourio.JKO_to_PLFA_pred F

def Frourio.real_to_placeholder_flags {X : Type u_2} [PseudoMetricSpace X] (F : X → ℝ) (lamEff : ℝ) (_real_flags : AnalyticFlagsReal X F lamEff) : AnalyticFlags F lamEff

Helper: Convert real flags to placeholder flags for compatibility.

Equations

• ⋯ = ⋯

theorem Frourio.plfa_ede_from_real_flags_impl {X : Type u_2} [PseudoMetricSpace X] (F : X → ℝ) (lamEff : ℝ) (_real_flags : AnalyticFlagsReal X F lamEff) (h_usc : ∀ (ρ : ℝ → X), ShiftedUSCHypothesis F ρ) : PLFA_EDE_pred F

Bridge theorem: Real flags with USC hypothesis imply PLFA/EDE equivalence

theorem Frourio.jko_plfa_from_real_flags_impl {X : Type u_2} [PseudoMetricSpace X] (F : X → ℝ) (lamEff : ℝ) (_real_flags : AnalyticFlagsReal X F lamEff) : JKO_to_PLFA_pred F

Bridge theorem: Real flags imply JKO→PLFA using minimizing movement.