Mathlib.LinearAlgebra.FinitePerronFrobeniusPositiveEigenvector
Finite-dimensional Perron--Frobenius infrastructure for symmetric entrywise-nonnegative irreducible real matrices: Rayleigh maxima, absolute-value maximizers, positivity propagation, and restriction/zero-extension bridges.
Basic 7 core · 4 supporting This file fixes the Euclidean-space conventions used by the finite positive Perron eigenvector substrate. ★ exists_unit_eigenvector_sphereRayleighValue
Finite Perron--Frobenius: Rayleigh-value interface
This file fixes the Euclidean-space conventions used by the finite positive
Perron eigenvector substrate. It defines the quadratic form and three equivalent
presentations of its top Rayleigh value: a coordinate unit-sphere sSup, a
Euclidean unit-sphere sSup, and Mathlib's iSup of the Rayleigh quotient.
abbrev EVec reviewed
⚑ flagged
Causalean.Mathlib.LinearAlgebra.FinitePerronFrobeniusPositiveEigenvector
A Euclidean real vector indexed by a finite coordinate type, called a finite real coordinate vector, is given by the Euclidean space on that coordinate type.
Definition (Lean source)
def absVec reviewed
⚑ flagged
Causalean.Mathlib.LinearAlgebra.FinitePerronFrobeniusPositiveEigenvector
The Euclidean vector obtained from a finite real vector by taking the absolute value of every coordinate is given coordinate by coordinate.
def rayleighForm reviewed
⚑ flagged
Causalean.Mathlib.LinearAlgebra.FinitePerronFrobeniusPositiveEigenvector
The quadratic form associated with a finite real matrix and a Euclidean coordinate vector, called its Rayleigh form, is given by the vector-matrix-vector quadratic sum.
def sphereRayleighValue reviewed
⚑ flagged
Causalean.Mathlib.LinearAlgebra.FinitePerronFrobeniusPositiveEigenvector
The greatest quadratic Rayleigh-form value among the Euclidean unit vectors for a finite real matrix, called the Euclidean-sphere top Rayleigh value, is given by a supremum. For an empty coordinate type there are no unit vectors and the supremum of the empty set is zero by convention.
Definition (Lean source)
def coordinateSphereRayleighValue reviewed
⚑ flagged
Causalean.Mathlib.LinearAlgebra.FinitePerronFrobeniusPositiveEigenvector
The greatest quadratic Rayleigh-form value among the coordinate vectors whose squared coordinates sum to one for a finite real matrix, called the coordinate-sphere top Rayleigh value, is given by a supremum. For an empty coordinate type no such vector exists and the supremum of the empty set is zero by convention.
def iSupRayleighValue reviewed
⚑ flagged
Causalean.Mathlib.LinearAlgebra.FinitePerronFrobeniusPositiveEigenvector
Mathlib's supremum Rayleigh quotient for a finite real matrix, called the nonzero-vector top Rayleigh value, is given by the matrix's Euclidean linear map. For an empty coordinate type there are no nonzero vectors and the empty supremum is zero by convention.
theorem exists_unit_eigenvector_sphereRayleighValue reviewed
⚑ flagged
Causalean.Mathlib.LinearAlgebra.FinitePerronFrobeniusPositiveEigenvector
On a nonempty finite coordinate space, a real symmetric matrix has a unit eigenvector at its Euclidean-sphere top Rayleigh value.
Formal statement
hypotheses
conclusion
∃ x : EVec ι,
conclusion 1
‖x‖ = 1
conclusion 2
A.mulVec x = sphereRayleighValue A • x
conclusion 3
rayleighForm A x = sphereRayleighValue A
Proof (Lean source)
theorem exists_unit_eigenvector_sphereRayleighValue [Nonempty ι]
(A : Matrix ι ι ℝ) (hA : A.IsSymm) :
∃ x : EVec ι, ‖x‖ = 1 ∧
A.mulVec x = sphereRayleighValue A • x ∧
rayleighForm A x = sphereRayleighValue A := by
obtain ⟨x, hx, hmax, hval⟩ := exists_unit_isMaxOn_rayleighForm A hA
let T := (toEuclideanLin A).toContinuousLinearMap
have hsym : (toEuclideanLin A).IsSymmetric := by
rw [Matrix.isSymmetric_toEuclideanLin_iff]
simpa [IsHermitian, IsSymm] using hA
have hself : IsSelfAdjoint T := hsym.toSelfAdjoint.prop
have hxne : x ≠ 0 := by
intro hzero
simp [hzero] at hx
have hmaxT : IsMaxOn T.reApplyInnerSelf (sphere (0 : EVec ι) ‖x‖) x := by
intro y hy
change T.reApplyInnerSelf y ≤ T.reApplyInnerSelf x
rw [show T.reApplyInnerSelf y = rayleighForm A y by
simpa [T] using reApplyInnerSelf_toEuclideanLin_eq_rayleighForm A y,
show T.reApplyInnerSelf x = rayleighForm A x by
simpa [T] using reApplyInnerSelf_toEuclideanLin_eq_rayleighForm A x]
apply hmax
simpa [hx] using hy
have heig := hself.hasEigenvector_of_isMaxOn hxne hmaxT
refine ⟨x, hx, ?_, hval⟩
have htop : (⨆ y : {y : EVec ι // y ≠ 0}, T.rayleighQuotient y) =
sphereRayleighValue A := by
simpa [iSupRayleighValue, T] using
(sphereRayleighValue_eq_iSupRayleighValue A).symm
rw [htop] at heig
exact congrArg ofLp heig.apply_eq_smul
4 supporting declarations (lemmas, instances)
-
coordinateSphereRayleighValue_eq_sphereRayleighValuetheorem — With a finite real matrix, the coordinate and Euclidean unit-sphere top Rayleigh values agree.Proof (Lean source)
theorem coordinateSphereRayleighValue_eq_sphereRayleighValue (A : Matrix ι ι ℝ) : coordinateSphereRayleighValue A = sphereRayleighValue A := by unfold coordinateSphereRayleighValue sphereRayleighValue congr 1 ext r constructor · rintro ⟨x, hx, rfl⟩ refine ⟨WithLp.toLp 2 x, ?_, ?_⟩ · have hs : ‖WithLp.toLp 2 x‖ ^ 2 = 1 ^ 2 := by simpa [EuclideanSpace.real_norm_sq_eq] using hx exact (sq_eq_sq₀ (norm_nonneg _) (by norm_num)).mp hs · rfl · rintro ⟨x, hx, rfl⟩ refine ⟨fun i => x i, ?_, rfl⟩ rw [← EuclideanSpace.real_norm_sq_eq, hx] norm_num -
sphereRayleighValue_eq_iSupRayleighValuetheorem — On a nonempty finite coordinate space, a real matrix has its Euclidean unit-sphere top value equal to Mathlib's supremum Rayleigh quotient.Proof (Lean source)
theorem sphereRayleighValue_eq_iSupRayleighValue [Nonempty ι] (A : Matrix ι ι ℝ) : sphereRayleighValue A = iSupRayleighValue A := by let T := (toEuclideanLin A).toContinuousLinearMap rw [iSupRayleighValue, show (toEuclideanLin A).toContinuousLinearMap = T from rfl] rw [T.iSup_rayleigh_eq_iSup_rayleigh_sphere (by norm_num : (0 : ℝ) < 1)] unfold sphereRayleighValue rw [show {r : ℝ | ∃ x : EVec ι, ‖x‖ = 1 ∧ r = rayleighForm A x} = rayleighForm A '' sphere (0 : EVec ι) 1 by ext r simp [eq_comm]] rw [sSup_image'] apply iSup_congr intro x simp only [ContinuousLinearMap.rayleighQuotient] rw [show ‖(x : EVec ι)‖ = 1 by simpa using x.property] simp [T, reApplyInnerSelf_toEuclideanLin_eq_rayleighForm] -
coordinateSphereRayleighValue_eq_iSupRayleighValuetheorem — On a nonempty finite coordinate space, a real matrix has its coordinate unit-sphere top value equal to Mathlib's supremum Rayleigh quotient.Proof (Lean source)
theorem coordinateSphereRayleighValue_eq_iSupRayleighValue [Nonempty ι] (A : Matrix ι ι ℝ) : coordinateSphereRayleighValue A = iSupRayleighValue A := by exact (coordinateSphereRayleighValue_eq_sphereRayleighValue A).trans (sphereRayleighValue_eq_iSupRayleighValue A) -
exists_unit_isMaxOn_rayleighFormtheorem — On a nonempty finite coordinate space, a real symmetric matrix has a unit vector attaining its Euclidean-sphere top Rayleigh value.hypothesesconclusion∃ x : EVec ι,conclusion 1‖x‖ = 1conclusion 2conclusion 3rayleighForm A x = sphereRayleighValue AProof (Lean source)
theorem exists_unit_isMaxOn_rayleighForm [Nonempty ι] (A : Matrix ι ι ℝ) (hA : A.IsSymm) : ∃ x : EVec ι, ‖x‖ = 1 ∧ IsMaxOn (rayleighForm A) (sphere (0 : EVec ι) 1) x ∧ rayleighForm A x = sphereRayleighValue A := by have hcompact : IsCompact (sphere (0 : EVec ι) 1) := isCompact_sphere _ _ have hsphere : (sphere (0 : EVec ι) 1).Nonempty := NormedSpace.sphere_nonempty.mpr (by norm_num) have hcontinuous : Continuous (rayleighForm A) := by unfold rayleighForm mulVec dotProduct fun_prop obtain ⟨x, hx, hmax⟩ := hcompact.exists_isMaxOn hsphere hcontinuous.continuousOn refine ⟨x, by simpa using hx, hmax, ?_⟩ symm apply IsGreatest.csSup_eq constructor · exact ⟨x, by simpa using hx, rfl⟩ · rintro r ⟨y, hy, rfl⟩ apply hmax simpa using hy
Restriction 5 core · 12 supporting This file supplies the coordinate bridges used for finite connected components. ★ sphereRayleighValue_zeroExtendMatrix
Restriction and zero extension
This file supplies the coordinate bridges used for finite connected components.
It defines principal-submatrix restriction and zero extension, proves the exact
mulVec identities they satisfy, and relates the corresponding top Rayleigh
values. Cross-boundary hypotheses are stated explicitly whenever an identity
for the original matrix would otherwise be false.
def restrictMatrix reviewed
⚑ flagged
Causalean.Mathlib.LinearAlgebra.FinitePerronFrobeniusPositiveEigenvector
The principal submatrix of a real square matrix on a finite set of coordinates, called its restricted matrix, is given by selecting those rows and columns.
def restrictVec reviewed
⚑ flagged
Causalean.Mathlib.LinearAlgebra.FinitePerronFrobeniusPositiveEigenvector
The Euclidean vector obtained by restricting a finite real vector to a finite coordinate set, called its restricted vector, is given by retaining those coordinates.
def zeroExtendVec reviewed
⚑ flagged
Causalean.Mathlib.LinearAlgebra.FinitePerronFrobeniusPositiveEigenvector
The Euclidean vector obtained by extending a vector on a finite coordinate subtype by zero outside that finite coordinate set, called its zero extension, is given coordinate by coordinate.
def zeroExtendMatrix reviewed
⚑ flagged
Causalean.Mathlib.LinearAlgebra.FinitePerronFrobeniusPositiveEigenvector
The matrix obtained by extending a matrix on a finite coordinate subtype by zero outside that coordinate set, called its zero extension, is given entry by entry.
theorem sphereRayleighValue_zeroExtendMatrix reviewed
⚑ flagged
Causalean.Mathlib.LinearAlgebra.FinitePerronFrobeniusPositiveEigenvector
On a nonempty finite coordinate space, a nonempty finite coordinate set and an entrywise nonnegative subtype matrix satisfy that zero extension preserves its top Rayleigh value.
Formal statement
hypotheses
conclusion
Proof (Lean source)
theorem sphereRayleighValue_zeroExtendMatrix [Nonempty ι]
(s : Finset ι) [Nonempty s] (B : Matrix s s ℝ)
(hB : ∀ i j, 0 ≤ B i j) :
sphereRayleighValue (zeroExtendMatrix s B) = sphereRayleighValue B := by
apply le_antisymm
· apply csSup_le
· obtain ⟨x, hx⟩ : (sphere (0 : EVec ι) 1).Nonempty :=
NormedSpace.sphere_nonempty.mpr (by norm_num)
exact ⟨rayleighForm (zeroExtendMatrix s B) x, x, by simpa using hx, rfl⟩
· rintro r ⟨x, hx, rfl⟩
rw [rayleighForm_zeroExtendMatrix]
let y := restrictVec s x
have hy_norm : ‖y‖ ≤ 1 := (norm_restrictVec_le s x).trans_eq hx
by_cases hy : y = 0
· change rayleighForm B y ≤ sphereRayleighValue B
simpa [hy, rayleighForm, mulVec, dotProduct] using
sphereRayleighValue_nonneg B hB
· have hy_norm_ne : ‖y‖ ≠ 0 := norm_ne_zero_iff.mpr hy
let u : EVec s := ‖y‖⁻¹ • y
have hu_norm : ‖u‖ = 1 := by
simp [u, norm_smul, hy_norm_ne]
have hu_le : rayleighForm B u ≤ sphereRayleighValue B :=
rayleighForm_le_sphereRayleighValue B u hu_norm
have htop : 0 ≤ sphereRayleighValue B :=
sphereRayleighValue_nonneg B hB
have hy_sq : ‖y‖ ^ 2 ≤ 1 := by nlinarith [norm_nonneg y]
have hy_eq : ‖y‖ • u = y := by
simp [u, smul_smul, hy_norm_ne]
calc
rayleighForm B y = rayleighForm B (‖y‖ • u) :=
congrArg (rayleighForm B) hy_eq.symm
_ = ‖y‖ ^ 2 * rayleighForm B u := rayleighForm_smul B ‖y‖ u
_ ≤ ‖y‖ ^ 2 * sphereRayleighValue B :=
mul_le_mul_of_nonneg_left hu_le (sq_nonneg _)
_ ≤ 1 * sphereRayleighValue B :=
mul_le_mul_of_nonneg_right hy_sq htop
_ = sphereRayleighValue B := one_mul _
· apply csSup_le
· obtain ⟨x, hx⟩ : (sphere (0 : EVec s) 1).Nonempty :=
NormedSpace.sphere_nonempty.mpr (by norm_num)
exact ⟨rayleighForm B x, x, by simpa using hx, rfl⟩
· rintro r ⟨x, hx, rfl⟩
calc
rayleighForm B x =
rayleighForm (zeroExtendMatrix s B) (zeroExtendVec s x) :=
(rayleighForm_zeroExtendMatrix_zeroExtendVec s B x).symm
_ ≤ sphereRayleighValue (zeroExtendMatrix s B) :=
rayleighForm_le_sphereRayleighValue _ _ (by simpa using hx)
12 supporting declarations (lemmas, instances)
-
restrictVec_zeroExtendVectheorem — A finite coordinate set and a vector on its subtype satisfy that restricting its zero extension recovers the original subtype vector.hypothesesconclusionrestrictVec s (zeroExtendVec s x) = xProof (Lean source)
@[simp] theorem restrictVec_zeroExtendVec (s : Finset ι) (x : EVec s) : restrictVec s (zeroExtendVec s x) = x := by ext i simp [restrictVec, zeroExtendVec] -
norm_zeroExtendVectheorem — A finite coordinate set and a vector on its subtype satisfy that zero extension preserves Euclidean norm.Proof (Lean source)
@[simp] theorem norm_zeroExtendVec (s : Finset ι) (x : EVec s) : ‖zeroExtendVec s x‖ = ‖x‖ := by apply (sq_eq_sq₀ (norm_nonneg _) (norm_nonneg _)).mp rw [EuclideanSpace.real_norm_sq_eq, EuclideanSpace.real_norm_sq_eq] change (∑ i : ι, (if hi : i ∈ s then x ⟨i, hi⟩ else 0) ^ 2) = ∑ i : s, (x i) ^ 2 calc _ = ∑ i ∈ s, (if hi : i ∈ s then x ⟨i, hi⟩ else 0) ^ 2 := by symm apply Finset.sum_subset (Finset.subset_univ s) intro i _ hi simp [hi] _ = ∑ i : s, (x i) ^ 2 := by rw [← Finset.sum_coe_sort] simp -
zeroExtendMatrix_mulVec_zeroExtendVectheorem — A finite coordinate set, a subtype matrix, and a subtype vector satisfy that applying the zero-extended matrix to the zero-extended vector equals the zero extension of the subtype action.hypothesesconclusion= zeroExtendVec s (toLp 2 (B.mulVec x))Proof (Lean source)
theorem zeroExtendMatrix_mulVec_zeroExtendVec (s : Finset ι) (B : Matrix s s ℝ) (x : EVec s) : (zeroExtendMatrix s B).mulVec (zeroExtendVec s x) = zeroExtendVec s (toLp 2 (B.mulVec x)) := by ext i by_cases hi : i ∈ s · simp only [zeroExtendMatrix, zeroExtendVec, mulVec, dotProduct, hi, dite_true] calc _ = ∑ j ∈ s, (if hj : j ∈ s then B ⟨i, hi⟩ ⟨j, hj⟩ else 0) * (if hj : j ∈ s then x ⟨j, hj⟩ else 0) := by symm apply Finset.sum_subset (Finset.subset_univ s) intro j _ hj simp [hj] _ = ∑ j : s, B ⟨i, hi⟩ j * x j := by rw [← Finset.sum_coe_sort] simp · simp [zeroExtendMatrix, zeroExtendVec, mulVec, dotProduct, hi] -
rayleighForm_zeroExtendMatrix_zeroExtendVectheorem — A finite coordinate set, a subtype matrix, and a subtype vector satisfy that zero extension preserves their Rayleigh form.hypothesesconclusionProof (Lean source)
theorem rayleighForm_zeroExtendMatrix_zeroExtendVec (s : Finset ι) (B : Matrix s s ℝ) (x : EVec s) : rayleighForm (zeroExtendMatrix s B) (zeroExtendVec s x) = rayleighForm B x := by unfold rayleighForm rw [zeroExtendMatrix_mulVec_zeroExtendVec] change (∑ i : ι, (if hi : i ∈ s then x ⟨i, hi⟩ else 0) * (if hi : i ∈ s then (B.mulVec x) ⟨i, hi⟩ else 0)) = ∑ i : s, x i * (B.mulVec x) i calc _ = ∑ i ∈ s, (if hi : i ∈ s then x ⟨i, hi⟩ else 0) * (if hi : i ∈ s then (B.mulVec x) ⟨i, hi⟩ else 0) := by symm apply Finset.sum_subset (Finset.subset_univ s) intro i _ hi simp [hi] _ = ∑ i : s, x i * (B.mulVec x) i := by rw [← Finset.sum_coe_sort] simp -
restrictMatrix_isSymmtheorem — A symmetric finite matrix and a finite coordinate set ensure that the principal restricted matrix remains symmetric.hypothesesconclusion(restrictMatrix A s).IsSymmProof (Lean source)
theorem restrictMatrix_isSymm {A : Matrix ι ι ℝ} (hA : A.IsSymm) (s : Finset ι) : (restrictMatrix A s).IsSymm := by exact hA.submatrix val -
restrictMatrix_nonnegtheorem — An entrywise nonnegative finite matrix and a finite coordinate set ensure that the principal restricted matrix remains entrywise nonnegative.hypothesesconclusion0 ≤ restrictMatrix A s i jProof (Lean source)
theorem restrictMatrix_nonneg {A : Matrix ι ι ℝ} (hA : ∀ i j, 0 ≤ A i j) (s : Finset ι) : ∀ i j, 0 ≤ restrictMatrix A s i j := by intro i j exact hA i.1 j.1 -
restrictMatrix_mulVec_restrictVec_of_zero_offtheorem — A finite matrix, a finite coordinate set, and a vector that vanishes outside the set ensure that restriction commutes with applying the matrix.hypothesesconclusionProof (Lean source)
theorem restrictMatrix_mulVec_restrictVec_of_zero_off (A : Matrix ι ι ℝ) (s : Finset ι) (x : EVec ι) (hx : ∀ i, i ∉ s → x i = 0) : (restrictMatrix A s).mulVec (restrictVec s x) = restrictVec s (toLp 2 (A.mulVec x)) := by ext i change (∑ j : s, A i.1 j.1 * x j.1) = ∑ j : ι, A i.1 j * x j calc _ = ∑ j ∈ s, A i.1 j * x j := by simpa using Finset.sum_coe_sort s (fun j => A i.1 j * x j) _ = ∑ j : ι, A i.1 j * x j := by apply Finset.sum_subset (Finset.subset_univ s) intro j _ hj simp [hx j hj] -
mulVec_zeroExtendVec_of_closedtheorem — A finite matrix, a finite coordinate set, and block closure from outside rows into the set ensure that applying the original matrix to a zero extension equals the zero extension of the restricted action.hypothesesι :sharedType u_1A :Matrix ι ι ℝs :Finset ιhclosed :∀ i jifi ∉ sandj ∈ sthenA i j = 0x :EVec sconclusionA.mulVec (zeroExtendVec s x)Proof (Lean source)
theorem mulVec_zeroExtendVec_of_closed (A : Matrix ι ι ℝ) (s : Finset ι) (hclosed : ∀ i j, i ∉ s → j ∈ s → A i j = 0) (x : EVec s) : A.mulVec (zeroExtendVec s x) = zeroExtendVec s (toLp 2 ((restrictMatrix A s).mulVec x)) := by ext i simp only [mulVec, dotProduct, zeroExtendVec, restrictMatrix, Matrix.submatrix_apply] by_cases hi : i ∈ s · simp only [hi, dite_true] calc _ = ∑ j ∈ s, A i j * (if hj : j ∈ s then x ⟨j, hj⟩ else 0) := by symm apply Finset.sum_subset (Finset.subset_univ s) intro j _ hj simp [hj] _ = ∑ j : s, A i j.1 * x j := by rw [← Finset.sum_coe_sort] simp · simp only [hi, dite_false] apply Finset.sum_eq_zero intro j _ by_cases hj : j ∈ s · simp [hj, hclosed i j hi hj] · simp [hj] -
zeroExtendVec_eigenvector_of_closedtheorem — A finite matrix, a finite coordinate set, block closure from outside rows into the set, and a restricted eigen-equation ensure that zero extension satisfies the corresponding global eigen-equation.hypothesesι :sharedType u_1A :Matrix ι ι ℝs :Finset ιhclosed :∀ i jifi ∉ sandj ∈ sthenA i j = 0x :EVec sρ :ℝhx :(restrictMatrix A s).mulVec x = ρ • xconclusionA.mulVec (zeroExtendVec s x) = ρ • zeroExtendVec s xProof (Lean source)
theorem zeroExtendVec_eigenvector_of_closed (A : Matrix ι ι ℝ) (s : Finset ι) (hclosed : ∀ i j, i ∉ s → j ∈ s → A i j = 0) {x : EVec s} {ρ : ℝ} (hx : (restrictMatrix A s).mulVec x = ρ • x) : A.mulVec (zeroExtendVec s x) = ρ • zeroExtendVec s x := by rw [mulVec_zeroExtendVec_of_closed A s hclosed, hx] ext i by_cases hi : i ∈ s <;> simp [zeroExtendVec, hi] -
rayleighForm_restrictVec_of_zero_offtheorem — A finite matrix, a finite coordinate set, and a vector that vanishes outside that set ensure that restriction preserves its Rayleigh form.hypothesesconclusionProof (Lean source)
theorem rayleighForm_restrictVec_of_zero_off (A : Matrix ι ι ℝ) (s : Finset ι) (x : EVec ι) (hx : ∀ i, i ∉ s → x i = 0) : rayleighForm (restrictMatrix A s) (restrictVec s x) = rayleighForm A x := by unfold rayleighForm rw [restrictMatrix_mulVec_restrictVec_of_zero_off A s x hx] change (∑ i : s, x i.1 * (A.mulVec x) i.1) = ∑ i : ι, x i * (A.mulVec x) i calc _ = ∑ i ∈ s, x i * (A.mulVec x) i := by simpa using Finset.sum_coe_sort s (fun i => x i * (A.mulVec x) i) _ = ∑ i : ι, x i * (A.mulVec x) i := by apply Finset.sum_subset (Finset.subset_univ s) intro i _ hi simp [hx i hi] -
sphereRayleighValue_restrictMatrix_letheorem — On a nonempty finite coordinate space, a finite matrix and a nonempty finite coordinate set satisfy that the restricted top Rayleigh value is at most the global top Rayleigh value.hypothesesconclusionProof (Lean source)
theorem sphereRayleighValue_restrictMatrix_le [Nonempty ι] (A : Matrix ι ι ℝ) (s : Finset ι) [Nonempty s] : sphereRayleighValue (restrictMatrix A s) ≤ sphereRayleighValue A := by apply csSup_le · obtain ⟨x, hx⟩ : (sphere (0 : EVec s) 1).Nonempty := NormedSpace.sphere_nonempty.mpr (by norm_num) exact ⟨rayleighForm (restrictMatrix A s) x, x, by simpa using hx, rfl⟩ · rintro r ⟨x, hx, rfl⟩ have hx_off : ∀ i, i ∉ s → zeroExtendVec s x i = 0 := by intro i hi simp [zeroExtendVec, hi] have hform := rayleighForm_restrictVec_of_zero_off A s (zeroExtendVec s x) hx_off calc rayleighForm (restrictMatrix A s) x = rayleighForm A (zeroExtendVec s x) := by simpa using hform _ ≤ sphereRayleighValue A := rayleighForm_le_sphereRayleighValue A (zeroExtendVec s x) (by simpa using hx) -
sphereRayleighValue_restrictMatrix_eq_of_supported_maximizertheorem — On a nonempty finite coordinate space, a finite matrix, a nonempty finite coordinate set, and a global unit maximizer supported on that set ensure that the restricted and global top Rayleigh values agree.hypothesesι :sharedType u_1Nonempty ιA :Matrix ι ι ℝs :Finset ιNonempty sx :EVec ιhx_norm :‖x‖ = 1hx_support :∀ iifi ∉ sthenx i = 0hx_top :rayleighForm A x = sphereRayleighValue AconclusionProof (Lean source)
theorem sphereRayleighValue_restrictMatrix_eq_of_supported_maximizer [Nonempty ι] (A : Matrix ι ι ℝ) (s : Finset ι) [Nonempty s] {x : EVec ι} (hx_norm : ‖x‖ = 1) (hx_support : ∀ i, i ∉ s → x i = 0) (hx_top : rayleighForm A x = sphereRayleighValue A) : sphereRayleighValue (restrictMatrix A s) = sphereRayleighValue A := by apply le_antisymm · exact sphereRayleighValue_restrictMatrix_le A s · have hzeroExtend : zeroExtendVec s (restrictVec s x) = x := by ext i by_cases hi : i ∈ s · simp [zeroExtendVec, restrictVec, hi] · simp [zeroExtendVec, hi, hx_support i hi] have hrestrict_norm : ‖restrictVec s x‖ = 1 := by rw [← norm_zeroExtendVec s (restrictVec s x), hzeroExtend, hx_norm] calc sphereRayleighValue A = rayleighForm A x := hx_top.symm _ = rayleighForm (restrictMatrix A s) (restrictVec s x) := (rayleighForm_restrictVec_of_zero_off A s x hx_support).symm _ ≤ sphereRayleighValue (restrictMatrix A s) := rayleighForm_le_sphereRayleighValue _ _ hrestrict_norm
AbsoluteValue 1 core · 7 supporting For an entrywise-nonnegative matrix, taking coordinatewise absolute values preserves Euclidean norm and can only increase the quadratic form. ★ absVec_eigenvector_of_isMaxOn
Absolute values of Rayleigh maximizers
For an entrywise-nonnegative matrix, taking coordinatewise absolute values preserves Euclidean norm and can only increase the quadratic form. Consequently it preserves unit-sphere maximality; for a symmetric matrix the resulting nonnegative maximizer is again a top eigenvector.
theorem absVec_eigenvector_of_isMaxOn reviewed
⚑ flagged
Causalean.Mathlib.LinearAlgebra.FinitePerronFrobeniusPositiveEigenvector
On a nonempty finite coordinate space, an entrywise nonnegative symmetric real matrix, a unit-sphere vector, and its Rayleigh-form maximality ensure that the coordinatewise absolute vector is an eigenvector at the top Rayleigh value.
Formal statement
Proof (Lean source)
theorem absVec_eigenvector_of_isMaxOn [Nonempty ι]
(A : Matrix ι ι ℝ) (hA_symm : A.IsSymm) (hA_nonneg : ∀ i j, 0 ≤ A i j)
{x : EVec ι} (hx : x ∈ sphere (0 : EVec ι) 1)
(hmax : IsMaxOn (rayleighForm A) (sphere (0 : EVec ι) 1) x) :
A.mulVec (absVec x) = sphereRayleighValue A • absVec x := by
let T := (toEuclideanLin A).toContinuousLinearMap
have hsym : (toEuclideanLin A).IsSymmetric := by
rw [Matrix.isSymmetric_toEuclideanLin_iff]
simpa [IsHermitian, IsSymm] using hA_symm
have hself : IsSelfAdjoint T := hsym.toSelfAdjoint.prop
have habs_norm : ‖absVec x‖ = 1 := by
rw [norm_absVec]
simpa [mem_sphere] using hx
have habs_ne : absVec x ≠ 0 := by
intro hzero
simp [hzero] at habs_norm
have habs_max := absVec_isMaxOn A hA_nonneg hx hmax
have hmaxT : IsMaxOn T.reApplyInnerSelf
(sphere (0 : EVec ι) ‖absVec x‖) (absVec x) := by
intro y hy
change T.reApplyInnerSelf y ≤ T.reApplyInnerSelf (absVec x)
change rayleighForm A y ≤ rayleighForm A (absVec x)
apply habs_max
simpa [habs_norm] using hy
have heig := hself.hasEigenvector_of_isMaxOn habs_ne hmaxT
have htop : (⨆ y : {y : EVec ι // y ≠ 0}, T.rayleighQuotient y) =
sphereRayleighValue A := by
simpa [iSupRayleighValue, T] using
(sphereRayleighValue_eq_iSupRayleighValue A).symm
rw [htop] at heig
exact congrArg ofLp heig.apply_eq_smul
7 supporting declarations (lemmas, instances)
-
norm_absVectheorem — With a Euclidean coordinate vector, coordinatewise absolute value preserves its Euclidean norm.Proof (Lean source)
@[simp] theorem norm_absVec (x : EVec ι) : ‖absVec x‖ = ‖x‖ := by apply (sq_eq_sq₀ (norm_nonneg _) (norm_nonneg _)).mp simp [EuclideanSpace.real_norm_sq_eq, absVec] -
absVec_nonnegtheorem — With a Euclidean coordinate vector and a coordinate, the corresponding coordinatewise absolute value is nonnegative.Proof (Lean source)
-
rayleighForm_le_absVectheorem — An entrywise nonnegative finite real matrix and a Euclidean coordinate vector satisfy that taking coordinatewise absolute values cannot lower the Rayleigh form.hypothesesconclusionProof (Lean source)
theorem rayleighForm_le_absVec (A : Matrix ι ι ℝ) (hA : ∀ i j, 0 ≤ A i j) (x : EVec ι) : rayleighForm A x ≤ rayleighForm A (absVec x) := by unfold rayleighForm mulVec dotProduct apply Finset.sum_le_sum intro i hi rw [Finset.mul_sum, Finset.mul_sum] apply Finset.sum_le_sum intro j hj have h := mul_le_mul_of_nonneg_left (le_abs_self (x i * x j)) (hA i j) change x i * (A i j * x j) ≤ |x i| * (A i j * |x j|) rw [abs_mul] at h nlinarith -
absVec_mem_spheretheorem — A radius and a Euclidean coordinate vector on the sphere of that radius satisfy that coordinatewise absolute value remains on the same sphere.hypotheses -
rayleighForm_absVec_eq_of_isMaxOntheorem — An entrywise nonnegative finite real matrix, a unit-sphere vector, and its Rayleigh-form maximality ensure that taking coordinatewise absolute values preserves the Rayleigh-form value.Proof (Lean source)
theorem rayleighForm_absVec_eq_of_isMaxOn (A : Matrix ι ι ℝ) (hA : ∀ i j, 0 ≤ A i j) {x : EVec ι} (hx : x ∈ sphere (0 : EVec ι) 1) (hmax : IsMaxOn (rayleighForm A) (sphere (0 : EVec ι) 1) x) : rayleighForm A (absVec x) = rayleighForm A x := by apply le_antisymm · exact hmax (absVec_mem_sphere hx) · exact rayleighForm_le_absVec A hA x -
absVec_isMaxOntheorem — An entrywise nonnegative finite real matrix, a unit-sphere vector, and its Rayleigh-form maximality ensure that coordinatewise absolute value is another unit-sphere maximizer.Proof (Lean source)
theorem absVec_isMaxOn (A : Matrix ι ι ℝ) (hA : ∀ i j, 0 ≤ A i j) {x : EVec ι} (hx : x ∈ sphere (0 : EVec ι) 1) (hmax : IsMaxOn (rayleighForm A) (sphere (0 : EVec ι) 1) x) : IsMaxOn (rayleighForm A) (sphere (0 : EVec ι) 1) (absVec x) := by intro y hy rw [rayleighForm_absVec_eq_of_isMaxOn A hA hx hmax] exact hmax hy -
absVec_preserves_top_eigenvectortheorem — On a nonempty finite coordinate space, an entrywise nonnegative symmetric real matrix and a normalized top eigenvector ensure that coordinatewise absolute value is a normalized nonnegative top eigenvector with the same top value.hypothesesι :sharedType u_1Nonempty ιA :Matrix ι ι ℝhA_symm :A.IsSymmhA_nonneg :∀ i j, 0 ≤ A i jx :EVec ιhx_norm :‖x‖ = 1hx_eigen :A.mulVec x = sphereRayleighValue A • xhx_top :rayleighForm A x = sphereRayleighValue Aconclusionconclusion 1‖absVec x‖ = 1conclusion 3conclusion 4Proof (Lean source)
theorem absVec_preserves_top_eigenvector [Nonempty ι] (A : Matrix ι ι ℝ) (hA_symm : A.IsSymm) (hA_nonneg : ∀ i j, 0 ≤ A i j) {x : EVec ι} (hx_norm : ‖x‖ = 1) (hx_eigen : A.mulVec x = sphereRayleighValue A • x) (hx_top : rayleighForm A x = sphereRayleighValue A) : ‖absVec x‖ = 1 ∧ (∀ i, 0 ≤ absVec x i) ∧ rayleighForm A (absVec x) = sphereRayleighValue A ∧ A.mulVec (absVec x) = sphereRayleighValue A • absVec x := by have hx : x ∈ sphere (0 : EVec ι) 1 := by simpa [mem_sphere] using hx_norm obtain ⟨y, hy_norm, hy_max, hy_value⟩ := exists_unit_isMaxOn_rayleighForm A hA_symm have hx_max : IsMaxOn (rayleighForm A) (sphere (0 : EVec ι) 1) x := by intro z hz calc rayleighForm A z ≤ rayleighForm A y := hy_max hz _ = sphereRayleighValue A := hy_value _ = rayleighForm A x := hx_top.symm refine ⟨norm_absVec x |>.trans hx_norm, absVec_nonneg x, ?_, ?_⟩ · exact (rayleighForm_absVec_eq_of_isMaxOn A hA_nonneg hx hx_max).trans hx_top · exact absVec_eigenvector_of_isMaxOn A hA_symm hA_nonneg hx hx_max
Main 1 core · 1 supporting This module assembles the finite-dimensional Perron--Frobenius theorem for a real symmetric irreducible nonnegative matrix. ★ finite_positive_perron_eigenvector
Finite positive Perron eigenvector
This module assembles the finite-dimensional Perron--Frobenius theorem for a
real symmetric irreducible nonnegative matrix. Its eigenvalue is simultaneously
identified with the coordinate unit-sphere supremum, the Euclidean unit-sphere
supremum, and Mathlib's nonzero-vector iSup Rayleigh quotient.
theorem finite_positive_perron_eigenvector reviewed
⚑ flagged
Causalean.Mathlib.LinearAlgebra.FinitePerronFrobeniusPositiveEigenvector
A real symmetric irreducible finite matrix has a strictly positive unit eigenvector whose eigenvalue is simultaneously the coordinate-sphere, Euclidean-sphere, and nonzero-vector top Rayleigh value.
Formal statement
hypotheses
conclusion
∃ (v : EVec ι) (ρ : ℝ),
‖v‖ = 1
conclusion 1
i :
0 < v i
conclusion 2
A.mulVec v = ρ • v
conclusion 3
rayleighForm A v = ρ
conclusion 4
ρ = sphereRayleighValue A
conclusion 5
conclusion 6
ρ = iSupRayleighValue A
Proof (Lean source)
theorem finite_positive_perron_eigenvector
(A : Matrix ι ι ℝ) (hA_symm : A.IsSymm) (hA_irred : A.IsIrreducible) :
∃ (v : EVec ι) (ρ : ℝ),
‖v‖ = 1 ∧
(∀ i, 0 < v i) ∧
A.mulVec v = ρ • v ∧
rayleighForm A v = ρ ∧
ρ = sphereRayleighValue A ∧
ρ = coordinateSphereRayleighValue A ∧
ρ = iSupRayleighValue A := by
obtain ⟨x, hx_norm, hx_eigen, hx_top⟩ :=
exists_unit_eigenvector_sphereRayleighValue A hA_symm
obtain ⟨habs_norm, habs_nonneg, habs_top, habs_eigen⟩ :=
absVec_preserves_top_eigenvector A hA_symm hA_irred.nonneg
hx_norm hx_eigen hx_top
refine ⟨absVec x, sphereRayleighValue A, habs_norm, ?_, habs_eigen,
habs_top, rfl, ?_, ?_⟩
· exact IsIrreducible.unit_eigenvector_pos hA_irred
habs_nonneg habs_norm habs_eigen
· exact (coordinateSphereRayleighValue_eq_sphereRayleighValue A).symm
· exact sphereRayleighValue_eq_iSupRayleighValue A
1 supporting declaration (lemmas, instances)
-
finite_positive_perron_eigenvector_on_restrictiontheorem — A symmetric finite matrix, a nonempty finite coordinate set, an irreducible restricted block, and block closure from outside rows into that set ensure that the block’s strictly positive unit Perron vector zero-extends to a global eigenvector.hypothesesι :sharedType u_1A :Matrix ι ι ℝhA_symm :A.IsSymms :Finset ιNonempty shA_irred :(restrictMatrix A s).IsIrreduciblehclosed :∀ i jifi ∉ sandj ∈ sthenA i j = 0conclusion∃ (v : EVec s) (ρ : ℝ),‖v‖ = 1conclusion 1i :0 < v iconclusion 2(restrictMatrix A s).mulVec v = ρ • vconclusion 3A.mulVec (zeroExtendVec s v) = ρ • zeroExtendVec s vconclusion 4ρ = sphereRayleighValue (restrictMatrix A s)conclusion 5ρ = coordinateSphereRayleighValue (restrictMatrix A s)conclusion 6ρ = iSupRayleighValue (restrictMatrix A s)Proof (Lean source)
theorem finite_positive_perron_eigenvector_on_restriction (A : Matrix ι ι ℝ) (hA_symm : A.IsSymm) (s : Finset ι) [Nonempty s] (hA_irred : (restrictMatrix A s).IsIrreducible) (hclosed : ∀ i j, i ∉ s → j ∈ s → A i j = 0) : ∃ (v : EVec s) (ρ : ℝ), ‖v‖ = 1 ∧ (∀ i, 0 < v i) ∧ (restrictMatrix A s).mulVec v = ρ • v ∧ A.mulVec (zeroExtendVec s v) = ρ • zeroExtendVec s v ∧ ρ = sphereRayleighValue (restrictMatrix A s) ∧ ρ = coordinateSphereRayleighValue (restrictMatrix A s) ∧ ρ = iSupRayleighValue (restrictMatrix A s) := by obtain ⟨v, ρ, hv_norm, hv_pos, hv_eigen, _, hρ_sphere, hρ_coordinate, hρ_iSup⟩ := finite_positive_perron_eigenvector (restrictMatrix A s) (restrictMatrix_isSymm hA_symm s) hA_irred refine ⟨v, ρ, hv_norm, hv_pos, hv_eigen, ?_, hρ_sphere, hρ_coordinate, hρ_iSup⟩ exact zeroExtendVec_eigenvector_of_closed A s hclosed hv_eigen
Positivity 1 core · 2 supporting This file isolates the graph-theoretic step of Perron--Frobenius: a nonzero, coordinatewise-nonnegative eigenvector of an irreducible nonnegative matrix has no zero coordinate. ★ eigenvector_pos
Positivity propagation for irreducible matrices
This file isolates the graph-theoretic step of Perron--Frobenius: a nonzero, coordinatewise-nonnegative eigenvector of an irreducible nonnegative matrix has no zero coordinate. No symmetry assumption is needed for this propagation.
theorem eigenvector_pos reviewed
⚑ flagged
Causalean.Mathlib.LinearAlgebra.FinitePerronFrobeniusPositiveEigenvector.IsIrreducible
An irreducible finite matrix and a nonnegative nonzero eigenvector ensure that every coordinate is strictly positive.
Formal statement
Proof (Lean source)
theorem IsIrreducible.eigenvector_pos
{A : Matrix ι ι ℝ} (hA : A.IsIrreducible)
{x : EVec ι} (hx_nonneg : ∀ i, 0 ≤ x i) (hx_ne : x ≠ 0) {ρ : ℝ}
(hx_eigen : A.mulVec x = ρ • x) :
∀ i, 0 < x i := by
have hpath : ∀ {i j : ι},
@Quiver.Path ι (Matrix.toQuiver A) i j → x i = 0 → x j = 0 := by
intro i j p
induction p with
| nil => exact id
| @cons j k p e ih =>
intro hxi
exact zero_coordinate_propagates_across_positive_entry A hA.nonneg hx_nonneg hx_eigen
(ih hxi) e.down
intro i
by_contra hxi_pos
have hxi : x i = 0 := le_antisymm (le_of_not_gt hxi_pos) (hx_nonneg i)
apply hx_ne
ext j
obtain ⟨p, _⟩ := hA.connected i j
exact hpath p hxi
2 supporting declarations (lemmas, instances)
-
zero_coordinate_propagates_across_positive_entrytheorem — An entrywise nonnegative matrix, a nonnegative eigenvector, a row coordinate where it vanishes, and a strictly positive matrix entry from that row ensure that the eigenvector also vanishes at the entry’s target coordinate.hypothesesι :sharedType u_1A :Matrix ι ι ℝhA_nonneg :∀ i j, 0 ≤ A i jx :EVec ιhx_nonneg :∀ i, 0 ≤ x iρ :ℝhx_eigen :A.mulVec x = ρ • xi j :ιhxi :x i = 0hAij :0 < A i jconclusionx j = 0Proof (Lean source)
theorem zero_coordinate_propagates_across_positive_entry (A : Matrix ι ι ℝ) (hA_nonneg : ∀ i j, 0 ≤ A i j) {x : EVec ι} (hx_nonneg : ∀ i, 0 ≤ x i) {ρ : ℝ} (hx_eigen : A.mulVec x = ρ • x) {i j : ι} (hxi : x i = 0) (hAij : 0 < A i j) : x j = 0 := by have hsum : ∑ k, A i k * x k = 0 := by have hi := congrFun hx_eigen i simpa [mulVec, dotProduct, hxi] using hi have hterm : A i j * x j = 0 := (Finset.sum_eq_zero_iff_of_nonneg (fun k _ => mul_nonneg (hA_nonneg i k) (hx_nonneg k))).mp hsum j (Finset.mem_univ j) exact (mul_eq_zero.mp hterm).resolve_left (ne_of_gt hAij) -
unit_eigenvector_postheorem — An irreducible finite matrix and a normalized nonnegative eigenvector ensure that every coordinate is strictly positive.hypotheseshA :A.IsIrreduciblex :EVec ιhx_nonneg :∀ i, 0 ≤ x ihx_norm :‖x‖ = 1ρ :ℝhx_eigen :A.mulVec x = ρ • xi :conclusion0 < x iProof (Lean source)
theorem IsIrreducible.unit_eigenvector_pos {A : Matrix ι ι ℝ} (hA : A.IsIrreducible) {x : EVec ι} (hx_nonneg : ∀ i, 0 ≤ x i) (hx_norm : ‖x‖ = 1) {ρ : ℝ} (hx_eigen : A.mulVec x = ρ • x) : ∀ i, 0 < x i := by apply eigenvector_pos hA hx_nonneg _ hx_eigen intro hx simp [hx] at hx_norm