Formalizing Perron-Frobenius

Stream: maths

[Matteo Cipollina]

I'm working on a formalization of Perron-Frobenius theorem (needed to prove convergence of discrete Markov chains to stationary distributions, again needed for our ongoing formalization of Boltzmann Machines and Neural Networks). I'm at a good stage, but I need to decide whether to use the Brouwer Fixed-Point theorem or the Collatz-Wielandt method. I'm now trying the CW - where I have set up the framework - but I now just realize that Brouwer fixed point theorem has indeed been formalized in Lean 3 (https://github.com/Shamrock-Frost/BrouwerFixedPoint/tree/master). I was wondering if anyone has done a partial porting of this repo. I'd like to try to port it, but the amount of API is a lot, and I guess some portions would now be obsolete....Any suggestions? Thanks :)

[Sébastien Gouëzel]

This proof will probably be very hard to port to Lean 4. We're waiting for a more principled approach based on singular homology (done using the category framework, which is why it's taking some time to get right). But you definitely don't need Brouwer for Perron-Frobenius, it's a much more elementary compactness argument -- see for instance the standard proof in Seneta's classical book "Non-negative matrices and Markov chains" (or you could do it using the Hilbert metric to get it also in infinite-dimensional spaces, but it requires more prerequisites)

[Oliver Nash]

Aside from agreeing with Sébastien, I'd like to highlight how pleased I am to hear that there is a plan to formalise Perron-Frobenius. I have another independent application ready and waiting: #maths > Eigenvalues of Cartan matrices @ 💬

[Matteo Cipollina]

Thanks for the advice :) I've been following Berman, Plemmons where they use CW function but the proofs are often too sketchy.

[Matteo Cipollina]

first defs and basic lemmas here :
https://github.com/mkaratarakis/HopfieldNet/blob/master/HopfieldNet/Mathematics/LinearAlgebra/Matrix/PerronFrobenius/Defs.lean
some work in progress is here:
https://github.com/mkaratarakis/HopfieldNet/blob/master/HopfieldNet/Mathematics/LinearAlgebra/Matrix/PerronFrobenius/CollatzWielandt.lean
I've got hold of Seneta's book, the proof is very detailed and it seems to roughly follow the one by Berman-Plemmons (CW function), but with much much more detail :)

[Sébastien Gouëzel]

Seneta's book is absolutely great, that's the one I always recommend to my students.

[Matteo Cipollina]

here is the extension of the Extreme Value theorem to upper semicontinuous functions in compact spaces , which I ended up needing to formalize the Collatz-Wielandt maximizer vector. I'm happy to PR it if it can be useful in mathlib
https://github.com/mkaratarakis/HopfieldNet/blob/master/HopfieldNet/Mathematics/Topology/Compactness/ExtremeValueUSC.lean
ExtremeValueUSC.lean

[Antoine Chambert-Loir]

@Anatole Dedecker and I have an alternative version that we had to provide for our formalization of Sion's minimax theorem (a generalization of the von Neumann minimax theorem).

https://github.com/AntoineChambert-Loir/Sion4/blob/cb94fe22577bf53bd59d56b177b83be30f85ce5b/Sion/Semicontinuous.lean#L160

[Matteo Cipollina]

Here is the existence and positivity part of the Perron-Frobenius theorem for primitive non-negative matrices.

https://github.com/mkaratarakis/HopfieldNet/blob/master/HopfieldNet/Mathematics/LinearAlgebra/Matrix/PerronFrobenius/Primitive.lean

The main theorem states:

/-- **Perron-Frobenius theorem for primitive matrices - Existence part**-/
theorem exists_positive_eigenvector_of_primitive
  (hA_prim : IsPrimitive A) (hA_nonneg : ∀ i j, 0 ≤ A i j) :
  ∃ (r : ℝ) (v : n → ℝ), r > 0 ∧ (∀ i, v i > 0) ∧ A *ᵥ v = r • v := by
  -- 1) We get maximizer v on the simplex
  haveI : Nonempty (stdSimplex ℝ n) := by
    let uniform : n → ℝ := fun _ => (Fintype.card n : ℝ)⁻¹
    use uniform
    constructor
    · intro i
      exact inv_nonneg.mpr (Nat.cast_nonneg _)
    · rw [Finset.sum_const, Finset.card_univ, nsmul_eq_mul]
      exact mul_inv_cancel₀ (Nat.cast_ne_zero.mpr Fintype.card_ne_zero)
  obtain ⟨v, hvS, hvM⟩ := CollatzWielandt.exists_maximizer (A := A)
  let r := collatzWielandtFn A v
  -- 2) We show r>0
  have hr : 0 < r := perron_root_pos_of_primitive hA_prim hA_nonneg hvS hvM
  -- 3) maximizer ⇒ eigenvector
  have h_eig := maximizer_is_eigenvector hA_prim hA_nonneg hvM hvS r rfl
  -- 4) primitive ⇒ strict positivity of v
  have hv0 : v ≠ 0 := by
    intro h
    have h_sum_zero : ∑ i, v i = 0 := by rw [h]; simp
    have h_sum_one : ∑ i, v i = 1 := hvS.2
    linarith [h_sum_zero, h_sum_one]
  have hvp := eigenvector_of_primitive_is_positive hA_prim hr h_eig hvS.1 hv0
  use r, v

I've made some minor changes to initial draft to better follows the approach found in Seneta. The proof now defines the Perron root as the supremum of the Collatz-Wielandt function and uses the Extreme Value theorem for semicontinuous functions and an upper-semicontinuity argument on the standard simplex to prove that a maximizer exists and is the required positive eigenvector. It also relies on a new Quiver API for path arguments to handle irreducibility.

Next steps would be to prove the remaining parts of the theorem (uniqueness of the eigenvector, simplicity and dominance of the eigenvalue) and then generalize to all irreducible matrices. Feedback on the current approach would be very welcome!

update: https://github.com/mkaratarakis/HopfieldNet/blob/master/HopfieldNet/Mathematics/LinearAlgebra/Matrix/PerronFrobenius/Uniqueness.lean

[Notification Bot]

9 messages were moved here from #maths > Completed proof of the Brouwer Fixed Point Theorem by Johan Commelin.

[Johan Commelin]

@Matteo Cipollina That's great! I've moved the discussion to a new thread, with a title that covers the topic.

[Matteo Cipollina]

Johan Commelin ha scritto:

Matteo Cipollina That's great! I've moved the discussion to a new thread, with a title that covers the topic.

thanks!

[Matteo Cipollina]

update: the existence, positivity and uniqueness part of the PF theorem has now been generalized to Irreducible matrices here
https://github.com/mkaratarakis/HopfieldNet/blob/master/HopfieldNet/Mathematics/LinearAlgebra/Matrix/PerronFrobenius/Irreducible.lean
implementing Seneta's. This required some non-trivial prerequisites (at least non-trivial for me...) for directed graphs (and Lists) for weights, path decomposition, splitting, cycles etc. I have provisionally put all this Quiver/combinatorics API here
https://github.com/mkaratarakis/HopfieldNet/edit/master/HopfieldNet/Mathematics/Combinatorics/Quiver/Path.lean
The spectral dominance for primitive is close and again it required a lot of background API, among which to prove that 'If equality holds in the triangle inequality for a family of nonzero complex vectors, then all vectors must point in the same direction, i.e., there exists a unit vector csuch that each vector is a non-negative real multiple of c.'
#find_home suggested to put it into Star/Classes folder though it may be more appropriate in some Norm folder.
https://github.com/mkaratarakis/HopfieldNet/blob/master/HopfieldNet/Mathematics/Analysis/CstarAlgebra/Classes.lean

[Matteo Cipollina]

here is the spectral dominance for irreducible and primitive matrices, next is the strict dominance for primitive matrices, then will be simplicity and dealing with irreducible cyclic matrices...

https://github.com/mkaratarakis/HopfieldNet/blob/master/HopfieldNet/Mathematics/LinearAlgebra/Matrix/PerronFrobenius/Dominance.lean

[Matteo Cipollina]

Oliver Nash ha scritto:

Aside from agreeing with Sébastien, I'd like to highlight how pleased I am to hear that there is a plan to formalise Perron-Frobenius. I have another independent application ready and waiting: #maths > Eigenvalues of Cartan matrices @ 💬

Knowing it will be a long process, I have started PRing to Mathlib the combinatorial Quiver API used in the formalization as part of a general clean-up and migration to a mathlib fork , aiming to ultimately PR all the pieces of the PF theorem.
First PRs for Quiver are #27315, #27325 and #27332

@Oliver Nash I think for your application you will need just exists_positive_eigenvector_of_irreducible (in Irreducible.lean) and perron_root_is_spectral_radius for irreducible matrices (in Dominance).

[Oliver Nash]

This is amazing work @Matteo Cipollina I'll try to find time to look at those PRs tomorrow. Separately I'm nearly ready with my own PR which will actually depend upon this work. Thanks so much for doing this, and for upstreaming to Mathlib.

[Matteo Cipollina]

In case anyone would like to have a look , here is the 2nd batch of PRs:
#28696 with lemmas for vertices splitting and decomposition
#28728 introducing StronglyConnected Quiver, toQuiver function bridging Quiver and Matrices, Irreducible and Primitive Matrices and their basic properties. This depends on # 28696
Thanks in advance :)

[Oliver Nash]

Thanks! I'll try to find time to review #28696 within the next day or so.

[Oliver Nash]

As it happens, yesterday we added docs#RootPairing.GeckConstruction.instHasTrivialRadical so the application would be to be able to drop the Fact argument from that typeclass.

[Matteo Cipollina]

Just an update that #29754 has been split from #28728, hope these are now of a size manageable for review.
Also a note that the PF code has been moved to this repository and further developed with more properties of perron root, aperiodicity for Quivers and matrices and applied to finite Markov chain Monte Carlo:
https://github.com/or4nge19/MCMC

[Junyan Xu]

FYI, Perron-Frobenius in Isabelle/HOL later today:

Anand Rao Tadipatri said:

This week's talk will be by René Thiemann on Combining Two Representations of Matrices for a Formalization of the Perron-Frobenius Theorem.

Matrix interpretations are useful for automated complexity analysis of term rewrite systems. For checking the correct application of these interpretations in automatically generated proofs, one needs a verified algorithm to determine the asymptotic growth rate of A^n for a given non-negative real matrix A. Since the direct approach to compute the growth rate of A via algebraic numbers is quite slow, in our certifier CeTA we utilize a simple algorithm that does not require algebraic numbers. Despite the simplicity of the algorithm, its verification in Isabelle/HOL is technically interesting. For proving soundness of the algorithm, we need to formalize the Perron-Frobenius theorem. And to achieve the latter task, we establish a connection between two different Isabelle/HOL libraries on matrices, that facilitates an easy exchange of theorems between both libraries.

We will be live-streaming at 2025-11-27T17:00:00Z on the following Zoom link:

Join Zoom Meeting https://cam-ac-uk.zoom.us/j/89856091954?pwd=Bba77QB2KuTideTlH6PjAmbXLO8HbY.1

Meeting ID: 898 5609 1954 Passcode: ITPtalk