Skip to content

Proof for spectralRadius_toReal_eq_perronRoot #37

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
or4nge19 merged 1 commit into from
May 1, 2026
Merged

Proof for spectralRadius_toReal_eq_perronRoot #37

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
17 changes: 16 additions & 1 deletion MCMC/PF/LinearAlgebra/Matrix/PerronFrobenius/Dominance.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
Loading