From 18fc96fe2d68edde2061d7a8e7e74c82c69aee05 Mon Sep 17 00:00:00 2001 From: raaghavt <96094982+raaghav-t@users.noreply.github.com> Date: Thu, 3 Sep 2026 00:17:22 -0700 Subject: [PATCH 1/2] feat: add Hurwitz matrix foundation --- LeanForControl.lean | 1 + LeanForControl/LinearSystems/Basic.lean | 3 +- LeanForControl/LinearSystems/Hurwitz.lean | 149 ++++++++++++++++++++++ LeanForControl/Stability/plan.md | 13 +- README.md | 2 +- blueprint/src/content.tex | 12 ++ 6 files changed, 171 insertions(+), 9 deletions(-) create mode 100644 LeanForControl/LinearSystems/Hurwitz.lean diff --git a/LeanForControl.lean b/LeanForControl.lean index 858e90f..c3718bc 100644 --- a/LeanForControl.lean +++ b/LeanForControl.lean @@ -11,6 +11,7 @@ import LeanForControl.Dini.DiniDeriv import LeanForControl.LinearSystems.Basic import LeanForControl.LinearSystems.Controllability import LeanForControl.LinearSystems.Hautus +import LeanForControl.LinearSystems.Hurwitz import LeanForControl.LinearSystems.MatrixLemmas import LeanForControl.LinearSystems.Observability import LeanForControl.ODEs.ComparisonLemma diff --git a/LeanForControl/LinearSystems/Basic.lean b/LeanForControl/LinearSystems/Basic.lean index a61b473..52fca77 100644 --- a/LeanForControl/LinearSystems/Basic.lean +++ b/LeanForControl/LinearSystems/Basic.lean @@ -23,6 +23,5 @@ This keeps `Aᵏ` available as `A ^ (k : ℕ)` for `k : Fin n` without going through `Fin.val` extraction in every lemma. This file holds *only* shared imports and documentation. Definitions and proofs -live in `LinearSystems.Controllability`, `LinearSystems.Observability`, -and `LinearSystems.MatrixLemmas`. +live in the sibling modules under `LeanForControl/LinearSystems`. -/ diff --git a/LeanForControl/LinearSystems/Hurwitz.lean b/LeanForControl/LinearSystems/Hurwitz.lean new file mode 100644 index 0000000..4831a7b --- /dev/null +++ b/LeanForControl/LinearSystems/Hurwitz.lean @@ -0,0 +1,149 @@ +import LeanForControl.LinearSystems.Basic +import Mathlib.Analysis.Complex.Basic +import Architect + +/-! +# Hurwitz matrices + +This file defines continuous-time Hurwitz stability for real square matrices through +eigenpairs of their complexification. The eigenpair formulation matches the concrete +matrix-vector equations used by the Hautus development and avoids choosing an enumeration +of eigenvalues. + +The definition intentionally allows zero-dimensional matrices. In dimension zero there +are no nonzero eigenvectors, so every matrix is Hurwitz with every rate; the theorem +`isHurwitzWithRate_fin_zero` records this convention explicitly. + +Reference: standard continuous-time linear systems terminology. +-/ + +namespace LinearSystems + +open Matrix + +variable {n : ℕ} + +/-- The entrywise complexification of a real matrix. -/ +noncomputable def complexification (A : Matrix (Fin n) (Fin n) ℝ) : + Matrix (Fin n) (Fin n) ℂ := + A.map (algebraMap ℝ ℂ) + +/-- A real matrix is Hurwitz with decay rate `α` when every complex eigenvalue `μ` +satisfies `μ.re < -α`. + +This is stated using nonzero eigenvectors rather than an eigenvalue enumeration so it can +be used directly with PBH/Hautus arguments. + +Reference: standard continuous-time linear systems terminology. -/ +@[blueprint "def:isHurwitzWithRate" + (statement := /-- A real square matrix $A$ is \emph{Hurwitz with decay rate} + $\alpha$ when every complex eigenpair $(\mu,v)$ with $v \ne 0$ satisfies + $\operatorname{Re}(\mu) < -\alpha$. -/)] +def IsHurwitzWithRate (α : ℝ) (A : Matrix (Fin n) (Fin n) ℝ) : Prop := + ∀ (μ : ℂ) (v : Fin n → ℂ), v ≠ 0 → + complexification A *ᵥ v = μ • v → μ.re < -α + +/-- A real matrix is Hurwitz when all of its complex eigenvalues have negative real part. + +Reference: standard continuous-time linear systems terminology. -/ +@[blueprint "def:isHurwitz" + (statement := /-- A real square matrix is \emph{Hurwitz} when every complex + eigenvalue has strictly negative real part. -/)] +abbrev IsHurwitz (A : Matrix (Fin n) (Fin n) ℝ) : Prop := + IsHurwitzWithRate 0 A + +/-- Ordinary Hurwitz stability is exactly Hurwitz stability with rate zero. + +Original: this is the compatibility lemma for the rate-indexed definition. -/ +theorem isHurwitz_iff_isHurwitzWithRate_zero (A : Matrix (Fin n) (Fin n) ℝ) : + IsHurwitz A ↔ IsHurwitzWithRate 0 A := + Iff.rfl + +/-- A certified Hurwitz decay rate may be weakened. + +Original: monotonicity of the rate-indexed predicate. -/ +theorem IsHurwitzWithRate.mono {A : Matrix (Fin n) (Fin n) ℝ} {α β : ℝ} + (hA : IsHurwitzWithRate α A) (hβα : β ≤ α) : + IsHurwitzWithRate β A := by + intro μ v hv hAv + have hμ := hA μ v hv hAv + linarith + +/-- Zero-dimensional matrices are Hurwitz with every rate, vacuously, because there is no +nonzero eigenvector. + +Original: documents the chosen zero-dimensional convention. -/ +theorem isHurwitzWithRate_fin_zero (α : ℝ) (A : Matrix (Fin 0) (Fin 0) ℝ) : + IsHurwitzWithRate α A := by + intro μ v hv + exfalso + apply hv + funext i + exact i.elim0 + +/-- Complexifying a real spectral shift and applying it to a vector adds the corresponding +complex scalar multiple of that vector. + +Original: bridge used by the spectral-shift characterization. -/ +lemma complexification_add_smul_one_mulVec + (A : Matrix (Fin n) (Fin n) ℝ) (α : ℝ) (v : Fin n → ℂ) : + complexification (A + α • (1 : Matrix (Fin n) (Fin n) ℝ)) *ᵥ v = + complexification A *ᵥ v + (α : ℂ) • v := by + simp [complexification, Matrix.map_add, Matrix.map_smul', Matrix.add_mulVec, + Matrix.smul_mulVec] + +/-- A matrix has decay rate `α` exactly when shifting it by `α I` makes it Hurwitz. + +The sign is positive: an eigenvalue `μ` of `A` becomes `μ + α` for `A + α I`, so +`Re μ < -α` is equivalent to `Re (μ + α) < 0`. + +Reference: the standard spectral-shift property for scalar multiples of the identity. -/ +@[blueprint "thm:isHurwitzWithRate-iff-spectral-shift" + (statement := /-- A real matrix $A$ is Hurwitz with decay rate $\alpha$ if and only if + the spectrally shifted matrix $A + \alpha I$ is Hurwitz. -/) + (proof := /-- A complex eigenvalue $\mu$ of $A$ becomes $\mu + \alpha$ after the shift, + and $\operatorname{Re}(\mu) < -\alpha$ is equivalent to + $\operatorname{Re}(\mu + \alpha) < 0$. -/)] +theorem isHurwitzWithRate_iff_add_smul_one + (α : ℝ) (A : Matrix (Fin n) (Fin n) ℝ) : + IsHurwitzWithRate α A ↔ IsHurwitz (A + α • (1 : Matrix (Fin n) (Fin n) ℝ)) := by + constructor + · intro hA μ v hv hshift + have hbase : complexification A *ᵥ v = (μ - α) • v := by + rw [complexification_add_smul_one_mulVec] at hshift + rw [sub_smul] + exact eq_sub_of_add_eq hshift + have hμ := hA (μ - α) v hv hbase + simp only [Complex.sub_re, Complex.ofReal_re] at hμ + linarith + · intro hshift μ v hv hbase + have heig : complexification (A + α • (1 : Matrix (Fin n) (Fin n) ℝ)) *ᵥ v = + (μ + α) • v := by + rw [complexification_add_smul_one_mulVec, hbase] + simp [add_smul] + have hμ := hshift (μ + α) v hv heig + simp only [Complex.add_re, Complex.ofReal_re] at hμ + linarith + +/-- The one-by-one matrix with entry `-γ` has every decay rate strictly below `γ`. +This is a concrete sanity check for the eigenpair definition and its sign convention. + +Original: direct computation included as a sanity check for the definition. -/ +theorem isHurwitzWithRate_neg_one_by_one {α γ : ℝ} (hαγ : α < γ) : + IsHurwitzWithRate α ((-γ) • (1 : Matrix (Fin 1) (Fin 1) ℝ)) := by + intro μ v hv hAv + have hv0 : v 0 ≠ 0 := by + intro hv0 + apply hv + funext i + fin_cases i + exact hv0 + have heig := congrFun hAv 0 + have hμ : μ = (-γ : ℝ) := by + apply mul_right_cancel₀ hv0 + simpa [complexification, Matrix.mulVec, dotProduct] using heig.symm + rw [hμ] + simp only [Complex.ofReal_re] + linarith + +end LinearSystems diff --git a/LeanForControl/Stability/plan.md b/LeanForControl/Stability/plan.md index 2dced13..a87708b 100644 --- a/LeanForControl/Stability/plan.md +++ b/LeanForControl/Stability/plan.md @@ -140,12 +140,13 @@ Let f : ℝⁿ → ℝⁿ be C¹ with f(x_eq) = 0. Let A = fderiv ℝ f x_eq (th This theorem needs substantial external infrastructure: -- **Hurwitz matrices**: `IsHurwitz A ↔ ∀ λ ∈ A.eigenvalues ℂ, λ.re < 0` - (partially developed in `Lyapunov_old/LinearSystems.lean`) +- **Hurwitz matrices (Phase 1 foundation)**: ✅ `LinearSystems/Hurwitz.lean` defines + `IsHurwitzWithRate` through complex eigenpairs, with rate weakening, spectral shifting, + and explicit zero-dimensional behavior. - **Lyapunov equation for Hurwitz matrices**: If A is Hurwitz, then for any Q ≻ 0 there exists a unique P ≻ 0 satisfying PA + AᵀP = -Q. Use Q = I for simplicity. - (sketched in `Lyapunov_old/LinearSystems.lean`, all sorry) + This is not yet implemented. - **Linearization error bound**: f(x) = Ax + g(x) where ‖g(x)‖/‖x‖ → 0 as x → x_eq. Lean path: Taylor's theorem / `HasFDerivAt` remainder bound. @@ -166,8 +167,8 @@ Given P satisfying PA + AᵀP = -I: ### Priority assessment Linearization is low priority for immediate Lean work because: -- It requires substantial eigenvalue/Hurwitz infrastructure not yet in the library. -- The LinearSystems files have this sketched but all sorry. +- It still requires Lyapunov-equation and linearization-remainder infrastructure. +- Positive-definite matrix Lyapunov-equation existence is not yet formalized. - Proving the Lyapunov equation existence (Sylvester-type) is a significant standalone project. Suggested order: prove Chetaev's theorem first, then revisit linearization. @@ -185,7 +186,7 @@ Suggested order: prove Chetaev's theorem first, then revisit linearization. 3. ~~**Barbashin/Krasovskii corollaries**~~ — ✅ done in `LaSalle.lean`. 4. **Linearization (indirect method)** — new file `Stability/Linearization.lean`. - Blocked on eigenvalue / Lyapunov equation infrastructure. + Blocked on Lyapunov-equation, linearization-remainder, and unstable-branch infrastructure. Estimated effort: 4+ sessions after unblocking. --- diff --git a/README.md b/README.md index bf46243..4b1b7e6 100644 --- a/README.md +++ b/README.md @@ -73,7 +73,7 @@ LeanForControl/ ← Lean source ├── ODEs/ ← comparison lemma, Gronwall–Bellman, ODE existence ├── Dini/ ← Dini derivatives (used by the comparison lemma) ├── Analysis/ ← supporting real-analysis lemmas -└── LinearSystems/ ← matrices, observability, controllability, Hautus +└── LinearSystems/ ← matrices, observability, controllability, Hautus, Hurwitz blueprint/src/ ← .tex sources (run leanblueprint web to render) docbuild/ ← nested project for doc-gen4 home_page/ ← Jekyll scaffold for the project's home page diff --git a/blueprint/src/content.tex b/blueprint/src/content.tex index a5131d5..708634c 100644 --- a/blueprint/src/content.tex +++ b/blueprint/src/content.tex @@ -74,6 +74,18 @@ \subsection{Hautus controllability} \inputleannode{thm:isControllable-iff-hautus} +\section{Hurwitz stability} + +For a real square matrix $A$, Hurwitz stability is expressed through the complex eigenpairs +of its entrywise complexification. The rate-indexed predicate records a strict spectral +margin, and ordinary Hurwitz stability is the zero-rate case. + +\inputleannode{def:isHurwitzWithRate} + +\inputleannode{def:isHurwitz} + +\inputleannode{thm:isHurwitzWithRate-iff-spectral-shift} + \chapter{Ordinary differential equations} \section{Dini derivatives} From 1b7032165f3945c138b5042b0fdb25e8c536b53b Mon Sep 17 00:00:00 2001 From: raaghavt <96094982+raaghav-t@users.noreply.github.com> Date: Thu, 3 Sep 2026 14:05:19 -0700 Subject: [PATCH 2/2] refactor: separate Hurwitz definitions --- LeanForControl.lean | 1 + LeanForControl/LinearSystems/DefsHurwitz.lean | 55 +++++++++++++++++++ LeanForControl/LinearSystems/Hurwitz.lean | 45 +++------------ LeanForControl/Stability/plan.md | 6 +- 4 files changed, 66 insertions(+), 41 deletions(-) create mode 100644 LeanForControl/LinearSystems/DefsHurwitz.lean diff --git a/LeanForControl.lean b/LeanForControl.lean index c3718bc..2e42a7e 100644 --- a/LeanForControl.lean +++ b/LeanForControl.lean @@ -10,6 +10,7 @@ import LeanForControl.Comparison.ComparisonFunctions import LeanForControl.Dini.DiniDeriv import LeanForControl.LinearSystems.Basic import LeanForControl.LinearSystems.Controllability +import LeanForControl.LinearSystems.DefsHurwitz import LeanForControl.LinearSystems.Hautus import LeanForControl.LinearSystems.Hurwitz import LeanForControl.LinearSystems.MatrixLemmas diff --git a/LeanForControl/LinearSystems/DefsHurwitz.lean b/LeanForControl/LinearSystems/DefsHurwitz.lean new file mode 100644 index 0000000..6ef3c04 --- /dev/null +++ b/LeanForControl/LinearSystems/DefsHurwitz.lean @@ -0,0 +1,55 @@ +import LeanForControl.LinearSystems.Basic +import Mathlib.Analysis.Complex.Basic +import Architect + +/-! +# Definitions for Hurwitz matrices + +This file defines continuous-time Hurwitz stability for real square matrices through +eigenpairs of their complexification. The eigenpair formulation matches the concrete +matrix-vector equations used by the Hautus development and avoids choosing an enumeration +of eigenvalues. + +The definition intentionally allows zero-dimensional matrices. In dimension zero there +are no nonzero eigenvectors, so every matrix satisfies the predicate with every rate; +`LinearSystems.isHurwitzWithRate_fin_zero` records this convention explicitly. + +Reference: standard continuous-time linear systems terminology. +-/ + +namespace LinearSystems + +open Matrix + +variable {n : ℕ} + +/-- The entrywise complexification of a real matrix. -/ +noncomputable def complexification (A : Matrix (Fin n) (Fin n) ℝ) : + Matrix (Fin n) (Fin n) ℂ := + A.map (algebraMap ℝ ℂ) + +/-- A real matrix is Hurwitz with decay rate `α` when every complex eigenvalue `μ` +satisfies `μ.re < -α`. + +This is stated using nonzero eigenvectors rather than an eigenvalue enumeration so it can +be used directly with PBH/Hautus arguments. + +Reference: standard continuous-time linear systems terminology. -/ +@[blueprint "def:isHurwitzWithRate" + (statement := /-- A real square matrix $A$ is \emph{Hurwitz with decay rate} + $\alpha$ when every complex eigenpair $(\mu,v)$ with $v \ne 0$ satisfies + $\operatorname{Re}(\mu) < -\alpha$. -/)] +def IsHurwitzWithRate (α : ℝ) (A : Matrix (Fin n) (Fin n) ℝ) : Prop := + ∀ (μ : ℂ) (v : Fin n → ℂ), v ≠ 0 → + complexification A *ᵥ v = μ • v → μ.re < -α + +/-- A real matrix is Hurwitz when all of its complex eigenvalues have negative real part. + +Reference: standard continuous-time linear systems terminology. -/ +@[blueprint "def:isHurwitz" + (statement := /-- A real square matrix is \emph{Hurwitz} when every complex + eigenvalue has strictly negative real part. -/)] +abbrev IsHurwitz (A : Matrix (Fin n) (Fin n) ℝ) : Prop := + IsHurwitzWithRate 0 A + +end LinearSystems diff --git a/LeanForControl/LinearSystems/Hurwitz.lean b/LeanForControl/LinearSystems/Hurwitz.lean index 4831a7b..b840c2b 100644 --- a/LeanForControl/LinearSystems/Hurwitz.lean +++ b/LeanForControl/LinearSystems/Hurwitz.lean @@ -1,20 +1,18 @@ -import LeanForControl.LinearSystems.Basic -import Mathlib.Analysis.Complex.Basic +import LeanForControl.LinearSystems.DefsHurwitz import Architect /-! -# Hurwitz matrices +# Basic theorems for Hurwitz matrices -This file defines continuous-time Hurwitz stability for real square matrices through -eigenpairs of their complexification. The eigenpair formulation matches the concrete -matrix-vector equations used by the Hautus development and avoids choosing an enumeration -of eigenvalues. +This file establishes the basic reusable API for the Hurwitz predicates defined in +`LeanForControl.LinearSystems.DefsHurwitz`. -The definition intentionally allows zero-dimensional matrices. In dimension zero there +The definition intentionally allows zero-dimensional matrices. In dimension zero there are no nonzero eigenvectors, so every matrix is Hurwitz with every rate; the theorem `isHurwitzWithRate_fin_zero` records this convention explicitly. -Reference: standard continuous-time linear systems terminology. +Reference: standard continuous-time spectral-shift properties; the remaining compatibility +lemmas are original infrastructure for this library. -/ namespace LinearSystems @@ -23,35 +21,6 @@ open Matrix variable {n : ℕ} -/-- The entrywise complexification of a real matrix. -/ -noncomputable def complexification (A : Matrix (Fin n) (Fin n) ℝ) : - Matrix (Fin n) (Fin n) ℂ := - A.map (algebraMap ℝ ℂ) - -/-- A real matrix is Hurwitz with decay rate `α` when every complex eigenvalue `μ` -satisfies `μ.re < -α`. - -This is stated using nonzero eigenvectors rather than an eigenvalue enumeration so it can -be used directly with PBH/Hautus arguments. - -Reference: standard continuous-time linear systems terminology. -/ -@[blueprint "def:isHurwitzWithRate" - (statement := /-- A real square matrix $A$ is \emph{Hurwitz with decay rate} - $\alpha$ when every complex eigenpair $(\mu,v)$ with $v \ne 0$ satisfies - $\operatorname{Re}(\mu) < -\alpha$. -/)] -def IsHurwitzWithRate (α : ℝ) (A : Matrix (Fin n) (Fin n) ℝ) : Prop := - ∀ (μ : ℂ) (v : Fin n → ℂ), v ≠ 0 → - complexification A *ᵥ v = μ • v → μ.re < -α - -/-- A real matrix is Hurwitz when all of its complex eigenvalues have negative real part. - -Reference: standard continuous-time linear systems terminology. -/ -@[blueprint "def:isHurwitz" - (statement := /-- A real square matrix is \emph{Hurwitz} when every complex - eigenvalue has strictly negative real part. -/)] -abbrev IsHurwitz (A : Matrix (Fin n) (Fin n) ℝ) : Prop := - IsHurwitzWithRate 0 A - /-- Ordinary Hurwitz stability is exactly Hurwitz stability with rate zero. Original: this is the compatibility lemma for the rate-indexed definition. -/ diff --git a/LeanForControl/Stability/plan.md b/LeanForControl/Stability/plan.md index a87708b..46104f7 100644 --- a/LeanForControl/Stability/plan.md +++ b/LeanForControl/Stability/plan.md @@ -140,9 +140,9 @@ Let f : ℝⁿ → ℝⁿ be C¹ with f(x_eq) = 0. Let A = fderiv ℝ f x_eq (th This theorem needs substantial external infrastructure: -- **Hurwitz matrices (Phase 1 foundation)**: ✅ `LinearSystems/Hurwitz.lean` defines - `IsHurwitzWithRate` through complex eigenpairs, with rate weakening, spectral shifting, - and explicit zero-dimensional behavior. +- **Hurwitz matrices (Phase 1 foundation)**: ✅ `LinearSystems/DefsHurwitz.lean` defines + `IsHurwitzWithRate` through complex eigenpairs; `LinearSystems/Hurwitz.lean` provides + rate weakening, spectral shifting, and explicit zero-dimensional behavior. - **Lyapunov equation for Hurwitz matrices**: If A is Hurwitz, then for any Q ≻ 0 there exists a unique P ≻ 0 satisfying PA + AᵀP = -Q. Use Q = I for simplicity.