def Frourio.linearGeodesicStructure : GeodesicStructure ℝ

Equations

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

def Frourio.chooseAnalyticRoute {X : Type u_1} [PseudoMetricSpace X] (F : X → ℝ) (lamEff : ℝ) (useReal : Bool) : Prop

Integration point: Choose between placeholder and real analytic flags.

Equations

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

theorem Frourio.both_routes_valid {X : Type u_1} [PseudoMetricSpace X] (F : X → ℝ) (lamEff : ℝ) (h_usc : ∀ (ρ : ℝ → X) (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₀) : (∃ (_real_flags : AnalyticFlagsReal X F lamEff), True) → (∃ (_ : AnalyticFlags F lamEff), True) → chooseAnalyticRoute F lamEff true ∨ chooseAnalyticRoute F lamEff false

Theorem: Both routes lead to PLFA/EDE equivalence (when they exist with USC).

Real-route bridge builders (exported): provide the PLFA_EDE_from_real_flags and JKO_PLFA_from_real_flags predicates directly from the corresponding implementation lemmas above. These are convenient when a caller expects the predicate-valued builders rather than the explicit lemmas.

theorem Frourio.plfa_ede_from_real_flags_builder {X : Type u_1} [PseudoMetricSpace X] (F : X → ℝ) (lamEff : ℝ) : PLFA_EDE_from_real_flags F lamEff

Exported builder: real flags ⇒ PLFA↔EDE predicate.

theorem Frourio.jko_plfa_from_real_flags_builder {X : Type u_1} [PseudoMetricSpace X] (F : X → ℝ) (lamEff : ℝ) : JKO_PLFA_from_real_flags F lamEff

Exported builder: real flags ⇒ JKO→PLFA predicate.

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

Equations

• Frourio.EDE_EVI_pred F lamEff = ∀ (ρ : ℝ → X), Frourio.EDE F ρ ↔ Frourio.IsEVISolution { E := F, lam := lamEff } ρ

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

Equations

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

structure Frourio.EquivBuildAssumptions {X : Type u_1} [PseudoMetricSpace X] (F : X → ℝ) (lamEff : ℝ) : Prop

• plfa_iff_ede (ρ : ℝ → X) : PLFA F ρ ↔ EDE F ρ
• ede_iff_evi (ρ : ℝ → X) : EDE F ρ ↔ IsEVISolution { E := F, lam := lamEff } ρ
• jko_to_plfa (ρ0 : X) : JKO F ρ0 → ∃ (ρ : ℝ → X), ρ 0 = ρ0 ∧ PLFA F ρ

theorem Frourio.build_plfaEdeEvi_package {X : Type u_1} [PseudoMetricSpace X] (F : X → ℝ) (lamEff : ℝ) (H : EquivBuildAssumptions F lamEff) : plfaEdeEviJko_equiv F lamEff

theorem Frourio.build_plfaEdeEvi_package_weak {X : Type u_1} [PseudoMetricSpace X] (F : X → ℝ) (lamEff : ℝ) (H : EquivBuildAssumptions F lamEff) : plfaEdeEviJko_equiv F lamEff

structure Frourio.EDEEVIAssumptions {X : Type u_1} [PseudoMetricSpace X] (F : X → ℝ) (lamEff : ℝ) : Prop

• ede_iff_evi (ρ : ℝ → X) : EDE F ρ ↔ IsEVISolution { E := F, lam := lamEff } ρ

theorem Frourio.ede_evi_from_pack {X : Type u_1} [PseudoMetricSpace X] (F : X → ℝ) (lamEff : ℝ) (H : EDEEVIAssumptions F lamEff) : EDE_EVI_pred F lamEff

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

Equations

• Frourio.EDE_EVI_from_analytic_flags F lamEff = (Frourio.HalfConvex F lamEff ∧ Frourio.StrongUpperBound F → Frourio.EDE_EVI_pred F lamEff)

theorem Frourio.ede_evi_from_analytic_flags_with_core {X : Type u_1} [PseudoMetricSpace X] (F : X → ℝ) (lamEff : ℝ) (H : EDE_EVI_from_analytic_flags F lamEff) : EDE_EVI_pred F lamEff

Convenience: instantiate EDE_EVI_from_analytic_flags using core flags. This is a statement-level helper to wire builders without supplying concrete half‑convexity and strong upper bound proofs (both are satisfiable with c = 0).

theorem Frourio.ede_evi_from_real_flags_and_builder_with_bound {X : Type u_2} [PseudoMetricSpace X] (F : X → ℝ) (lamEff : ℝ) (flags : AnalyticFlagsReal X F lamEff) (H : EDE_EVI_from_analytic_flags F lamEff) : EDE_EVI_pred F lamEff ∧ lamEff ≥ lamLowerFromRealFlags flags

Real flags also carry an explicit numeric lower bound for lamEff. Pair the builder result with lamEff ≥ lamLowerBound extracted from the flags.

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

Directional bridge (flags → EDE ⇒ EVI). If this holds together with the reverse direction, it yields EDE_EVI_from_analytic_flags.

Equations

• Frourio.EDE_to_EVI_from_flags F lamEff = (Frourio.HalfConvex F lamEff ∧ Frourio.StrongUpperBound F → ∀ (ρ : ℝ → X), Frourio.EDE F ρ → Frourio.IsEVISolution { E := F, lam := lamEff } ρ)

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

Directional bridge (flags → EVI ⇒ EDE). Pairs with EDE_to_EVI_from_flags to produce EDE_EVI_from_analytic_flags.

Equations

• Frourio.EVI_to_EDE_from_flags F lamEff = (Frourio.HalfConvex F lamEff ∧ Frourio.StrongUpperBound F → ∀ (ρ : ℝ → X), Frourio.IsEVISolution { E := F, lam := lamEff } ρ → Frourio.EDE F ρ)

theorem Frourio.build_ede_evi_from_directional_bridges {X : Type u_1} [PseudoMetricSpace X] (F : X → ℝ) (lamEff : ℝ) (Hfwd : EDE_to_EVI_from_flags F lamEff) (Hrev : EVI_to_EDE_from_flags F lamEff) : EDE_EVI_from_analytic_flags F lamEff

Assemble the equivalence builder EDE_EVI_from_analytic_flags from the two directional bridges under the same analytic flags.

theorem Frourio.ede_evi_pred_from_directional_bridges {X : Type u_1} [PseudoMetricSpace X] (F : X → ℝ) (lamEff : ℝ) (A : AnalyticFlags F lamEff) (Hfwd : EDE_to_EVI_from_flags F lamEff) (Hrev : EVI_to_EDE_from_flags F lamEff) : EDE_EVI_pred F lamEff

From AnalyticFlags, obtain the predicate-level equivalence EDE_EVI_pred provided the two directional bridges hold under the (weaker) core flags HalfConvex and StrongUpperBound.

theorem Frourio.build_EDEEVI_pack_from_directional_bridges {X : Type u_1} [PseudoMetricSpace X] (F : X → ℝ) (lamEff : ℝ) (A : AnalyticFlags F lamEff) (Hfwd : EDE_to_EVI_from_flags F lamEff) (Hrev : EVI_to_EDE_from_flags F lamEff) : EDEEVIAssumptions F lamEff

Package form: build EDEEVIAssumptions from AnalyticFlags and the two directional bridges. This is convenient for downstream pack-based assembly.

theorem Frourio.ede_to_evi_from_builder {X : Type u_1} [PseudoMetricSpace X] (F : X → ℝ) (lamEff : ℝ) (H : EDE_EVI_from_analytic_flags F lamEff) (HC : HalfConvex F lamEff) (SUB : StrongUpperBound F) (ρ : ℝ → X) : EDE F ρ → IsEVISolution { E := F, lam := lamEff } ρ

Convenience: extract each implication directly from the builder and flags.

theorem Frourio.evi_to_ede_from_builder {X : Type u_1} [PseudoMetricSpace X] (F : X → ℝ) (lamEff : ℝ) (H : EDE_EVI_from_analytic_flags F lamEff) (HC : HalfConvex F lamEff) (SUB : StrongUpperBound F) (ρ : ℝ → X) : IsEVISolution { E := F, lam := lamEff } ρ → EDE F ρ

Convenience: extract the reverse implication from the builder and flags.

theorem Frourio.ede_evi_bridge_from_pack {X : Type u_1} [PseudoMetricSpace X] (F : X → ℝ) (lamEff : ℝ) (H : EDEEVIAssumptions F lamEff) : EDE_EVI_from_analytic_flags F lamEff

theorem Frourio.plfa_ede_bridge_from_equiv_pack {X : Type u_1} [PseudoMetricSpace X] (F : X → ℝ) (lamEff : ℝ) (H : EquivBuildAssumptions F lamEff) : PLFA_EDE_from_analytic_flags F lamEff

theorem Frourio.ede_evi_bridge_from_equiv_pack {X : Type u_1} [PseudoMetricSpace X] (F : X → ℝ) (lamEff : ℝ) (H : EquivBuildAssumptions F lamEff) : EDE_EVI_from_analytic_flags F lamEff

theorem Frourio.jko_plfa_bridge_from_equiv_pack {X : Type u_1} [PseudoMetricSpace X] (F : X → ℝ) (lamEff : ℝ) (H : EquivBuildAssumptions F lamEff) : JKO_PLFA_from_analytic_flags F

theorem Frourio.ede_evi_equiv_from_flags {X : Type u_1} [PseudoMetricSpace X] (F : X → ℝ) (lamEff : ℝ) (HC : HalfConvex F lamEff) (SUB : StrongUpperBound F) (H : EDE_EVI_from_analytic_flags F lamEff) (ρ : ℝ → X) : EDE F ρ ↔ IsEVISolution { E := F, lam := lamEff } ρ

theorem Frourio.ede_evi_pred_from_core_flags {X : Type u_1} [PseudoMetricSpace X] (F : X → ℝ) (lamEff : ℝ) (A : AnalyticFlags F lamEff) (Hfwd : EDE_to_EVI_from_flags F lamEff) (Hrev : EVI_to_EDE_from_flags F lamEff) : EDE_EVI_pred F lamEff

theorem Frourio.ede_evi_pred_from_core_flags_via_builder {X : Type u_1} [PseudoMetricSpace X] (F : X → ℝ) (lamEff : ℝ) (A : AnalyticFlags F lamEff) (H : EDE_EVI_from_analytic_flags F lamEff) : EDE_EVI_pred F lamEff

Compatibility alias: recover the old route from flags via a builder.