HermitianFunctionalCalculus

📁 Source: Mathlib/Analysis/Matrix/HermitianFunctionalCalculus.lean

Statistics

Metric	Count
Definitions cfc, cfcAux	2
Theorems cfcAux_apply, cfcAux_id, cfc_eq, charpoly_cfc_eq, instContinuousFunctionalCalculus, isClosedEmbedding_cfcAux	6
Total	8

Matrix.IsHermitian

Definitions

Name	Category	Theorems
cfc 📖	CompOp	1 math math: cfc_eq
cfcAux 📖	CompOp	3 math math: isClosedEmbedding_cfcAux, cfcAux_apply, cfcAux_id

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cfcAux_apply 📖	mathematical	Matrix.IsHermitian InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField StarRing.toStarAddMonoid RCLike.toStarRing	DFunLike.coe StarAlgHom Real ContinuousMap Set.Elem spectrum Matrix Real.instCommSemiring Matrix.instRing NormedRing.toRing NormedCommRing.toNormedRing Matrix.instAlgebra Ring.toSemiring NormedAlgebra.toAlgebra Real.normedField SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing RCLike.toNormedAlgebra instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace ContinuousMap.instSemiringOfIsTopologicalSemiring Real.semiring IsTopologicalRing.toIsTopologicalSemiring Real.normedCommRing instIsTopologicalRingReal ContinuousMap.algebra Algebra.id ContinuousMap.instStar instStarRingReal instContinuousStarReal Matrix.semiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Matrix.instStar StarAlgHom.instFunLike cfcAux StarAlgEquiv Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Distrib.toMul Matrix.smul Algebra.toSMul Semifield.toCommSemiring CommSemiring.toSemiring StarMul.toInvolutiveStar StarRing.toStarMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain Matrix.instStarRing NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing StarAlgEquiv.instFunLike MonoidHom Submonoid Monoid.toMulOneClass MonoidWithZero.toMonoid Semiring.toMonoidWithZero SetLike.instMembership Submonoid.instSetLike unitary MulOneClass.toMulOne Submonoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid StarAlgEquiv.aut MonoidHom.instFunLike Unitary.conjStarAlgAut eigenvectorUnitary Matrix.diagonal MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass RCLike.ofReal ContinuousMap.instFunLike eigenvalues eigenvalues_mem_spectrum_real	—	IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal
cfcAux_id 📖	mathematical	Matrix.IsHermitian InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField StarRing.toStarAddMonoid RCLike.toStarRing	DFunLike.coe StarAlgHom Real ContinuousMap Set.Elem spectrum Matrix Real.instCommSemiring Matrix.instRing NormedRing.toRing NormedCommRing.toNormedRing Matrix.instAlgebra Ring.toSemiring NormedAlgebra.toAlgebra Real.normedField SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing RCLike.toNormedAlgebra instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace ContinuousMap.instSemiringOfIsTopologicalSemiring Real.semiring IsTopologicalRing.toIsTopologicalSemiring Real.normedCommRing instIsTopologicalRingReal ContinuousMap.algebra Algebra.id ContinuousMap.instStar instStarRingReal instContinuousStarReal Matrix.semiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Matrix.instStar StarAlgHom.instFunLike cfcAux ContinuousMap.restrict ContinuousMap.id	—	IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal IsScalarTower.right Algebra.to_smulCommClass spectral_theorem
cfc_eq 📖	mathematical	Matrix.IsHermitian InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField StarRing.toStarAddMonoid RCLike.toStarRing	cfc Real Matrix IsSelfAdjoint Matrix.instStar Real.instCommSemiring instStarRingReal Real.metricSpace IsTopologicalRing.toIsTopologicalSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace Real.normedCommRing instIsTopologicalRingReal instContinuousStarReal instTopologicalSpaceMatrix SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing Matrix.instRing NormedRing.toRing NormedCommRing.toNormedRing Matrix.instStarRing NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring Matrix.instAlgebra Ring.toSemiring NormedAlgebra.toAlgebra Real.normedField RCLike.toNormedAlgebra instContinuousFunctionalCalculus cfc	—	IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal instContinuousFunctionalCalculus cfcHom_eq_of_continuous_of_map_id Real.instContinuousMapUniqueHom instT2SpaceMatrix TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace Topology.IsClosedEmbedding.continuous isClosedEmbedding_cfcAux cfcAux_id ContinuousOn.restrict continuousOn_iff_continuous_restrict continuous_of_discreteTopology Finite.instDiscreteTopology Subtype.t1Space T5Space.toT1Space OrderTopology.t5Space instOrderTopologyReal Matrix.instFiniteElemRealSpectrum cfc_apply
charpoly_cfc_eq 📖	mathematical	Matrix.IsHermitian InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField StarRing.toStarAddMonoid RCLike.toStarRing	Matrix.charpoly EuclideanDomain.toCommRing Field.toEuclideanDomain NormedField.toField cfc Real Matrix IsSelfAdjoint Matrix.instStar Real.instCommSemiring instStarRingReal Real.metricSpace IsTopologicalRing.toIsTopologicalSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace Real.normedCommRing instIsTopologicalRingReal instContinuousStarReal instTopologicalSpaceMatrix SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing Matrix.instRing NormedRing.toRing NormedCommRing.toNormedRing Matrix.instStarRing NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring Matrix.instAlgebra Ring.toSemiring NormedAlgebra.toAlgebra Real.normedField RCLike.toNormedAlgebra instContinuousFunctionalCalculus Finset.prod Polynomial CommSemiring.toSemiring CommRing.toCommSemiring CommRing.toCommMonoid Polynomial.commRing Finset.univ DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Polynomial.instSub Polynomial.X DFunLike.coe RingHom Semiring.toNonAssocSemiring Polynomial.semiring RingHom.instFunLike Polynomial.C RCLike.ofReal eigenvalues	—	IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal instContinuousFunctionalCalculus cfc_eq cfc.eq_1 Unitary.conjStarAlgAut_apply Matrix.charpoly_mul_comm mul_assoc Matrix.charpoly.congr_simp Unitary.star_mul_self_of_mem one_mul Matrix.charpoly_diagonal Finset.prod_congr
instContinuousFunctionalCalculus 📖	mathematical	—	ContinuousFunctionalCalculus Real Matrix IsSelfAdjoint Matrix.instStar InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField StarRing.toStarAddMonoid RCLike.toStarRing Real.instCommSemiring instStarRingReal Real.metricSpace IsTopologicalRing.toIsTopologicalSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace Real.normedCommRing instIsTopologicalRingReal instContinuousStarReal Matrix.instRing NormedRing.toRing NormedCommRing.toNormedRing Matrix.instStarRing NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring instTopologicalSpaceMatrix SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing Matrix.instAlgebra Ring.toSemiring NormedAlgebra.toAlgebra Real.normedField RCLike.toNormedAlgebra	—	IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal IsSelfAdjoint.zero TopologicalSpace.NoetherianSpace.compactSpace TopologicalSpace.Finite.to_noetherianSpace Matrix.instFiniteElemRealSpectrum isEmpty_or_nonempty exists_pair_ne Equiv.injective Unique.instSubsingleton Set.range_nonempty spectrum_real_eq_range_eigenvalues isClosedEmbedding_cfcAux cfcAux_id Set.eq_of_subset_of_subset IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing ContinuousMap.spectrum_eq_range Real.instCompleteSpace AlgHom.spectrum_apply_subset StarAlgHom.instAlgHomClass eigenvalues_mem_spectrum_real cfcAux_apply Unitary.conjStarAlgAut_apply Unitary.spectrum_star_right_conjugate spectrum.of_algebraMap_mem Matrix.isScalarTower IsScalarTower.right spectrum_diagonal NonUnitalStarRingHomClass.toStarHomClass NonUnitalAlgHomClass.toNonUnitalRingHomClass instNonUnitalAlgHomClassOfNonUnitalAlgEquivClass StarAlgEquiv.instNonUnitalAlgEquivClass NonUnitalStarAlgHomClass.instNonUnitalStarRingHomClassOfStarHomClass RingEquivClass.toNonUnitalRingHomClass NonUnitalAlgEquivClass.toRingEquivClass StarRingEquivClass.instNonUnitalStarRingHomClass StarAlgEquiv.instStarRingEquivClass Matrix.star_eq_conjTranspose Matrix.diagonal_conjTranspose RCLike.conj_ofReal
isClosedEmbedding_cfcAux 📖	mathematical	Matrix.IsHermitian InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField StarRing.toStarAddMonoid RCLike.toStarRing	Topology.IsClosedEmbedding ContinuousMap Set.Elem Real spectrum Matrix Real.instCommSemiring Matrix.instRing NormedRing.toRing NormedCommRing.toNormedRing Matrix.instAlgebra Ring.toSemiring NormedAlgebra.toAlgebra Real.normedField SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing RCLike.toNormedAlgebra instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace ContinuousMap.compactOpen instTopologicalSpaceMatrix SeminormedRing.toPseudoMetricSpace DFunLike.coe StarAlgHom ContinuousMap.instSemiringOfIsTopologicalSemiring Real.semiring IsTopologicalRing.toIsTopologicalSemiring Real.normedCommRing instIsTopologicalRingReal ContinuousMap.algebra Algebra.id ContinuousMap.instStar instStarRingReal instContinuousStarReal Matrix.semiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Matrix.instStar StarAlgHom.instFunLike cfcAux	—	instIsTopologicalAddGroupReal UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul instIsUniformAddGroupReal IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal FiniteDimensional.of_injective IsTopologicalSemiring.toContinuousAdd DFunLike.coe_injective FiniteDimensional.finiteDimensional_pi' Matrix.instFiniteElemRealSpectrum FiniteDimensional.rclike_to_real LinearMap.isClosedEmbedding_of_injective Real.instCompleteSpace ContinuousMap.instIsTopologicalAddGroup ContinuousMap.instContinuousSMul IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology instT2SpaceMatrix TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace instIsTopologicalAddGroupMatrix SeminormedAddCommGroup.toIsTopologicalAddGroup instContinuousSMulMatrix IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul ContinuousMap.instT2Space instContinuousStarReal NonUnitalAlgHomClass.instLinearMapClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass StarAlgHom.instAlgHomClass LinearMap.ker_eq_bot' eigenvalues_mem_spectrum_real Unitary.star_mul_self_of_mem one_mul MulZeroClass.mul_zero mul_assoc mul_one MulZeroClass.zero_mul ContinuousMap.ext spectrum_real_eq_range_eigenvalues Matrix.diagonal_eq_diagonal_iff Matrix.diagonal_zero RCLike.ofReal_eq_zero

---

← Back to Index