NN.MLTheory.Stability.Runtime

Executable Float-specialized diagnostics for the stability specifications in NN.MLTheory.Stability.Spec.

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 NN.MLTheory.Stability.Spec.

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.testExponentialStability {s : Spec.Shape} (f : TorchLean.Tensor Float s → TorchLean.Tensor Float s) (equilibrium x₀ : TorchLean.Tensor Float s) (expectedDecayRate : Float) (maxIterations : ℕ) : Except String Bool

Empirical exponential decay test:

We simulate a trajectory, compute distances $d_t=\lVert x_t-\mathrm{equilibrium}\rVert_2$, and check a simple inequality of the form

$$ d_t\leq d_0 e^{-\mathrm{rate}\,t} $$

for the given expectedDecayRate.

This is a heuristic diagnostic. A theorem about exponential stability should state the dynamical hypotheses separately and use this run only as runtime evidence.

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.testTrainingStability (lossSequence : Array Float) (tolerance : Float) : Except String Bool

Empirical monotonic-loss check for a training log.

Returns .ok true if each consecutive loss satisfies $\ell_{t+1}\leq\ell_t+\mathrm{tolerance}$. Fewer than two losses and non-finite values are inconclusive errors.

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 in testRadii, we generate a small finite set of points on a coordinatewise cosine perturbation around equilibrium and check a bounded-horizon Lyapunov test. The generated points are not generally on the L2 sphere of radius r. 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).

@[instance_reducible]

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

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

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)