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 Bool for convenience in scripts/CLIs.

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:

• true means the sampled runtime diagnostic passed;
• false means “found a counterexample to the tested condition”.

def NN.MLTheory.Stability.Runtime.testLyapunovStability {s : Spec.Shape} (f : Spec.Tensor Float s → Spec.Tensor Float s) (equilibrium : Spec.Tensor Float s) (initial_points : List (Spec.Tensor Float s)) (max_iterations : ℕ) (tolerance : Float) : Bool

Empirical Lyapunov stability test:

For each initial point x₀ in initial_points, generate a length-max_iterations trajectory 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.testLyapunovStability.test_trajectory_bounded {s : Spec.Shape} (f : Spec.Tensor Float s → Spec.Tensor Float s) (eq x₀ : Spec.Tensor Float s) (max_iter : ℕ) (tol : Float) : Bool

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

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

The returned list includes the initial state $x_0$ as the first element (because we use scanl).

def NN.MLTheory.Stability.Runtime.testAsymptoticStability {s : Spec.Shape} (f : Spec.Tensor Float s → Spec.Tensor Float s) (equilibrium : Spec.Tensor Float s) (initial_points : List (Spec.Tensor Float s)) (max_iterations : ℕ) (convergence_threshold : Float) : Bool

Empirical asymptotic stability test (finite-horizon):

For each x₀ in initial_points, simulate max_iterations steps and check that the final state is within convergence_threshold 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 : Spec.Tensor Float s → Spec.Tensor Float s) (equilibrium x₀ : Spec.Tensor Float s) (expected_decay_rate : Float) (max_iterations : ℕ) : 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 expected_decay_rate.

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.testExponentialStability.test_exponential_decay (distances : List Float) (rate : Float) : Bool

def NN.MLTheory.Stability.Runtime.testContractivity {s : Spec.Shape} (f : Spec.Tensor Float s → Spec.Tensor Float s) (test_pairs : List (Spec.Tensor Float s × Spec.Tensor Float s)) (expected_contraction_factor : Float) : 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) in test_pairs, ignoring pairs with zero input distance.

def NN.MLTheory.Stability.Runtime.testBiboStability {s₁ s₂ : Spec.Shape} (f : Spec.Tensor Float s₁ → Spec.Tensor Float s₂) (test_inputs : List (Spec.Tensor Float s₁)) (input_bound output_bound : Float) : 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 (loss_sequence : List Float) (tolerance : Float) : Bool

Empirical monotonic-loss check for a training log.

Returns true if each consecutive loss satisfies $\ell_{t+1}\leq\ell_t+\mathrm{tolerance}$.

def NN.MLTheory.Stability.Runtime.estimateStabilityMargin {s : Spec.Shape} (f : Spec.Tensor Float s → Spec.Tensor Float s) (equilibrium : Spec.Tensor Float s) (test_radii : List Float) (max_iterations : ℕ) : Float

Empirical estimate of a Lyapunov-style stability margin.

For each candidate radius r in test_radii, we generate a small finite set of points on a synthetic “sphere” of radius r around equilibrium and check a bounded-horizon Lyapunov test. The result is the maximum radius that passes these finite checks.

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

def NN.MLTheory.Stability.Runtime.estimateStabilityMargin.add_spherical_perturbation {s : Spec.Shape} (center : Spec.Tensor Float s) (radius angle : Float) : Spec.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 (test_lyapunov_stability).

• isAsymptoticallyStable : Bool

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

• isContractive : Bool

  Result of an empirical contractivity test (test_contractivity).

• isBiboStable : Bool

  Result of a BIBO check (test_bibo_stability).

• stabilityMargin : Float

  Empirical stability margin estimate (estimate_stability_margin).

• convergence_rate : Float

  Empirical convergence-rate estimate (see analyze_stability).

def NN.MLTheory.Stability.Runtime.analyzeStability {s : Spec.Shape} (f : Spec.Tensor Float s → Spec.Tensor Float s) (equilibrium : Spec.Tensor Float s) (test_points : List (Spec.Tensor Float s)) (max_iterations : ℕ) : StabilityAnalysisResult

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

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