Spectrum

📁 Source: Mathlib/Analysis/InnerProductSpace/Spectrum.lean

Statistics

Metric	Count
Definitions diagonalization, directSumDecomposition, eigenvalues, eigenvectorBasis	4
Theorems apply_eigenvectorBasis, card_filter_eigenvalues_eq, conj_eigenvalue_eq_self, diagonalization_apply_self_apply, diagonalization_symm_apply, directSum_decompose_apply, direct_sum_isInternal, eigenvalues_antitone, eigenvalues_def, eigenvectorBasis_apply_self_apply, eigenvectorBasis_def, exists_eigenvalues_eq, hasEigenvalue_eigenvalues, hasEigenvector_eigenvectorBasis, invariant_orthogonalComplement_eigenspace, orthogonalComplement_iSup_eigenspaces, orthogonalComplement_iSup_eigenspaces_eq_bot, orthogonalComplement_iSup_eigenspaces_eq_bot', orthogonalComplement_iSup_eigenspaces_invariant, orthogonalFamily_eigenspaces, orthogonalFamily_eigenspaces', eigenvalue_nonneg_of_nonneg, eigenvalue_pos_of_pos, inner_product_apply_eigenvector	24
Total	28

LinearMap.IsSymmetric

Definitions

Name	Category	Theorems
diagonalization 📖	CompOp	2 math math: diagonalization_apply_self_apply, diagonalization_symm_apply
directSumDecomposition 📖	CompOp	1 math math: directSum_decompose_apply
eigenvalues 📖	CompOp	11 math math: LinearMap.IsPositive.nonneg_eigenvalues, card_filter_eigenvalues_eq, hasEigenvalue_eigenvalues, eigenvectorBasis_apply_self_apply, apply_eigenvectorBasis, eigenvalues_def, trace_eq_sum_eigenvalues, exists_eigenvalues_eq, re_trace_eq_sum_eigenvalues, hasEigenvector_eigenvectorBasis, eigenvalues_antitone
eigenvectorBasis 📖	CompOp	4 math math: eigenvectorBasis_apply_self_apply, apply_eigenvectorBasis, hasEigenvector_eigenvectorBasis, eigenvectorBasis_def

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
apply_eigenvectorBasis 📖	mathematical	LinearMap.IsSymmetric NormedAddCommGroup.toSeminormedAddCommGroup Module.finrank DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike OrthonormalBasis Fin.fintype OrthonormalBasis.instFunLike eigenvectorBasis SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction RCLike.ofReal eigenvalues	—	Module.End.mem_eigenspace_iff hasEigenvector_eigenvectorBasis
card_filter_eigenvalues_eq 📖	mathematical	LinearMap.IsSymmetric NormedAddCommGroup.toSeminormedAddCommGroup Module.finrank DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace Module.End.HasEigenvalue EuclideanDomain.toCommRing Field.toEuclideanDomain SeminormedAddCommGroup.toAddCommGroup	Finset.card Finset.filter RCLike.ofReal eigenvalues RCLike.toDecidableEq Finset.univ Fin.fintype Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike Module.End.eigenspace Submodule.addCommMonoid Submodule.module	—	eigenvalues_def Finset.card_equiv
conj_eigenvalue_eq_self 📖	mathematical	LinearMap.IsSymmetric NormedAddCommGroup.toSeminormedAddCommGroup Module.End.HasEigenvalue EuclideanDomain.toCommRing Field.toEuclideanDomain NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule InnerProductSpace.toNormedSpace	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield RingHom.instFunLike starRingEnd RCLike.toStarRing	—	Module.End.HasEigenvalue.exists_hasEigenvector Module.End.mem_eigenspace_iff inner_smul_left inner_self_eq_norm_sq_to_K inner_smul_right IsCancelMulZero.toIsRightCancelMulZero IsDomain.toIsCancelMulZero instIsDomain isReduced_of_noZeroDivisors NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass Nat.instCharZero Nat.instAtLeastTwoHAddOfNat IsLocalRing.toNontrivial Field.instIsLocalRing RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass
diagonalization_apply_self_apply 📖	mathematical	LinearMap.IsSymmetric NormedAddCommGroup.toSeminormedAddCommGroup	WithLp.ofLp ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Nat.instAtLeastTwoHAddOfNat DFunLike.coe LinearIsometryEquiv DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids PiLp Module.End.Eigenvalues EuclideanDomain.toCommRing Field.toEuclideanDomain SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule InnerProductSpace.toNormedSpace Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike Module.End.eigenspace Module.End.UnifEigenvalues.val ENat AddMonoidWithOne.toOne NonAssocSemiring.toAddCommMonoidWithOne instCommSemiringENat PiLp.seminormedAddCommGroup fact_one_le_two_ennreal Module.End.instFintypeEigenvalues instIsDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors DivisionSemiring.toGroupWithZero SubNegMonoid.toAddMonoid SubNegZeroMonoid.toSubNegMonoid SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Module.toDistribMulAction Submodule.seminormedAddCommGroup NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing WithLp.instModule Pi.addCommGroup Pi.module Submodule.addCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Submodule.module EquivLike.toFunLike LinearIsometryEquiv.instEquivLike diagonalization LinearMap LinearMap.instFunLike Submodule.smul Algebra.toSMul Semifield.toCommSemiring Algebra.id SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero IsScalarTower.left DistribMulAction.toMulAction AddCommMonoid.toAddMonoid	—	Nat.instAtLeastTwoHAddOfNat RingHomInvPair.ids fact_one_le_two_ennreal instIsDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors IsScalarTower.left Module.End.mem_eigenspace_iff diagonalization_symm_apply Finset.sum_congr map_sum DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass LinearIsometryEquiv.symm_apply_apply LinearIsometryEquiv.apply_symm_apply
diagonalization_symm_apply 📖	mathematical	LinearMap.IsSymmetric NormedAddCommGroup.toSeminormedAddCommGroup	DFunLike.coe LinearIsometryEquiv DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids PiLp ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Nat.instAtLeastTwoHAddOfNat Module.End.Eigenvalues EuclideanDomain.toCommRing Field.toEuclideanDomain SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule InnerProductSpace.toNormedSpace Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike Module.End.eigenspace Module.End.UnifEigenvalues.val ENat AddMonoidWithOne.toOne NonAssocSemiring.toAddCommMonoidWithOne instCommSemiringENat PiLp.seminormedAddCommGroup fact_one_le_two_ennreal Module.End.instFintypeEigenvalues instIsDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors DivisionSemiring.toGroupWithZero SubNegMonoid.toAddMonoid SubNegZeroMonoid.toSubNegMonoid SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Module.toDistribMulAction Submodule.seminormedAddCommGroup NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing WithLp.instModule Pi.addCommGroup Pi.module Submodule.addCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Submodule.module EquivLike.toFunLike LinearIsometryEquiv.instEquivLike LinearIsometryEquiv.symm diagonalization Finset.sum Finset.univ WithLp.ofLp	—	Nat.instAtLeastTwoHAddOfNat DirectSum.IsInternal.isometryL2OfOrthogonalFamily_symm_apply instIsDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors direct_sum_isInternal orthogonalFamily_eigenspaces'
directSum_decompose_apply 📖	mathematical	—	DFunLike.coe DFinsupp Module.End.Eigenvalues EuclideanDomain.toCommRing Field.toEuclideanDomain NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule InnerProductSpace.toNormedSpace AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike Module.End.eigenspace Module.End.UnifEigenvalues.val ENat AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring instCommSemiringENat DFinsupp.instDFunLike Equiv DirectSum AddSubmonoidClass.toAddCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Submodule.addSubmonoidClass EquivLike.toFunLike Equiv.instEquivLike DirectSum.decompose Module.End.UnivEigenvalues.instDecidableEq NormedAddCommGroup.toAddCommGroup RCLike.toDecidableEq directSumDecomposition ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.id instTopologicalSpaceSubtype Submodule.addCommMonoid Submodule.module ContinuousLinearMap.funLike Submodule.orthogonalProjection Submodule.HasOrthogonalProjection.ofCompleteSpace complete_of_proper Subtype.pseudoMetricSpace FiniteDimensional.RCLike.properSpace_submodule FiniteDimensional.finiteDimensional_submodule NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing	—	Submodule.addSubmonoidClass
direct_sum_isInternal 📖	mathematical	LinearMap.IsSymmetric NormedAddCommGroup.toSeminormedAddCommGroup	DirectSum.IsInternal Module.End.Eigenvalues EuclideanDomain.toCommRing Field.toEuclideanDomain NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule InnerProductSpace.toNormedSpace Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Module.End.UnivEigenvalues.instDecidableEq NormedAddCommGroup.toAddCommGroup RCLike.toDecidableEq ENat AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring instCommSemiringENat ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Submodule.setLike Submodule.addSubmonoidClass Module.End.eigenspace Module.End.UnifEigenvalues.val	—	Submodule.addSubmonoidClass OrthogonalFamily.isInternal_iff orthogonalFamily_eigenspaces' orthogonalComplement_iSup_eigenspaces_eq_bot'
eigenvalues_antitone 📖	mathematical	LinearMap.IsSymmetric NormedAddCommGroup.toSeminormedAddCommGroup Module.finrank DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace	Antitone Real PartialOrder.toPreorder Fin.instPartialOrder Real.instPreorder eigenvalues	—	eigenvalues_def Function.comp_assoc Monotone.comp_antitone Tuple.monotone_sort
eigenvalues_def 📖	mathematical	LinearMap.IsSymmetric NormedAddCommGroup.toSeminormedAddCommGroup Module.finrank DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace	eigenvalues Real DFunLike.coe Equiv.Perm EquivLike.toFunLike Equiv.instEquivLike Tuple.sort Real.linearOrder Fin.revPerm	—	—
eigenvectorBasis_apply_self_apply 📖	mathematical	LinearMap.IsSymmetric NormedAddCommGroup.toSeminormedAddCommGroup Module.finrank DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace	WithLp.ofLp ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal DFunLike.coe LinearIsometryEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids EuclideanSpace PiLp.seminormedAddCommGroup fact_one_le_two_ennreal Fin.fintype NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing WithLp.instModule Pi.addCommGroup SeminormedAddCommGroup.toAddCommGroup Pi.Function.module NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring SeminormedRing.toRing SeminormedCommRing.toSeminormedRing RCLike.innerProductSpace EquivLike.toFunLike LinearIsometryEquiv.instEquivLike OrthonormalBasis.repr eigenvectorBasis LinearMap LinearMap.instFunLike Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing RCLike.ofReal eigenvalues	—	RingHomInvPair.ids fact_one_le_two_ennreal Nat.instAtLeastTwoHAddOfNat Finset.sum_congr map_sum DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass map_smul SemilinearMapClass.toMulActionSemiHomClass apply_eigenvectorBasis Fintype.sum_congr smul_smul mul_comm WithLp.ofLp_toLp LinearIsometryEquiv.symm_apply_apply LinearIsometryEquiv.apply_symm_apply
eigenvectorBasis_def 📖	mathematical	LinearMap.IsSymmetric NormedAddCommGroup.toSeminormedAddCommGroup Module.finrank DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace	eigenvectorBasis OrthonormalBasis.reindex Fin.fintype DirectSum.IsInternal.subordinateOrthonormalBasis Module.End.Eigenvalues EuclideanDomain.toCommRing Field.toEuclideanDomain SeminormedAddCommGroup.toAddCommGroup Module.End.instFintypeEigenvalues Module.End.UnivEigenvalues.instDecidableEq NormedAddCommGroup.toAddCommGroup RCLike.toDecidableEq ENat AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat Module.End.eigenspace Module.End.UnifEigenvalues.val direct_sum_isInternal orthogonalFamily_eigenspaces' Equiv.symm Equiv.Perm Equiv.Perm.instMul Tuple.sort Real Real.linearOrder Fin.revPerm	—	direct_sum_isInternal orthogonalFamily_eigenspaces'
exists_eigenvalues_eq 📖	mathematical	LinearMap.IsSymmetric NormedAddCommGroup.toSeminormedAddCommGroup Module.finrank DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace Module.End.HasEigenvalue EuclideanDomain.toCommRing Field.toEuclideanDomain SeminormedAddCommGroup.toAddCommGroup	RCLike.ofReal eigenvalues	—	eigenvalues_def Equiv.apply_symm_apply
hasEigenvalue_eigenvalues 📖	mathematical	LinearMap.IsSymmetric NormedAddCommGroup.toSeminormedAddCommGroup Module.finrank DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace	Module.End.HasEigenvalue EuclideanDomain.toCommRing Field.toEuclideanDomain SeminormedAddCommGroup.toAddCommGroup RCLike.ofReal eigenvalues	—	Module.End.hasEigenvalue_of_hasEigenvector hasEigenvector_eigenvectorBasis
hasEigenvector_eigenvectorBasis 📖	mathematical	LinearMap.IsSymmetric NormedAddCommGroup.toSeminormedAddCommGroup Module.finrank DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace	Module.End.HasEigenvector EuclideanDomain.toCommRing Field.toEuclideanDomain SeminormedAddCommGroup.toAddCommGroup RCLike.ofReal eigenvalues DFunLike.coe OrthonormalBasis Fin.fintype OrthonormalBasis.instFunLike eigenvectorBasis	—	eigenvalues_def direct_sum_isInternal orthogonalFamily_eigenspaces' eigenvectorBasis_def OrthonormalBasis.reindex_apply
invariant_orthogonalComplement_eigenspace 📖	mathematical	LinearMap.IsSymmetric NormedAddCommGroup.toSeminormedAddCommGroup Submodule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace SetLike.instMembership Submodule.setLike Submodule.orthogonal Module.End.eigenspace Field.toCommRing SeminormedAddCommGroup.toAddCommGroup	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike	—	Module.End.mem_eigenspace_iff inner_smul_left MulZeroClass.mul_zero
orthogonalComplement_iSup_eigenspaces 📖	mathematical	LinearMap.IsSymmetric NormedAddCommGroup.toSeminormedAddCommGroup	Module.End.eigenspace Submodule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace SetLike.instMembership Submodule.setLike Submodule.orthogonal iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice Field.toCommRing SeminormedAddCommGroup.toAddCommGroup EuclideanDomain.toCommRing Field.toEuclideanDomain Submodule.addCommGroup NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing Submodule.module LinearMap.restrict orthogonalComplement_iSup_eigenspaces_invariant Bot.bot CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Submodule.instBot	—	Module.End.eigenspace_restrict_eq_bot orthogonalComplement_iSup_eigenspaces_invariant Submodule.IsOrtho.mono_left le_iSup Submodule.isOrtho_orthogonal_right Submodule.IsOrtho.disjoint
orthogonalComplement_iSup_eigenspaces_eq_bot 📖	mathematical	LinearMap.IsSymmetric NormedAddCommGroup.toSeminormedAddCommGroup	Submodule.orthogonal iSup Submodule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice Module.End.eigenspace Field.toCommRing SeminormedAddCommGroup.toAddCommGroup Bot.bot Submodule.instBot	—	orthogonalComplement_iSup_eigenspaces_invariant restrict_invariant Submodule.eq_bot_of_subsingleton subsingleton_of_no_eigenvalue_finiteDimensional FiniteDimensional.finiteDimensional_submodule orthogonalComplement_iSup_eigenspaces
orthogonalComplement_iSup_eigenspaces_eq_bot' 📖	mathematical	LinearMap.IsSymmetric NormedAddCommGroup.toSeminormedAddCommGroup	Submodule.orthogonal iSup Submodule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace Module.End.Eigenvalues EuclideanDomain.toCommRing Field.toEuclideanDomain SeminormedAddCommGroup.toAddCommGroup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice Module.End.eigenspace Field.toCommRing Module.End.UnifEigenvalues.val ENat AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat Bot.bot Submodule.instBot	—	iSup_ne_bot_subtype orthogonalComplement_iSup_eigenspaces_eq_bot
orthogonalComplement_iSup_eigenspaces_invariant 📖	mathematical	LinearMap.IsSymmetric NormedAddCommGroup.toSeminormedAddCommGroup Submodule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace SetLike.instMembership Submodule.setLike Submodule.orthogonal iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice Module.End.eigenspace Field.toCommRing SeminormedAddCommGroup.toAddCommGroup	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike	—	Submodule.iInf_orthogonal LinearMap.iInf_invariant invariant_orthogonalComplement_eigenspace
orthogonalFamily_eigenspaces 📖	mathematical	LinearMap.IsSymmetric NormedAddCommGroup.toSeminormedAddCommGroup	OrthogonalFamily Submodule CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule InnerProductSpace.toNormedSpace SetLike.instMembership Submodule.setLike Module.End.eigenspace Submodule.seminormedAddCommGroup NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing Submodule.innerProductSpace Submodule.subtypeₗᵢ	—	inner_zero_left conj_eigenvalue_eq_self Module.End.hasEigenvalue_of_hasEigenvector Module.End.mem_eigenspace_iff inner_smul_right inner_smul_left IsCancelMulZero.toIsRightCancelMulZero IsDomain.toIsCancelMulZero instIsDomain
orthogonalFamily_eigenspaces' 📖	mathematical	LinearMap.IsSymmetric NormedAddCommGroup.toSeminormedAddCommGroup	OrthogonalFamily Module.End.Eigenvalues EuclideanDomain.toCommRing Field.toEuclideanDomain NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule InnerProductSpace.toNormedSpace Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike Module.End.eigenspace Module.End.UnifEigenvalues.val ENat AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring instCommSemiringENat Submodule.seminormedAddCommGroup NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing Submodule.innerProductSpace Submodule.subtypeₗᵢ	—	OrthogonalFamily.comp orthogonalFamily_eigenspaces Subtype.coe_injective

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eigenvalue_nonneg_of_nonneg 📖	—	Module.End.HasEigenvalue EuclideanDomain.toCommRing Field.toEuclideanDomain NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule InnerProductSpace.toNormedSpace RCLike.ofReal Real Real.instLE Real.instZero DFunLike.coe AddMonoidHom AddMonoid.toZero AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring CommRing.toRing Field.toCommRing AddSemigroup.toAdd AddMonoid.toAddSemigroup AddZeroClass.toAddZero AddMonoid.toAddZeroClass Real.instAddMonoid AddMonoidHom.instFunLike RCLike.re Inner.inner InnerProductSpace.toInner LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid LinearMap.instFunLike	—	—	Module.End.HasEigenvalue.exists_hasEigenvector Real.instIsStrictOrderedRing AddGroup.existsAddOfLE RCLike.ofReal_re inner_product_apply_eigenvector mul_nonneg_iff_of_pos_right IsStrictOrderedRing.toMulPosStrictMono
eigenvalue_pos_of_pos 📖	—	Module.End.HasEigenvalue EuclideanDomain.toCommRing Field.toEuclideanDomain NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule InnerProductSpace.toNormedSpace RCLike.ofReal Real Real.instLT Real.instZero DFunLike.coe AddMonoidHom AddMonoid.toZero AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring CommRing.toRing Field.toCommRing AddSemigroup.toAdd AddMonoid.toAddSemigroup AddZeroClass.toAddZero AddMonoid.toAddZeroClass Real.instAddMonoid AddMonoidHom.instFunLike RCLike.re Inner.inner InnerProductSpace.toInner LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid LinearMap.instFunLike	—	—	Module.End.HasEigenvalue.exists_hasEigenvector Real.instIsStrictOrderedRing AddGroup.existsAddOfLE RCLike.ofReal_re inner_product_apply_eigenvector mul_pos_iff_of_pos_right IsStrictOrderedRing.toMulPosStrictMono MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE
inner_product_apply_eigenvector 📖	mathematical	DFunLike.coe LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace LinearMap.instFunLike SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	Inner.inner InnerProductSpace.toInner Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing Monoid.toNatPow RCLike.ofReal Norm.norm NormedAddCommGroup.toNorm	—	inner_smul_right inner_self_eq_norm_sq_to_K

---

← Back to Index