FG Interop: Bridges to analysis APIs

Lightweight helpers connecting FG data to the analysis layer without renaming existing APIs. These are thin wrappers around EVIProblem and its predicates, aligning with the design goal of non-destructive integration.

def Frourio.evi_from_fg {X : Type u_1} [PseudoMetricSpace X] [MeasurableSpace X] (FG : FGData X) : EVIProblem X

Induce an EVIProblem from FG data.

Equations

• Frourio.evi_from_fg FG = FG.toEVI

def Frourio.fg_IsEVISolution {X : Type u_1} [PseudoMetricSpace X] [MeasurableSpace X] (FG : FGData X) (u : ℝ → X) : Prop

Predicate alias: u is an EVI solution for the problem induced by FG.

Equations

• Frourio.fg_IsEVISolution FG u = Frourio.IsEVISolution (Frourio.evi_from_fg FG) u

def Frourio.fg_evi_contraction {X : Type u_1} [PseudoMetricSpace X] [MeasurableSpace X] (FG : FGData X) (u v : ℝ → X) (hu : IsEVISolution (evi_from_fg FG) u) (hv : IsEVISolution (evi_from_fg FG) v) : Prop

Contraction statement alias for two curves under the FG-induced EVI problem.

Equations

• Frourio.fg_evi_contraction FG u v hu hv = Frourio.evi_contraction (Frourio.evi_from_fg FG) u v hu hv

def Frourio.fg_evi_contraction_nonneg {X : Type u_1} [PseudoMetricSpace X] [MeasurableSpace X] (FG : FGData X) (u v : Rge0 → X) (hu : IsEVISolutionNonneg (evi_from_fg FG) u) (hv : IsEVISolutionNonneg (evi_from_fg FG) v) : Prop

Nonnegative-time contraction alias via the FG-induced problem.

Equations

• Frourio.fg_evi_contraction_nonneg FG u v hu hv = Frourio.evi_contraction_nonneg (Frourio.evi_from_fg FG) u v hu hv