Linear and multilinear algebra; matrix theory

The Lean Pool projects whose card's first MSC2020 code is in class 15, “Linear and multilinear algebra; matrix theory”: 2 articles, one per card.

TheoremMonlib4 Operator-Algebra and Quantum-Set Core#

Formalizes monlib4's finite matrix-algebra inner-automorphism theorem, unitary inner automorphisms, star-preserving linear maps, the structural core of quantum sets, the core Schur-product definition of quantum graphs, and a self-contained digit-sum divisibility theorem.

Quoted from the card LeanPool/projects/monlib4.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.

Main results

The card lists 16 main results, each with its informal statement quoted from the card. The scan finds 16 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.

• Matrix.automorphism_matrix_inner (theorem), declared in LeanPool/Monlib4/RepTheory/AutMat.lean, line 49: “Shows that any automorphism of a finite nontrivial matrix algebra is implemented by an invertible intertwining matrix.”
• Matrix.aut_mat_inner (theorem; a main declaration), declared in LeanPool/Monlib4/RepTheory/AutMat.lean, line 210: “Packages matrix-algebra automorphisms as inner automorphisms induced by a linear equivalence of the underlying coordinate space.”
• Matrix.aut_mat_inner' (theorem), declared in LeanPool/Monlib4/RepTheory/AutMat.lean, line 224: “Packages matrix-algebra automorphisms as conjugation by an element of GL n 𝕜.”
• Matrix.aut_mat_inner_trace_preserving (theorem), declared in LeanPool/Monlib4/RepTheory/AutMat.lean, line 243: “Proves that automorphisms of finite matrix algebras preserve trace.”
• Matrix.innerAut (abbrev), declared in LeanPool/Monlib4/LinearAlgebra/InnerAut.lean, line 180: “Defines the linear map induced by conjugation with a unitary matrix.”
• Matrix.innerAut_apply_trace_eq (theorem), declared in LeanPool/Monlib4/LinearAlgebra/InnerAut.lean, line 334: “Proves that unitary inner automorphisms preserve matrix trace.”
• Matrix.innerAut.spectrum_eq (theorem), declared in LeanPool/Monlib4/LinearAlgebra/InnerAut.lean, line 258: “Proves that unitary inner automorphisms preserve the spectrum of the associated linear operator.”
• LinearMap.IsReal (def), declared in LeanPool/Monlib4/LinearAlgebra/IsReal.lean, line 24: “Defines star-preserving, or real, function-like maps.”
• LinearMap.real (def), declared in LeanPool/Monlib4/LinearAlgebra/IsReal.lean, line 40: “Defines the star-conjugate involution on linear maps.”
• QuantumSet (class; a main declaration), declared in LeanPool/Monlib4/LinearAlgebra/QuantumSet/Basic.lean, line 123: “Defines the monlib4 quantum-set structure with modular automorphisms and a fixed orthonormal basis.”
• Complex.quantumSet (instance), declared in LeanPool/Monlib4/LinearAlgebra/QuantumSet/Basic.lean, line 214: “Instantiates the complex numbers as the base quantum set.”
• schurMul (def; a main declaration), declared in LeanPool/Monlib4/LinearAlgebra/QuantumSet/SchurMul.lean, line 35: “Defines the Schur product of linear maps using multiplication, tensoring, and coalgebra comultiplication.”
• QuantumGraph (class; a main declaration), declared in LeanPool/Monlib4/QuantumGraph/Basic.lean, line 527: “Defines quantum graphs as Schur-idempotent endomorphisms.”
• QuantumGraph.Real (class), declared in LeanPool/Monlib4/QuantumGraph/Basic.lean, line 544: “Defines real quantum graphs as Schur-idempotent, star-preserving endomorphisms.”
• nat_repr_mod_eq_sum_repr_mod (theorem), declared in LeanPool/Monlib4/Other/Sonia.lean, line 79: “Proves that the value represented by digits in base a + 1 has the same remainder modulo a as the sum of those digits.”
• nat_dvd_repr_iff_nat_dvd_sum_repr (theorem), declared in LeanPool/Monlib4/Other/Sonia.lean, line 104: “Proves the generalized digit-sum divisibility criterion for base a + 1 modulo a.”

Project

• Authors: Monica Omar.
• Source: doi:10.4169/amer.math.monthly.124.10.966, arXiv:1810.08368.
• Project repository: themathqueen/monlib4.
• Provenance: human, which in Lean Pool's terms means its Lean proofs were “written by people”.
• License: Apache-2.0.
• MSC2020: 15A69, 16W20.
• In Lean Pool: LeanPool/Monlib4, from the card LeanPool/projects/monlib4.yaml.

Sources

• Lean Pool at 2b205bf9: LeanPool/projects/monlib4.yaml
• Lean Pool at 2b205bf9: LeanPool/Monlib4

LeanMatrix.aut_mat_inner · QuantumSet · schurMul · QuantumGraph

TheoremSpectral positivity#

Perron-Frobenius theory, Jentzsch's theorem, and matrix/operator positivity in Lean 4. At the matrix level it proves that nonnegative matrices have nonnegative powers, the Metzler decomposition and positivity of the matrix exponential of a Metzler matrix, M-matrix inverse positivity, and the Perron-Frobenius theorem for irreducible nonnegative matrices (a positive dominant eigenvalue with a strictly positive eigenvector). At the operator level it proves Jentzsch's theorem for compact self-adjoint positivity-improving operators on L2 — a simple, strictly positive ground state with a spectral gap — together with a kernel positivity criterion.

Quoted from the card LeanPool/projects/spectral-positivity.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.

Main results

The card lists 4 main results, each with its informal statement quoted from the card. The scan finds 4 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.

• allpos_has_pos_eigenvec (theorem; a main declaration), declared in LeanPool/SpectralPositivity/Matrix/PerronFrobenius.lean, line 266: “A matrix with all strictly positive entries has a positive eigenvalue with a strictly positive eigenvector (Perron-Frobenius for positive matrices, via the Collatz-Wielandt characterization).”
• perron_frobenius (theorem; a main declaration), declared in LeanPool/SpectralPositivity/Matrix/PerronFrobenius.lean, line 481: “An irreducible (primitive) nonnegative matrix has a positive eigenvalue with a strictly positive eigenvector.”
• ground_state_strictly_positive (theorem; a main declaration), declared in LeanPool/SpectralPositivity/Operator/JentzschProof.lean, line 294: “The ground eigenfunction of a compact self-adjoint positivity-improving operator on L2 is strictly positive almost everywhere (Jentzsch).”
• SpectralPositivity.Matrix.MMatrix.inverse_pos (theorem), declared in LeanPool/SpectralPositivity/Matrix/MMatrixInverse.lean, line 309: “The inverse of a nonsingular irreducible M-matrix is entrywise strictly positive.”

Project

• Authors: Michael R. Douglas.
• Source: spectral-positivity: Perron-Frobenius, Jentzsch, and matrix positivity in Lean 4 by Michael R. Douglas.
• Project repository: mrdouglasny/spectral-positivity.
• Provenance: AI, which in Lean Pool's terms means its Lean proofs were “mostly produced by an AI system”.
• License: Apache-2.0.
• MSC2020: 15B48, 15A18.
• In Lean Pool: LeanPool/SpectralPositivity, from the card LeanPool/projects/spectral-positivity.yaml.

Sources

• Lean Pool at 2b205bf9: LeanPool/projects/spectral-positivity.yaml
• Lean Pool at 2b205bf9: LeanPool/SpectralPositivity

Leanallpos_has_pos_eigenvec · perron_frobenius · ground_state_strictly_positive

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.