From 4e2ff28b04a5b7ccf45f3bb169c1c93be05aa7d0 Mon Sep 17 00:00:00 2001
From: "ax-prover[bot]" <254142790+ax-prover[bot]@users.noreply.github.com>
Date: Fri, 1 May 2026 17:24:11 +0000
Subject: [PATCH] Add proof for
 MCMC/PF/LinearAlgebra/Matrix/PerronFrobenius/Dominance.lean

---
 .../Matrix/PerronFrobenius/Dominance.lean       | 17 ++++++++++++++++-
 1 file changed, 16 insertions(+), 1 deletion(-)

diff --git a/MCMC/PF/LinearAlgebra/Matrix/PerronFrobenius/Dominance.lean b/MCMC/PF/LinearAlgebra/Matrix/PerronFrobenius/Dominance.lean
index 7666963..1d33fca 100644
--- a/MCMC/PF/LinearAlgebra/Matrix/PerronFrobenius/Dominance.lean
+++ b/MCMC/PF/LinearAlgebra/Matrix/PerronFrobenius/Dominance.lean
@@ -524,7 +524,22 @@ theorem spectralRadius_eq_nnnorm_perronRoot (hA_irred : A.IsIrreducible) (hA_non
 /-- The spectral radius of an irreducible nonnegative matrix is the Perron root as a real number. -/
 theorem spectralRadius_toReal_eq_perronRoot (hA_irred : A.IsIrreducible) (hA_nonneg : ∀ i j, 0 ≤ A i j) :
     (spectralRadius ℝ A).toReal = perronRoot A := by
-  sorry
+  obtain ⟨hr_spec, hr_bound⟩ := perron_root_is_spectral_radius hA_irred hA_nonneg
+  have hr_nonneg : 0 ≤ perronRoot A := (perronRoot_pos_of_irreducible hA_irred hA_nonneg).le
+  have h_eq : spectralRadius ℝ A = ‖perronRoot A‖₊ := by
+    apply le_antisymm
+    · apply iSup₂_le
+      intro μ hμ
+      simp only [ENNReal.coe_le_coe]
+      have h_abs_le : |μ| ≤ perronRoot A := hr_bound μ hμ
+      calc ‖μ‖₊ = ‖|μ|‖₊ := (Real.nnnorm_abs μ).symm
+           _ = |μ|.toNNReal := (Real.toNNReal_eq_nnnorm_of_nonneg (abs_nonneg μ)).symm
+           _ ≤ (perronRoot A).toNNReal := Real.toNNReal_le_toNNReal h_abs_le
+           _ = ‖perronRoot A‖₊ := Real.toNNReal_eq_nnnorm_of_nonneg hr_nonneg
+    · apply le_iSup₂_of_le (perronRoot A) hr_spec
+      rfl
+  rw [h_eq]
+  simp [Real.norm_eq_abs, abs_of_nonneg hr_nonneg]
 
 /--
 **Perron–Frobenius at the spectral radius:** an irreducible nonnegative matrix admits a strictly