NN.MLTheory.Stability.Spec

Scalar-polymorphic stability definitions for discrete-time dynamical systems $x_{t+1}=f(x_t)$ over shape-indexed tensors.

Stability specifications (discrete-time dynamical systems)

This module defines standard stability notions for iterated maps f : Tensor α s → Tensor α s, phrased over TorchLean's shape-indexed tensors:

• Lyapunov stability,
• asymptotic/exponential stability,
• global stability, and
• input-to-state stability (ISS).

The definitions are polymorphic in the scalar type α via [TorchLean.Storage α] [Context α]; for noncomputable quantities (e.g. the supremum defining a stability margin on ℝ), we expose the notion via a type class StabilityMarginComputable. TorchLean installs the real supremum instance globally and keeps the conservative 0 lower-bound instance behind an explicit opt-in scope for examples and tests.

References

These are standard definitions in control theory / dynamical systems. Useful entry points include:

• H. K. Khalil, Nonlinear Systems (Lyapunov stability, exponential stability, ISS).
• E. D. Sontag, Input-to-State Stability: Basic Concepts and Results (ISS).

@[reducible, inline]

abbrev NN.MLTheory.Stability.Spec.iterate {α : Type} [TorchLean.Storage α] {s : Spec.Shape} (f : TorchLean.Tensor α s → TorchLean.Tensor α s) (n : ℕ) (x : TorchLean.Tensor α s) : TorchLean.Tensor α s

Iterate f for $n$ steps: $\operatorname{iterate}(f,n,x)=f^{[n]}(x)$.

class NN.MLTheory.Stability.Spec.StabilityMarginComputable (α : Type) [TorchLean.Storage α] [Context α] : Type

An interface for a scalar stability-margin calculation. The ℝ instance takes the supremum of nonnegative forward-invariant closed-ball radii. It is not necessarily an attained largest radius; the real supremum requires a nonempty, bounded-above radius set for its usual interpretation. The class itself contains no correctness law for other instances.

TorchLean only installs a real supremum-based instance globally for ℝ. Other scalar backends can opt into the conservative lower-bound instance below explicitly; this avoids silently reporting 0 as a semantic stability margin for arbitrary scalar types.

• computeStabilityMargin {s : Spec.Shape} : (TorchLean.Tensor α s → TorchLean.Tensor α s) → ({s : Spec.Shape} → TorchLean.Tensor α s → α) → TorchLean.Tensor α s → α

Named opt-in scope for the conservative stability-margin lower bound.

Use open scoped NN.MLTheory.Stability.Spec.StabilityMarginComputable.ConservativeMargin only in examples/tests that deliberately want a total fallback. Production theorem statements should either use the ℝ instance or require an explicit StabilityMarginComputable α hypothesis.

@[instance_reducible]

def NN.MLTheory.Stability.Spec.StabilityMarginComputable.ConservativeMargin.inst (α : Type) [TorchLean.Storage α] [Context α] : StabilityMarginComputable α

@[instance_reducible]

noncomputable instance NN.MLTheory.Stability.Spec.instStabilityMarginComputableReal : StabilityMarginComputable ℝ

def NN.MLTheory.Stability.Spec.IsLyapunovStable {α : Type} [TorchLean.Storage α] [Context α] {s : Spec.Shape} (f : TorchLean.Tensor α s → TorchLean.Tensor α s) (norm : {s : Spec.Shape} → TorchLean.Tensor α s → α) (equilibrium : TorchLean.Tensor α s) : Prop

Lyapunov stability of equilibrium for the discrete-time system $x_{t+1}=f(x_t)$.

This is the usual $\varepsilon$/$\delta$ definition using the distance induced by norm.

def NN.MLTheory.Stability.Spec.IsAsymptoticallyStable {α : Type} [TorchLean.Storage α] [Context α] {s : Spec.Shape} (f : TorchLean.Tensor α s → TorchLean.Tensor α s) (norm : {s : Spec.Shape} → TorchLean.Tensor α s → α) (equilibrium : TorchLean.Tensor α s) : Prop

Asymptotic stability: Lyapunov stability plus convergence to equilibrium for nearby initial conditions.

def NN.MLTheory.Stability.Spec.IsExponentiallyStable {α : Type} [TorchLean.Storage α] [Context α] {s : Spec.Shape} (f : TorchLean.Tensor α s → TorchLean.Tensor α s) (norm : {s : Spec.Shape} → TorchLean.Tensor α s → α) (equilibrium : TorchLean.Tensor α s) (decayRate M : α) : Prop

Exponential stability with decay parameters decayRate and M.

Over real scalars with the usual norm and exponential laws, this expresses quantitative decay. The generic predicate alone does not supply those laws.

def NN.MLTheory.Stability.Spec.IsGloballyStable {α : Type} [TorchLean.Storage α] [Context α] {s : Spec.Shape} (f : TorchLean.Tensor α s → TorchLean.Tensor α s) (norm : {s : Spec.Shape} → TorchLean.Tensor α s → α) (equilibrium : TorchLean.Tensor α s) : Prop

Global attraction: every initial condition converges to equilibrium.

The established name IsGloballyStable denotes convergence only; it does not also require the Lyapunov-stability predicate.

This is stated as convergence in the distance induced by norm.

def NN.MLTheory.Stability.Spec.IsInputToStateStable {α : Type} [TorchLean.Storage α] [Context α] {s₁ s₂ : Spec.Shape} (f : TorchLean.Tensor α s₁ → TorchLean.Tensor α s₂ → TorchLean.Tensor α s₁) (norm : {s : Spec.Shape} → TorchLean.Tensor α s → α) (β : α → α → α) (γ : α → α) : Prop

Input-to-state stability (ISS) for an input-driven system $x_{t+1}=f(x_t,u_t)$.

This is the standard bound

$$ \lVert x_t\rVert \leq \beta(\lVert x_0\rVert,t) +\gamma\!\left(\max_{k<t}\lVert u_k\rVert\right) $$

packaged as a Prop. The maximum includes an initial zero and inputs at indices k < t, which are the inputs used to reach state t. This predicate does not require the usual class-KL conditions on β or class-K conditions on γ; those must be supplied separately for standard ISS.

def NN.MLTheory.Stability.Spec.IsInputToStateStable.iterateWithInput {α : Type} [TorchLean.Storage α] {s₁ s₂ : Spec.Shape} (f : TorchLean.Tensor α s₁ → TorchLean.Tensor α s₂ → TorchLean.Tensor α s₁) (inputSeq : ℕ → TorchLean.Tensor α s₂) : ℕ → TorchLean.Tensor α s₁ → TorchLean.Tensor α s₁

def NN.MLTheory.Stability.Spec.IsInputToStateStable.supNormOverTime {α : Type} [TorchLean.Storage α] [Context α] {s₂ : Spec.Shape} (norm : {s : Spec.Shape} → TorchLean.Tensor α s → α) (inputSeq : ℕ → TorchLean.Tensor α s₂) (t : ℕ) : α

def NN.MLTheory.Stability.Spec.IsBiboStable {α : Type} [TorchLean.Storage α] [Context α] {s₁ s₂ : Spec.Shape} (f : TorchLean.Tensor α s₁ → TorchLean.Tensor α s₂) (norm₁ norm₂ : {s : Spec.Shape} → TorchLean.Tensor α s → α) (bound : α) : Prop

A fixed-bound input/output implication: inputs of norm at most bound have outputs of norm at most the same bound. This is not the general BIBO quantification over input and output bounds.

def NN.MLTheory.Stability.Spec.IsIncrementallyStable {α : Type} [TorchLean.Storage α] [Context α] {s : Spec.Shape} (f : TorchLean.Tensor α s → TorchLean.Tensor α s) (norm : {s : Spec.Shape} → TorchLean.Tensor α s → α) (contractionFactor : α) : Prop

Incremental stability: distances between trajectories contract by contractionFactor.

This is a discrete-time contraction condition phrased using tensorDistance.

def NN.MLTheory.Stability.Spec.stabilityMargin {α : Type} [TorchLean.Storage α] [Context α] {s : Spec.Shape} [StabilityMarginComputable α] (f : TorchLean.Tensor α s → TorchLean.Tensor α s) (norm : {s : Spec.Shape} → TorchLean.Tensor α s → α) (equilibrium : TorchLean.Tensor α s) : α

Return the configured stability-margin value. The real instance uses a supremum, which need not be attained and requires boundedness for its usual interpretation; custom instances have no correctness law in this interface.

def NN.MLTheory.Stability.Spec.IsFiniteTimeStable {α : Type} [TorchLean.Storage α] {s : Spec.Shape} (f : TorchLean.Tensor α s → TorchLean.Tensor α s) (_norm : {s : Spec.Shape} → TorchLean.Tensor α s → α) (equilibrium : TorchLean.Tensor α s) (settlingTimeSteps : ℕ) : Prop

Finite-time stability: trajectories reach equilibrium exactly within a fixed step budget.

def NN.MLTheory.Stability.Spec.IsPracticallyStable {α : Type} [TorchLean.Storage α] [Context α] {s : Spec.Shape} (f : TorchLean.Tensor α s → TorchLean.Tensor α s) (norm : {s : Spec.Shape} → TorchLean.Tensor α s → α) (equilibrium : TorchLean.Tensor α s) (ultimateBound : α) : Prop

Practical stability: trajectories eventually enter and remain in a fixed ultimateBound ball.

def NN.MLTheory.Stability.Spec.IsTrainingStable {α : Type} [TorchLean.Storage α] [Context α] {s : Spec.Shape} (updateRule : TorchLean.Tensor α s → TorchLean.Tensor α s) (loss : TorchLean.Tensor α s → α) (parameters : TorchLean.Tensor α s) : Prop

One-step monotonicity of a training loss under an update rule.

This is the “training stability” predicate used as a spec for decreasing-loss update rules.

def NN.MLTheory.Stability.Spec.IsGeneralizationStable {α : Type} [TorchLean.Storage α] [Context α] {s₁ s₂ : Spec.Shape} (trainingAlgorithm : Array (TorchLean.Tensor α s₁ × TorchLean.Tensor α s₂) → TorchLean.Tensor α s₁ → TorchLean.Tensor α s₂) (norm₁ norm₂ : {s : Spec.Shape} → TorchLean.Tensor α s → α) (stabilityConstant : α) : Prop

Generalization stability of a learning algorithm: small dataset changes produce small prediction changes.

This is a generic stability-style specification; concrete instances typically choose a specific dataset metric and output norm.

def NN.MLTheory.Stability.Spec.IsGeneralizationStable.datasetDistance {α : Type} [TorchLean.Storage α] [Context α] {s₁ s₂ : Spec.Shape} (norm₁ norm₂ : {s : Spec.Shape} → TorchLean.Tensor α s → α) (d₁ d₂ : Array (TorchLean.Tensor α s₁ × TorchLean.Tensor α s₂)) : α