PINN Dataset Helpers

Reusable parsing and interval diagnostics for dataset-backed PINN checks.

structure NN.Verification.PINN.Dataset.Point : Type

A scalar PINN sample point (x, y-or-t, u).

• x : Float

  First coordinate.

• yOrT : Float

  Second coordinate, read from y for spatial data or t for time data.

• u : Float

  Reference solution value at the point.

def NN.Verification.PINN.Dataset.instReprPoint.repr : Point → Nat → Std.Format

@[implicit_reducible]

instance NN.Verification.PINN.Dataset.instReprPoint : Repr Point

def NN.Verification.PINN.Dataset.absDiff (a b : Float) : Float

Absolute difference for Float diagnostics.

def NN.Verification.PINN.Dataset.containsWithTol (u lo hi tol : Float) : Bool

Check interval containment with a symmetric tolerance on the endpoints.

def NN.Verification.PINN.Dataset.getYorT (j : Lean.Json) : Except String Float

Read the second coordinate, accepting either y for 2D data or t for 1D-in-time data.

def NN.Verification.PINN.Dataset.parsePoint (j : Lean.Json) : Except String Point

Parse one dataset point as (x, y-or-t, u).

def NN.Verification.PINN.Dataset.loadSection (path sectionName : String) : IO (Array Point)

Load one named dataset section into checked PINN sample points.