From 83ab6248c195dd59b63e8d6666cfc93b8faae225 Mon Sep 17 00:00:00 2001 From: Per Alexandersson Date: Mon, 24 Aug 2026 11:58:42 +0000 Subject: [PATCH 1/2] feat(matrix): derive irreducibility from adjacent positivity --- .../LinearAlgebra/Matrix/Oscillatory.lean | 130 ++++++++++++++++++ 1 file changed, 130 insertions(+) create mode 100644 RealRooted/Mathlib/LinearAlgebra/Matrix/Oscillatory.lean diff --git a/RealRooted/Mathlib/LinearAlgebra/Matrix/Oscillatory.lean b/RealRooted/Mathlib/LinearAlgebra/Matrix/Oscillatory.lean new file mode 100644 index 000000000..5412ec758 --- /dev/null +++ b/RealRooted/Mathlib/LinearAlgebra/Matrix/Oscillatory.lean @@ -0,0 +1,130 @@ +module + +public import Mathlib.LinearAlgebra.Matrix.Irreducible.Defs +public import Mathlib.Tactic +public import RealRooted.Mathlib.LinearAlgebra.Matrix.TotallyNonneg + +public section + +/- +Copyright (c) 2026 Per Alexandersson. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Per Alexandersson +-/ + +/-! +# Oscillatory matrices + +This file starts the upstream-shaped infrastructure for the classical oscillation +criterion. Fallat--Woerdeman, Theorem 2, says that a totally nonnegative matrix +is oscillatory exactly when it is nonsingular and its first sub- and +superdiagonal entries are positive. + +The local graph-theoretic part of that criterion is independent of total +nonnegativity: a nonnegative matrix indexed by a nontrivial finite chain is +irreducible when both adjacent diagonals are positive. The one-dimensional +case additionally needs a positive entry; total nonnegativity and a nonzero +determinant supply it. + +The remaining oscillation and leading-principal interlacing argument requires +the Li--Mathias Whitney reduction preserving the endpoint principal-section +spectrum, or the equivalent Gantmacher--Krein nodal theorem. It is not claimed +here. + +## Main results + +* `Matrix.isIrreducible_of_nonneg_of_adjacent_pos` +* `Matrix.IsTotallyNonneg.isIrreducible_of_det_ne_zero_of_adjacent_pos` +-/ + +open Quiver + +namespace Quiver + +private noncomputable def pathFromZeroFin {n : ℕ} [Quiver (Fin (n + 1))] + (hforward : ∀ i : Fin n, Nonempty (i.castSucc ⟶ i.succ)) : + ∀ j : Fin (n + 1), Path 0 j := fun j => + Nat.rec + (motive := fun m => ∀ hm : m < n + 1, + Path 0 (⟨m, hm⟩ : Fin (n + 1))) + (fun _ => Path.nil) + (fun m ih hm => by + let i : Fin n := ⟨m, by lia⟩ + exact (ih (by lia)).cons (hforward i).some) + j.val j.isLt + +private noncomputable def pathToZeroFin {n : ℕ} [Quiver (Fin (n + 1))] + (hbackward : ∀ i : Fin n, Nonempty (i.succ ⟶ i.castSucc)) : + ∀ j : Fin (n + 1), Path j 0 := fun j => + Nat.rec + (motive := fun m => ∀ hm : m < n + 1, + Path (⟨m, hm⟩ : Fin (n + 1)) 0) + (fun _ => Path.nil) + (fun m ih hm => by + let i : Fin n := ⟨m, by lia⟩ + exact (hbackward i).some.toPath.comp (ih (by lia))) + j.val j.isLt + +private theorem isStronglyConnected_fin_of_adjacent {n : ℕ} + [Quiver (Fin (n + 1))] + (hforward : ∀ i : Fin n, Nonempty (i.castSucc ⟶ i.succ)) + (hbackward : ∀ i : Fin n, Nonempty (i.succ ⟶ i.castSucc)) : + IsStronglyConnected (Fin (n + 1)) := by + intro i j + exact ⟨(pathToZeroFin hbackward i).comp (pathFromZeroFin hforward j)⟩ + +private theorem isSStronglyConnected_fin_of_adjacent {n : ℕ} + [Quiver (Fin (n + 2))] + (hforward : ∀ i : Fin (n + 1), Nonempty (i.castSucc ⟶ i.succ)) + (hbackward : ∀ i : Fin (n + 1), Nonempty (i.succ ⟶ i.castSucc)) : + IsSStronglyConnected (Fin (n + 2)) := + IsStronglyConnected.isSStronglyConnected_of_hom + (isStronglyConnected_fin_of_adjacent hforward hbackward) + (hforward 0).some + +end Quiver + +namespace Matrix + +/-- A nonnegative matrix on a finite chain of cardinality at least two is +irreducible when all entries immediately above and below the diagonal are +positive. -/ +theorem isIrreducible_of_nonneg_of_adjacent_pos {n : ℕ} + {R : Type*} [Ring R] [LinearOrder R] + {A : Matrix (Fin (n + 2)) (Fin (n + 2)) R} + (hA : ∀ i j, 0 ≤ A i j) + (hsuper : ∀ i : Fin (n + 1), 0 < A i.castSucc i.succ) + (hsub : ∀ i : Fin (n + 1), 0 < A i.succ i.castSucc) : + A.IsIrreducible := by + refine ⟨hA, ?_⟩ + letI : Quiver (Fin (n + 2)) := toQuiver A + exact Quiver.isSStronglyConnected_fin_of_adjacent + (fun i => ⟨PLift.up (hsuper i)⟩) (fun i => ⟨PLift.up (hsub i)⟩) + +/-- The nonsingular TN adjacent-diagonal criterion implies irreducibility. + +This is the graph-theoretic part of the classical oscillation criterion. No +claim that a power is totally positive, that compounds are primitive, or that +principal-section characteristic polynomials interlace is made here. -/ +theorem IsTotallyNonneg.isIrreducible_of_det_ne_zero_of_adjacent_pos + {n : ℕ} {R : Type*} [CommRing R] [LinearOrder R] + {A : Matrix (Fin (n + 1)) (Fin (n + 1)) R} + (hA : A.IsTotallyNonneg) (hdet : A.det ≠ 0) + (hsuper : ∀ i : Fin n, 0 < A i.castSucc i.succ) + (hsub : ∀ i : Fin n, 0 < A i.succ i.castSucc) : + A.IsIrreducible := by + cases n with + | zero => + refine ⟨hA.nonneg, ?_⟩ + intro i j + rw [Fin.eq_zero i, Fin.eq_zero j] + have hne : A 0 0 ≠ 0 := by + simpa [Matrix.det_fin_one] using hdet + have hpos : 0 < A 0 0 := + lt_of_le_of_ne (hA.nonneg 0 0) hne.symm + letI : Quiver (Fin 1) := toQuiver A + exact ⟨(show (0 : Fin 1) ⟶ 0 from PLift.up hpos).toPath, by simp⟩ + | succ n => + exact isIrreducible_of_nonneg_of_adjacent_pos hA.nonneg hsuper hsub + +end Matrix From d7cddc2ff2a7ac0cb49923e291f8dc11c04a1370 Mon Sep 17 00:00:00 2001 From: Per Alexandersson Date: Mon, 24 Aug 2026 12:14:03 +0000 Subject: [PATCH 2/2] feat(matrix): preserve principal spectra under block conjugation --- .../LinearAlgebra/Matrix/Oscillatory.lean | 48 +++++++++++++++++++ 1 file changed, 48 insertions(+) diff --git a/RealRooted/Mathlib/LinearAlgebra/Matrix/Oscillatory.lean b/RealRooted/Mathlib/LinearAlgebra/Matrix/Oscillatory.lean index 5412ec758..68007303c 100644 --- a/RealRooted/Mathlib/LinearAlgebra/Matrix/Oscillatory.lean +++ b/RealRooted/Mathlib/LinearAlgebra/Matrix/Oscillatory.lean @@ -1,5 +1,6 @@ module +public import Mathlib.LinearAlgebra.Matrix.Charpoly.Basic public import Mathlib.LinearAlgebra.Matrix.Irreducible.Defs public import Mathlib.Tactic public import RealRooted.Mathlib.LinearAlgebra.Matrix.TotallyNonneg @@ -35,6 +36,9 @@ here. * `Matrix.isIrreducible_of_nonneg_of_adjacent_pos` * `Matrix.IsTotallyNonneg.isIrreducible_of_det_ne_zero_of_adjacent_pos` +* `Matrix.charpoly_fromBlocks_diagonal_conj` +* `Matrix.charpoly_toBlocks₁₁_fromBlocks_diagonal_conj` +* `Matrix.charpoly_toBlocks₂₂_fromBlocks_diagonal_conj` -/ open Quiver @@ -86,6 +90,50 @@ end Quiver namespace Matrix +section BlockDiagonalConjugation + +variable {R m n : Type*} [CommRing R] + [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] + +/-- Conjugation by two invertible diagonal blocks preserves the characteristic +polynomial of the ambient block matrix. -/ +theorem charpoly_fromBlocks_diagonal_conj + (A : Matrix (m ⊕ n) (m ⊕ n) R) + (P : (Matrix m m R)ˣ) (Q : (Matrix n n R)ˣ) : + (fromBlocks (P : Matrix m m R) 0 0 (Q : Matrix n n R) * A * + fromBlocks (P⁻¹ : Matrix m m R) 0 0 (Q⁻¹ : Matrix n n R)).charpoly = + A.charpoly := by + rw [Matrix.charpoly_mul_comm, ← Matrix.mul_assoc] + simp [Matrix.fromBlocks_multiply, Matrix.fromBlocks_one] + +/-- Block-diagonal conjugation preserves the characteristic polynomial of the +upper-left principal block. -/ +theorem charpoly_toBlocks₁₁_fromBlocks_diagonal_conj + (A₁₁ : Matrix m m R) (A₁₂ : Matrix m n R) + (A₂₁ : Matrix n m R) (A₂₂ : Matrix n n R) + (P : (Matrix m m R)ˣ) (Q : (Matrix n n R)ˣ) : + ((fromBlocks (P : Matrix m m R) 0 0 (Q : Matrix n n R) * + fromBlocks A₁₁ A₁₂ A₂₁ A₂₂ * + fromBlocks (P⁻¹ : Matrix m m R) 0 0 + (Q⁻¹ : Matrix n n R)).toBlocks₁₁).charpoly = + A₁₁.charpoly := by + simp [Matrix.fromBlocks_multiply] + +/-- Block-diagonal conjugation preserves the characteristic polynomial of the +lower-right principal block. -/ +theorem charpoly_toBlocks₂₂_fromBlocks_diagonal_conj + (A₁₁ : Matrix m m R) (A₁₂ : Matrix m n R) + (A₂₁ : Matrix n m R) (A₂₂ : Matrix n n R) + (P : (Matrix m m R)ˣ) (Q : (Matrix n n R)ˣ) : + ((fromBlocks (P : Matrix m m R) 0 0 (Q : Matrix n n R) * + fromBlocks A₁₁ A₁₂ A₂₁ A₂₂ * + fromBlocks (P⁻¹ : Matrix m m R) 0 0 + (Q⁻¹ : Matrix n n R)).toBlocks₂₂).charpoly = + A₂₂.charpoly := by + simp [Matrix.fromBlocks_multiply] + +end BlockDiagonalConjugation + /-- A nonnegative matrix on a finite chain of cardinality at least two is irreducible when all entries immediately above and below the diagonal are positive. -/