Consequences of valid Lyapunov bounds

This module derives Lyapunov inequalities from a certificate whose bounds have already been proved valid for the stated functions.

Design:

• LyapunovCert packages bounds on a candidate Lyapunov function V and its derivative V̇ over a boxed region.
• NeuralLyapunov is an abstract interface for V and V̇ (typically defined from a network).
• LyapunovCert.ValidFor records the substantive enclosure theorem. A graph checker may prove it; an external producer cannot obtain it merely by writing numbers to JSON.

The bottom portion specializes to ℝ so that strict inequalities like V_lo > 0 ⟹ V(x) > 0 can be discharged by simple order transitivity (0 < V_lo and V_lo ≤ V(x)).

theorem NN.MLTheory.CROWN.Lyapunov.v_bounded_below {α : Type} [Context α] {n : ℕ} (lyap : NeuralLyapunov α n) (cert : LyapunovCert α n) (hcert : cert.ValidFor lyap) (x : Spec.Tensor α (Spec.Shape.dim n Spec.Shape.scalar)) (hx : cert.region.contains x) : lyap.value x ≥ cert.vLower

V is bounded below on the certified region.

theorem NN.MLTheory.CROWN.Lyapunov.v_bounded_above {α : Type} [Context α] {n : ℕ} (lyap : NeuralLyapunov α n) (cert : LyapunovCert α n) (hcert : cert.ValidFor lyap) (x : Spec.Tensor α (Spec.Shape.dim n Spec.Shape.scalar)) (hx : cert.region.contains x) : lyap.value x ≤ cert.vUpper

V is bounded above on the certified region.

theorem NN.MLTheory.CROWN.Lyapunov.vdot_bounded_below {α : Type} [Context α] {n : ℕ} (lyap : NeuralLyapunov α n) (cert : LyapunovCert α n) (hcert : cert.ValidFor lyap) (x : Spec.Tensor α (Spec.Shape.dim n Spec.Shape.scalar)) (hx : cert.region.contains x) : lyap.orbitalDerivative x ≥ cert.derivativeLower

V̇ is bounded below on the certified region.

theorem NN.MLTheory.CROWN.Lyapunov.vdot_bounded_above {α : Type} [Context α] {n : ℕ} (lyap : NeuralLyapunov α n) (cert : LyapunovCert α n) (hcert : cert.ValidFor lyap) (x : Spec.Tensor α (Spec.Shape.dim n Spec.Shape.scalar)) (hx : cert.region.contains x) : lyap.orbitalDerivative x ≤ cert.derivativeUpper

V̇ is bounded above on the certified region.

theorem NN.MLTheory.CROWN.Lyapunov.quantitative_bounds {α : Type} [Context α] {n : ℕ} (lyap : NeuralLyapunov α n) (cert : LyapunovCert α n) (hcert : cert.ValidFor lyap) : (∀ (x : Spec.Tensor α (Spec.Shape.dim n Spec.Shape.scalar)), cert.region.contains x → cert.vLower ≤ lyap.value x ∧ lyap.value x ≤ cert.vUpper) ∧ ∀ (x : Spec.Tensor α (Spec.Shape.dim n Spec.Shape.scalar)), cert.region.contains x → cert.derivativeLower ≤ lyap.orbitalDerivative x ∧ lyap.orbitalDerivative x ≤ cert.derivativeUpper

Quantitative bounds on V and Vdot over the certified region.

Specialization to ℝ

For proofs involving strict positivity and negativity, we specialize to ℝ, whose linear order supports the required transitivity arguments.

structure NN.MLTheory.CROWN.Lyapunov.RealCert (n : ℕ) : Type

Concrete real-valued certificate format for JSON/importer-facing workflows.

• vLower : ℝ

  Lower bound for the Lyapunov candidate V.

• vUpper : ℝ

  Upper bound for the Lyapunov candidate V.

• derivativeLower : ℝ

  Lower bound for the orbital derivative Vdot.

• derivativeUpper : ℝ

  Upper bound for the orbital derivative Vdot.

• regionLower : Fin n → ℝ

  Lower endpoint of the certified input region, componentwise.

• regionUpper : Fin n → ℝ

  Upper endpoint of the certified input region, componentwise.

noncomputable def NN.MLTheory.CROWN.Lyapunov.RealCert.toCert {n : ℕ} (rc : RealCert n) : LyapunovCert ℝ n

Convert the importer-friendly RealCert record into the canonical LyapunovCert.

theorem NN.MLTheory.CROWN.Lyapunov.Real.v_positive {n : ℕ} (lyap : NeuralLyapunov ℝ n) (cert : LyapunovCert ℝ n) (hcert : cert.ValidFor lyap) (h_pos : cert.vLower > 0) (x : Spec.Tensor ℝ (Spec.Shape.dim n Spec.Shape.scalar)) (hx : cert.region.contains x) : lyap.value x > 0

For ℝ: V is positive when the certified lower bound is positive.

theorem NN.MLTheory.CROWN.Lyapunov.Real.vdot_negative {n : ℕ} (lyap : NeuralLyapunov ℝ n) (cert : LyapunovCert ℝ n) (hcert : cert.ValidFor lyap) (h_neg : cert.derivativeUpper < 0) (x : Spec.Tensor ℝ (Spec.Shape.dim n Spec.Shape.scalar)) (hx : cert.region.contains x) : lyap.orbitalDerivative x < 0

For ℝ: V̇ is negative when its certified upper bound is negative.

theorem NN.MLTheory.CROWN.Lyapunov.Real.lyapunov_conditions {n : ℕ} (lyap : NeuralLyapunov ℝ n) (cert : LyapunovCert ℝ n) (hcert : cert.ValidFor lyap) (h_V_pos : cert.vLower > 0) (h_Vdot_neg : cert.derivativeUpper < 0) : (∀ (x : Spec.Tensor ℝ (Spec.Shape.dim n Spec.Shape.scalar)), cert.region.contains x → lyap.value x > 0) ∧ ∀ (x : Spec.Tensor ℝ (Spec.Shape.dim n Spec.Shape.scalar)), cert.region.contains x → lyap.orbitalDerivative x < 0

Positivity and decay follow from valid strict certificate margins.