NN.MLTheory.Stability.Runtime

Executable Float-specialized diagnostics for the stability specifications in Spec.Dynamics (NN.Spec.Dynamics.System).

Stability runtime utilities (Float)

This module provides executable, Float-specialized helpers for exploring stability properties of discrete-time systems ($x_{t+1}=f(x_t)$).

All routines in this file are runtime diagnostics:

• they compute concrete trajectories and check concrete inequalities, and
• they return Except String so absent or non-finite evidence cannot pass vacuously.

They are factually correct as computations: “this inequality held on these sampled points for this many steps.” The corresponding theorem statements live in the Prop definitions in Spec.Dynamics.

In other words:

• .ok true means the sampled runtime diagnostic passed;
• .ok false means “found a counterexample to the tested condition”; and
• .error _ means the evidence was empty, non-finite, or otherwise inconclusive.

def NN.MLTheory.Stability.Runtime.generateTrajectory {s : Spec.Shape} (f : TorchLean.Tensor Float s → TorchLean.Tensor Float s) (x₀ : TorchLean.Tensor Float s) (steps : ℕ) : Array (TorchLean.Tensor Float s)

Apply steps transitions of a discrete-time system $x_{t+1}=f(x_t)$, starting at $x_0$.

The returned array has steps + 1 states, including the initial state $x_0$.

def NN.MLTheory.Stability.Runtime.testLyapunovStability {s : Spec.Shape} (f : TorchLean.Tensor Float s → TorchLean.Tensor Float s) (equilibrium : TorchLean.Tensor Float s) (initialPoints : Array (TorchLean.Tensor Float s)) (maxIterations : ℕ) (tolerance : Float) : Except String Bool

Empirical Lyapunov stability test:

For each initial point x₀ in initialPoints, generate maxIterations + 1 states and check that every state stays within tolerance (in L2 distance) of equilibrium.

This is a bounded-time and finite-set check; it does not certify Lyapunov stability.

def NN.MLTheory.Stability.Runtime.testAsymptoticStability {s : Spec.Shape} (f : TorchLean.Tensor Float s → TorchLean.Tensor Float s) (equilibrium : TorchLean.Tensor Float s) (initialPoints : Array (TorchLean.Tensor Float s)) (maxIterations : ℕ) (convergenceThreshold : Float) : Except String Bool

Empirical asymptotic stability test (finite-horizon):

For each x₀ in initialPoints, simulate maxIterations steps and check that the final state is within convergenceThreshold of equilibrium (in L2 distance).

This is a very coarse check: it only inspects the last iterate and does not quantify a rate.

def NN.MLTheory.Stability.Runtime.testContractivity {s : Spec.Shape} (f : TorchLean.Tensor Float s → TorchLean.Tensor Float s) (testPairs : Array (TorchLean.Tensor Float s × TorchLean.Tensor Float s)) (expectedContractionFactor : Float) : Except String Bool

Empirical contractivity test on a finite list of input pairs.

Checks the inequality

$$ \frac{\lVert f(x)-f(y)\rVert_2}{\lVert x-y\rVert_2} \leq \mathrm{expected\_contraction\_factor} $$

for each pair (x,y). Zero-distance pairs are ignored, but at least one positive-distance pair is required.

def NN.MLTheory.Stability.Runtime.testBiboStability {s₁ s₂ : Spec.Shape} (f : TorchLean.Tensor Float s₁ → TorchLean.Tensor Float s₂) (testInputs : Array (TorchLean.Tensor Float s₁)) (inputBound outputBound : Float) : Except String Bool

Empirical BIBO stability test on a finite list of inputs.

For each test input $x$, if $\lVert x\rVert_2\leq\mathrm{input\_bound}$ then we check $\lVert f(x)\rVert_2\leq\mathrm{output\_bound}$.

def NN.MLTheory.Stability.Runtime.estimateStabilityMargin {s : Spec.Shape} (f : TorchLean.Tensor Float s → TorchLean.Tensor Float s) (equilibrium : TorchLean.Tensor Float s) (testRadii : Array Float) (maxIterations : ℕ) : Except String (Option Float)

Empirical estimate of a Lyapunov-style stability margin.

For each candidate radius r, normalize cosine directions and sample inside its L2 ball around equilibrium, then check a bounded-horizon Lyapunov test. If boundary rounding places a point outside the ball, use an interior point on the same ray (or the center if it still rounds outside). The result is some maximum radius when at least one radius passes, and none when valid evidence was collected but every radius failed. Empty or non-finite radius sets are errors.

def NN.MLTheory.Stability.Runtime.estimateStabilityMargin.generatePointsOnSphere {s : Spec.Shape} (center : TorchLean.Tensor Float s) (radius : Float) (count : ℕ) : Array (TorchLean.Tensor Float s)

def NN.MLTheory.Stability.Runtime.estimateStabilityMargin.addSphericalPerturbation {s : Spec.Shape} (center : TorchLean.Tensor Float s) (radius angle : Float) : TorchLean.Tensor Float s

structure NN.MLTheory.Stability.Runtime.StabilityAnalysisResult : Type

Results of a small battery of empirical stability diagnostics.

• isLyapunovStable : Bool

  Result of a finite-horizon Lyapunov test (testLyapunovStability).

• isAsymptoticallyStable : Bool

  Result of a finite-horizon asymptotic test (testAsymptoticStability).

• isContractive : Bool

  Result of an empirical contractivity test (testContractivity).

• isBiboStable : Bool

  Result of a BIBO check (testBiboStability).

• stabilityMargin : Option Float

  Empirical stability margin estimate (estimateStabilityMargin).

• convergenceRate : Option Float

  Empirical convergence-rate estimate (see analyzeStability).

def NN.MLTheory.Stability.Runtime.instReprStabilityAnalysisResult.repr : StabilityAnalysisResult → ℕ → Std.Format

@[instance_reducible]

instance NN.MLTheory.Stability.Runtime.instReprStabilityAnalysisResult : Repr StabilityAnalysisResult

def NN.MLTheory.Stability.Runtime.analyzeStability {s : Spec.Shape} (f : TorchLean.Tensor Float s → TorchLean.Tensor Float s) (equilibrium : TorchLean.Tensor Float s) (testPoints : Array (TorchLean.Tensor Float s)) (maxIterations : ℕ) : Except String StabilityAnalysisResult

Run a small collection of empirical stability diagnostics and summarize the results.

def NN.MLTheory.Stability.Runtime.analyzeStability.estimateConvergenceRate {s : Spec.Shape} (f : TorchLean.Tensor Float s → TorchLean.Tensor Float s) (eq x₀ : TorchLean.Tensor Float s) (steps : ℕ) : Except String (Option Float)