Perron eigenvectors of finite nonnegative symmetric matrices

The finite matrix argument is shared by the binary, Johnson, spherical, and higher-hierarchy bounds. It requires no coding-theory definitions. Positivity is propagated along the quiver of positive matrix entries, allowing arbitrary finite index sets rather than just tridiagonal grids.

@[reducible, inline]

abbrev MetricCodes.Spherical.HigherHierarchyFinitePerron.Space (I : Type u_2) : Type u_2

Euclidean space on the matrix index set.

Equations

• MetricCodes.Spherical.HigherHierarchyFinitePerron.Space I = EuclideanSpace ℝ I

structure MetricCodes.Spherical.HigherHierarchyFinitePerron.ConnectedNonnegativeMatrix {I : Type u_1} (A : Matrix I I ℝ) : Prop

A nonnegative matrix whose positive-entry quiver is strongly connected.

• nonneg (i j : I) : 0 ≤ A i j
• connected : Quiver.IsSStronglyConnected I

noncomputable def MetricCodes.Spherical.HigherHierarchyFinitePerron.operator {I : Type u_1} [Fintype I] [DecidableEq I] (A : Matrix I I ℝ) : Space I →ₗ[ℝ] Space I

The linear operator associated to a real matrix.

Equations

• MetricCodes.Spherical.HigherHierarchyFinitePerron.operator A = Matrix.toEuclideanLin A

noncomputable def MetricCodes.Spherical.HigherHierarchyFinitePerron.continuousOperator {I : Type u_1} [Fintype I] [DecidableEq I] (A : Matrix I I ℝ) : Space I →L[ℝ] Space I

The continuous linear operator associated to a finite real matrix.

Equations

• MetricCodes.Spherical.HigherHierarchyFinitePerron.continuousOperator A = LinearMap.toContinuousLinearMap (MetricCodes.Spherical.HigherHierarchyFinitePerron.operator A)

noncomputable def MetricCodes.Spherical.HigherHierarchyFinitePerron.rayleigh {I : Type u_1} [Fintype I] [DecidableEq I] (A : Matrix I I ℝ) (x : Space I) : ℝ

The Rayleigh quotient of the matrix operator.

Equations

• MetricCodes.Spherical.HigherHierarchyFinitePerron.rayleigh A x = (MetricCodes.Spherical.HigherHierarchyFinitePerron.continuousOperator A).rayleighQuotient x

theorem MetricCodes.Spherical.HigherHierarchyFinitePerron.rayleigh_bddAbove {I : Type u_1} [Fintype I] [DecidableEq I] (A : Matrix I I ℝ) : BddAbove (Set.range fun (x : { x : Space I // x ≠ 0 }) => rayleigh A ↑x)

noncomputable def MetricCodes.Spherical.HigherHierarchyFinitePerron.topEigenvalue {I : Type u_1} [Fintype I] [DecidableEq I] (A : Matrix I I ℝ) : ℝ

The supremum of the Rayleigh quotient over nonzero vectors.

Equations

• One or more equations did not get rendered due to their size.

theorem MetricCodes.Spherical.HigherHierarchyFinitePerron.rayleigh_le_top {I : Type u_1} [Fintype I] [DecidableEq I] (A : Matrix I I ℝ) (x : Space I) (hx : x ≠ 0) : rayleigh A x ≤ topEigenvalue A

theorem MetricCodes.Spherical.HigherHierarchyFinitePerron.operator_isSymmetric {I : Type u_1} [Fintype I] [DecidableEq I] (A : Matrix I I ℝ) (hA : A.transpose = A) : (operator A).IsSymmetric

theorem MetricCodes.Spherical.HigherHierarchyFinitePerron.exists_topEigenvector {I : Type u_1} [Fintype I] [DecidableEq I] [Nonempty I] (A : Matrix I I ℝ) (hA : A.transpose = A) : ∃ (x : Space I), x ≠ 0 ∧ (operator A) x = topEigenvalue A • x

def MetricCodes.Spherical.HigherHierarchyFinitePerron.coordinateAbs {I : Type u_1} (x : Space I) : Space I

Take the absolute value of each coordinate.

Equations

• MetricCodes.Spherical.HigherHierarchyFinitePerron.coordinateAbs x = WithLp.toLp 2 fun (i : I) => |x.ofLp i|

theorem MetricCodes.Spherical.HigherHierarchyFinitePerron.coordinateAbs_norm {I : Type u_1} [Fintype I] (x : Space I) : ‖coordinateAbs x‖ = ‖x‖

theorem MetricCodes.Spherical.HigherHierarchyFinitePerron.coordinateAbs_ne_zero {I : Type u_1} {x : Space I} (hx : x ≠ 0) : coordinateAbs x ≠ 0

theorem MetricCodes.Spherical.HigherHierarchyFinitePerron.inner_le_inner_coordinateAbs {I : Type u_1} [Fintype I] [DecidableEq I] (A : Matrix I I ℝ) (hA : ∀ (i j : I), 0 ≤ A i j) (x : Space I) : inner ℝ ((operator A) x) x ≤ inner ℝ ((operator A) (coordinateAbs x)) (coordinateAbs x)

theorem MetricCodes.Spherical.HigherHierarchyFinitePerron.rayleigh_eq_of_eigenvector {I : Type u_1} [Fintype I] [DecidableEq I] (A : Matrix I I ℝ) (x : Space I) (hx : x ≠ 0) (eigenvalue : ℝ) (heig : (operator A) x = eigenvalue • x) : rayleigh A x = eigenvalue

theorem MetricCodes.Spherical.HigherHierarchyFinitePerron.rayleigh_le_coordinateAbs {I : Type u_1} [Fintype I] [DecidableEq I] (A : Matrix I I ℝ) (hA : ∀ (i j : I), 0 ≤ A i j) (x : Space I) : rayleigh A x ≤ rayleigh A (coordinateAbs x)

theorem MetricCodes.Spherical.HigherHierarchyFinitePerron.exists_nonnegative_topEigenvector {I : Type u_1} [Fintype I] [DecidableEq I] [Nonempty I] (A : Matrix I I ℝ) (hsymm : A.transpose = A) (hnonneg : ∀ (i j : I), 0 ≤ A i j) : ∃ (x : Space I), x ≠ 0 ∧ (operator A) x = topEigenvalue A • x ∧ ∀ (i : I), 0 ≤ x.ofLp i

theorem MetricCodes.Spherical.HigherHierarchyFinitePerron.exists_nonnegative_unit_topEigenvector {I : Type u_1} [Fintype I] [DecidableEq I] [Nonempty I] (A : Matrix I I ℝ) (hsymm : A.transpose = A) (hnonneg : ∀ (i j : I), 0 ≤ A i j) : ∃ (x : Space I), ‖x‖ = 1 ∧ (operator A) x = topEigenvalue A • x ∧ ∀ (i : I), 0 ≤ x.ofLp i

A finite nonnegative symmetric matrix has a unit nonnegative vector for its top eigenvalue.

theorem MetricCodes.Spherical.HigherHierarchyFinitePerron.eigenvector_zero_of_positive_edge {I : Type u_1} [Fintype I] [DecidableEq I] (A : Matrix I I ℝ) (hnonneg : ∀ (i j : I), 0 ≤ A i j) (x : Space I) (hx : ∀ (i : I), 0 ≤ x.ofLp i) (eigenvalue : ℝ) (heig : (operator A) x = eigenvalue • x) {i j : I} (hzero : x.ofLp i = 0) (hedge : 0 < A i j) : x.ofLp j = 0

theorem MetricCodes.Spherical.HigherHierarchyFinitePerron.eigenvector_zero_of_positive_path {I : Type u_1} [Fintype I] [DecidableEq I] (A : Matrix I I ℝ) (hnonneg : ∀ (i j : I), 0 ≤ A i j) (x : Space I) (hx : ∀ (i : I), 0 ≤ x.ofLp i) (eigenvalue : ℝ) (heig : (operator A) x = eigenvalue • x) {i j : I} (p : Quiver.Path i j) (hzero : x.ofLp i = 0) : x.ofLp j = 0

theorem MetricCodes.Spherical.HigherHierarchyFinitePerron.eigenvector_pos_of_irreducible {I : Type u_1} [Fintype I] [DecidableEq I] (A : Matrix I I ℝ) (hirreducible : ConnectedNonnegativeMatrix A) (x : Space I) (hxzero : x ≠ 0) (hx : ∀ (i : I), 0 ≤ x.ofLp i) (eigenvalue : ℝ) (heig : (operator A) x = eigenvalue • x) (i : I) : 0 < x.ofLp i

theorem MetricCodes.Spherical.HigherHierarchyFinitePerron.exists_positive_topEigenvector {I : Type u_1} [Fintype I] [DecidableEq I] [Nonempty I] (A : Matrix I I ℝ) (hsymm : A.transpose = A) (hirreducible : ConnectedNonnegativeMatrix A) : ∃ (x : Space I), x ≠ 0 ∧ (operator A) x = topEigenvalue A • x ∧ ∀ (i : I), 0 < x.ofLp i

theorem MetricCodes.Spherical.HigherHierarchyFinitePerron.exists_positive_unit_topEigenvector {I : Type u_1} [Fintype I] [DecidableEq I] [Nonempty I] (A : Matrix I I ℝ) (hsymm : A.transpose = A) (hirreducible : ConnectedNonnegativeMatrix A) : ∃ (x : Space I), ‖x‖ = 1 ∧ (operator A) x = topEigenvalue A • x ∧ ∀ (i : I), 0 < x.ofLp i

theorem MetricCodes.Spherical.HigherHierarchyFinitePerron.unit_coordinate_sq_sum {I : Type u_1} [Fintype I] {x : Space I} (hx : ‖x‖ = 1) : ∑ i : I, x.ofLp i ^ 2 = 1

theorem MetricCodes.Spherical.HigherHierarchyFinitePerron.exists_positive_unit_topEigenpair {I : Type u_1} [Fintype I] [DecidableEq I] [Nonempty I] (A : Matrix I I ℝ) (hsymm : A.transpose = A) (hirreducible : ConnectedNonnegativeMatrix A) : ∃ (x : I → ℝ), (∀ (i : I), 0 < x i) ∧ ∑ i : I, x i ^ 2 = 1 ∧ ∀ (i : I), ∑ j : I, A i j * x j = topEigenvalue A * x i