Spectrum

📁 Source: Mathlib/Analysis/Normed/Algebra/Spectrum.lean

Statistics

Metric	Count
Definitions toContinuousLinearMap, equivAlgHom, spectralRadius	3
Theorems coe_toContinuousLinearMap, instContinuousLinearMapClassOfAlgHomClass, norm_apply_le_self, norm_apply_le_self_mul_norm_one, toContinuousLinearMap_norm, spectralRadius_mem_spectrum, compactSpace, spectralRadius_mem_spectrum, spectralRadius_mem_spectrum_or, nnreal_iff_spectralRadius_le, spectralRadius_eq, frontier_spectrum, frontier_subset_frontier, isUnit_of_isUnit_val_of_eventually, spectrum_eq_of_isPreconnected_compl, spectrum_isBounded_connectedComponentIn, spectrum_sUnion_connectedComponentIn, equivAlgHom_coe, equivAlgHom_symm_coe, instCompactSpace, instCompactSpaceNNReal, isCompact, isCompact_nnreal, of_subsingleton, coe_le_norm_of_mem, eventually_isUnit_resolvent, exists_nnnorm_eq_spectralRadius_of_nonempty, exp_mem_exp, hasFPowerSeriesOnBall_inverse_one_sub_smul, instCompactSpace, instCompactSpaceNNReal, isBounded, isClosed, isCompact, isCompact_nnreal, isOpen_resolventSet, isUnit_one_sub_smul_of_lt_inv_radius, le_nnnorm_of_mem, mem_resolventSet_of_norm_lt, mem_resolventSet_of_norm_lt_mul, mem_resolventSet_of_spectralRadius_lt, norm_le_norm_mul_of_mem, norm_le_norm_of_mem, resolvent_isBigO_inv, resolvent_tendsto_cobounded, spectralRadius_le_liminf_pow_nnnorm_pow_one_div, spectralRadius_le_nnnorm, spectralRadius_le_pow_nnnorm_pow_one_div, spectralRadius_lt_of_forall_lt_of_nonempty, spectralRadius_one, spectralRadius_pow_le, spectralRadius_pow_le', spectralRadius_zero, subset_closedBall_norm, subset_closedBall_norm_mul, upperHemicontinuous_quasispectrum, upperHemicontinuous_quasispectrum_nnreal, upperHemicontinuous_spectrum, upperHemicontinuous_spectrum_nnreal	59
Total	62

AlgHom

Definitions

Name	Category	Theorems
toContinuousLinearMap 📖	CompOp	2 math math: coe_toContinuousLinearMap, toContinuousLinearMap_norm

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_toContinuousLinearMap 📖	mathematical	—	DFunLike.coe StrongDual DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NormedRing.toSeminormedRing ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing NormedAlgebra.toNormedSpace ContinuousLinearMap.funLike RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule toContinuousLinearMap AlgHom Semifield.toCommSemiring Ring.toSemiring NormedRing.toRing NormedAlgebra.toAlgebra Algebra.id funLike	—	—
instContinuousLinearMapClassOfAlgHomClass 📖	mathematical	—	ContinuousLinearMapClass DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing NormedAlgebra.toNormedSpace NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedField.toNormedSpace	—	AlgHomClass.linearMapClass AddMonoidHomClass.continuous_of_bound DistribMulActionSemiHomClass.toAddMonoidHomClass NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass instNonUnitalAlgHomClassOfAlgHomClass spectrum.norm_le_norm_mul_of_mem apply_mem_spectrum IsLocalRing.toNontrivial Field.instIsLocalRing mul_comm
norm_apply_le_self 📖	mathematical	—	Real Real.instLE Norm.norm NormedField.toNorm DFunLike.coe NormedRing.toNorm	—	spectrum.norm_le_norm_of_mem apply_mem_spectrum IsLocalRing.toNontrivial Field.instIsLocalRing
norm_apply_le_self_mul_norm_one 📖	mathematical	—	Real Real.instLE Norm.norm NormedField.toNorm DFunLike.coe Real.instMul NormedRing.toNorm AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedRing.toRing	—	spectrum.norm_le_norm_mul_of_mem apply_mem_spectrum IsLocalRing.toNontrivial Field.instIsLocalRing
toContinuousLinearMap_norm 📖	mathematical	—	Norm.norm StrongDual DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NormedRing.toSeminormedRing ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing NormedAlgebra.toNormedSpace ContinuousLinearMap.hasOpNorm NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedField.toNormedSpace RingHom.id Semiring.toNonAssocSemiring toContinuousLinearMap Real Real.instOne	—	ContinuousLinearMap.opNorm_eq_of_bounds zero_le_one Real.instZeroLEOneClass spectrum.norm_le_norm_of_mem apply_mem_spectrum algHomClass IsLocalRing.toNontrivial Field.instIsLocalRing one_mul map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass NormOneClass.norm_one NormedDivisionRing.to_normOneClass mul_one

NNReal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
spectralRadius_mem_spectrum 📖	mathematical	Set.Nonempty Real spectrum Real.instCommSemiring NormedRing.toRing NormedAlgebra.toAlgebra Real.normedField NormedRing.toSeminormedRing SpectrumRestricts NNReal instSemifield Field.toSemifield Real.instField instAlgebraOfReal Ring.toSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Algebra.id DFunLike.coe ContinuousMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace instTopologicalSpace ContinuousMap.instFunLike ContinuousMap.realToNNReal	Set Set.instMembership instCommSemiringNNReal ENNReal.toNNReal spectralRadius	—	spectrum.exists_nnnorm_eq_spectralRadius_of_nonempty instProperSpaceReal ENNReal.toNNReal_coe spectrum.algebraMap_mem_iff instIsScalarTowerOfReal IsScalarTower.left algebraMap_eq_coe zero_le_coe SpectrumRestricts.rightInvOn Real.instIsOrderedAddMonoid

QuasispectrumRestricts

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
compactSpace 📖	mathematical	QuasispectrumRestricts Semifield.toCommSemiring Field.toSemifield DFunLike.coe ContinuousMap ContinuousMap.instFunLike	CompactSpace Set.Elem quasispectrum instTopologicalSpaceSubtype Set Set.instMembership	—	isCompact_iff_compactSpace IsCompact.image ContinuousMapClass.map_continuous ContinuousMap.instContinuousMapClass image

Real

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
spectralRadius_mem_spectrum 📖	mathematical	Set.Nonempty Real spectrum instCommSemiring NormedRing.toRing NormedAlgebra.toAlgebra normedField NormedRing.toSeminormedRing SpectrumRestricts NNReal NNReal.instSemifield Field.toSemifield instField NNReal.instAlgebraOfReal Ring.toSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Algebra.id DFunLike.coe ContinuousMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace NNReal.instTopologicalSpace ContinuousMap.instFunLike ContinuousMap.realToNNReal	Set Set.instMembership ENNReal.toReal spectralRadius	—	NNReal.spectralRadius_mem_spectrum
spectralRadius_mem_spectrum_or 📖	mathematical	Set.Nonempty Real spectrum instCommSemiring NormedRing.toRing NormedAlgebra.toAlgebra normedField NormedRing.toSeminormedRing	Set Set.instMembership ENNReal.toReal spectralRadius instNeg	—	spectrum.exists_nnnorm_eq_spectralRadius_of_nonempty instProperSpaceReal neg_neg abs_choice

SpectrumRestricts

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
nnreal_iff_spectralRadius_le 📖	mathematical	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder spectralRadius Real Real.normedField ENNReal.ofNNReal	SpectrumRestricts NNReal NNReal.instSemifield Field.toSemifield Real.instField NNReal.instAlgebraOfReal Ring.toSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Algebra.id Real.instCommSemiring DFunLike.coe ContinuousMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace NNReal.instTopologicalSpace ContinuousMap.instFunLike ContinuousMap.realToNNReal SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike algebraMap NNReal.toReal	—	Set.mem_Icc abs_le Real.instIsOrderedAddMonoid Real.norm_eq_abs coe_nnnorm NNReal.coe_le_coe ENNReal.coe_le_coe LE.le.trans le_iSup₂ nnreal_iff iSup₂_le Set.singleton_sub Set.image_congr spectrum.singleton_sub_eq CanLift.prf NNReal.canLift NNReal.coe_sub NNReal.nnnorm_eq ENNReal.coe_sub ENNReal.instOrderedSub ENNReal.instCanonicallyOrderedAdd iSup_congr_Prop iSup_exists le_of_not_gt Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.cast_zero Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero Mathlib.Tactic.Linarith.add_lt_of_le_of_neg Real.instIsStrictOrderedRing Mathlib.Tactic.Linarith.sub_nonpos_of_le Real.instIsOrderedRing Mathlib.Tactic.Linarith.sub_neg_of_lt
spectralRadius_eq 📖	mathematical	SpectrumRestricts Field.toSemifield NormedField.toField NormedRing.toRing NormedAlgebra.toAlgebra NormedRing.toSeminormedRing SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing	spectralRadius	—	spectralRadius.eq_1 Isometry.nnnorm_map_of_map_zero algebraMap_isometry NormedDivisionRing.to_normOneClass map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass le_antisymm iSup₂_le Eq.trans_le le_iSup₂ spectrum.algebraMap_mem_iff algebraMap_image

Subalgebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
frontier_spectrum 📖	mathematical	—	Set Set.instHasSubset frontier UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing spectrum SetLike.instMembership Semifield.toCommSemiring Field.toSemifield NormedField.toField NormedRing.toRing SubringClass.toNormedRing NormedAlgebra.toAlgebra SubringClass.toSeminormedRing NormedRing.toSeminormedRing SubalgebraClass.toNormedAlgebra	—	IsClosed.completeSpace_coe Set.mem_diff IsOpen.frontier_eq IsClosed.isOpen_compl spectrum.isClosed frontier_compl Set.mem_compl_iff spectrum.notMem_iff isUnit_of_isUnit_val_of_eventually SubringClass.addSubgroupClass Filter.map_mono Filter.Tendsto.eq_1 ContinuousAt.eq_1 ContinuousAt.sub IsTopologicalAddGroup.to_continuousSub SeminormedAddCommGroup.toIsTopologicalAddGroup Continuous.continuousAt continuous_algebraMap SMulMemClass.continuousSMul IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul continuousAt_const Filter.eventually_map Filter.Eventually.filter_mono inf_le_right Filter.NeBot.map mem_closure_iff_clusterPt
frontier_subset_frontier 📖	mathematical	—	Set Set.instHasSubset frontier UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing spectrum SetLike.instMembership Semifield.toCommSemiring Field.toSemifield NormedField.toField NormedRing.toRing SubringClass.toNormedRing NormedAlgebra.toAlgebra SubringClass.toSeminormedRing NormedRing.toSeminormedRing SubalgebraClass.toNormedAlgebra	—	frontier_eq_closure_inter_closure IsClosed.closure_eq spectrum.isClosed Set.subset_inter frontier_spectrum HasSubset.Subset.trans Set.instIsTransSubset Set.inter_subset_right closure_mono Set.compl_subset_compl spectrum.subset_subalgebra
isUnit_of_isUnit_val_of_eventually 📖	—	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NormedRing.toRing SetLike.instMembership Filter Preorder.toLE PartialOrder.toPreorder Filter.instPartialOrder nhds instTopologicalSpaceSubtype UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing Filter.Eventually SubringClass.toNormedRing	—	—	SubringClass.toSubsemiringClass Ring.inverse_unit Filter.Tendsto.comp ContinuousAt.tendsto NormedRing.inverse_continuousAt instHasSummableGeomSeriesOfCompleteSpace continuousAt_subtype_val Filter.map_mono IsClosed.mem_of_tendsto Filter.map_neBot Filter.eventually_map Filter.Eventually.mono IsUnit.map MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass IsUnit.unit_spec SubalgebraClass.val.eq_1 Units.mul_eq_one_iff_inv_eq IsUnit.mul_val_inv IsUnit.val_inv_mul
spectrum_eq_of_isPreconnected_compl 📖	mathematical	IsPreconnected UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField Compl.compl Set Set.instCompl spectrum Semifield.toCommSemiring Field.toSemifield NormedField.toField NormedRing.toRing NormedAlgebra.toAlgebra NormedRing.toSeminormedRing SetLike.instMembership	SubringClass.toNormedRing SubringClass.toSeminormedRing SubalgebraClass.toNormedAlgebra	—	Set.eq_empty_of_forall_notMem NormedSpace.unbounded_univ IsLocalRing.toNontrivial Field.instIsLocalRing Set.mem_diff Bornology.IsBounded.union spectrum.isBounded spectrum_isBounded_connectedComponentIn IsPreconnected.connectedComponentIn Set.union_compl_self spectrum_sUnion_connectedComponentIn Set.iUnion_congr_Prop Set.iUnion_of_empty instIsEmptyFalse Set.iUnion_empty Set.union_empty
spectrum_isBounded_connectedComponentIn 📖	mathematical	Set Set.instMembership spectrum SetLike.instMembership Semifield.toCommSemiring Field.toSemifield NormedField.toField NormedRing.toRing SubringClass.toNormedRing NormedAlgebra.toAlgebra SubringClass.toSeminormedRing NormedRing.toSeminormedRing SubalgebraClass.toNormedAlgebra	Bornology.IsBounded PseudoMetricSpace.toBornology SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing connectedComponentIn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Compl.compl Set.instCompl	—	connectedComponentIn_eq_empty IsClosed.completeSpace_coe spectrum_sUnion_connectedComponentIn HasSubset.Subset.trans Set.instIsTransSubset Set.subset_biUnion_of_mem Set.mem_diff_of_mem Set.subset_union_right Bornology.IsBounded.subset spectrum.isBounded
spectrum_sUnion_connectedComponentIn 📖	mathematical	—	spectrum SetLike.instMembership Semifield.toCommSemiring Field.toSemifield NormedField.toField NormedRing.toRing SubringClass.toNormedRing NormedAlgebra.toAlgebra SubringClass.toSeminormedRing NormedRing.toSeminormedRing SubalgebraClass.toNormedAlgebra Set Set.instUnion Set.iUnion Set.instMembership Set.instSDiff connectedComponentIn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Compl.compl Set.instCompl	—	IsClosed.completeSpace_coe IsClosed.closure_eq spectrum.isClosed closure_eq_interior_union_frontier Set.union_diff_distrib Set.diff_eq_empty frontier_spectrum Set.diff_eq_compl_inter Set.union_empty IsOpen.inter IsClosed.isOpen_compl isOpen_interior isClopen_preimage_val HasSubset.Subset.trans Set.instIsTransSubset frontier_inter_subset frontier_compl Set.union_subset Set.inter_subset_left Set.inter_subset_inter_right frontier_subset_frontier Set.inter_subset_right Set.disjoint_of_subset_left Disjoint.frontier_left disjoint_compl_right IsClopen.biUnion_connectedComponentIn Set.diff_subset_compl SubringClass.toSubsemiringClass Set.union_diff_cancel spectrum.subset_subalgebra

WeakDual.CharacterSpace

Definitions

Name	Category	Theorems
equivAlgHom 📖	CompOp	3 math math: compContinuousMap_apply, equivAlgHom_coe, equivAlgHom_symm_coe

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
equivAlgHom_coe 📖	mathematical	—	DFunLike.coe AlgHom Semifield.toCommSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField Ring.toSemiring NormedRing.toRing DivisionSemiring.toSemiring Semifield.toDivisionSemiring NormedAlgebra.toAlgebra NormedRing.toSeminormedRing Algebra.id AlgHom.funLike Equiv Set.Elem WeakDual UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing IsTopologicalSemiring.toContinuousAdd NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing UniformContinuousConstSMul.to_continuousConstSMul Algebra.toSMul Ring.uniformContinuousConstSMul NormedCommRing.toNormedRing SeminormedAddCommGroup.to_isUniformAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing IsTopologicalSemiring.toContinuousMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NonUnitalNonAssocSemiring.toAddCommMonoid NormedSpace.toModule NonUnitalNormedRing.toNonUnitalSeminormedRing NormedRing.toNonUnitalNormedRing NormedAlgebra.toNormedSpace WeakDual.characterSpace EquivLike.toFunLike Equiv.instEquivLike equivAlgHom instFunLike	—	IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul
equivAlgHom_symm_coe 📖	mathematical	—	DFunLike.coe Set.Elem WeakDual Semifield.toCommSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing IsTopologicalSemiring.toContinuousAdd NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing UniformContinuousConstSMul.to_continuousConstSMul Algebra.toSMul Algebra.id Ring.uniformContinuousConstSMul NormedRing.toRing NormedCommRing.toNormedRing SeminormedAddCommGroup.to_isUniformAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing IsTopologicalSemiring.toContinuousMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NonUnitalNonAssocSemiring.toAddCommMonoid NormedSpace.toModule NonUnitalNormedRing.toNonUnitalSeminormedRing NormedRing.toNonUnitalNormedRing NormedAlgebra.toNormedSpace NormedRing.toSeminormedRing WeakDual.characterSpace instFunLike Equiv AlgHom Ring.toSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring NormedAlgebra.toAlgebra EquivLike.toFunLike Equiv.instEquivLike Equiv.symm equivAlgHom AlgHom.funLike	—	IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul

(root)

Definitions

Name	Category	Theorems
spectralRadius 📖	CompOp	24 math math: IsStarNormal.spectralRadius_eq_nnnorm, spectrum.SpectralRadius.of_subsingleton, spectrum.spectralRadius_le_liminf_pow_nnnorm_pow_one_div, spectrum.spectralRadius_lt_of_forall_lt, spectrum.spectralRadius_one, spectrum.gelfand_formula, Real.spectralRadius_mem_spectrum, spectrum.spectralRadius_lt_of_forall_lt_of_nonempty, spectrum.pow_nnnorm_pow_one_div_tendsto_nhds_spectralRadius, IsSelfAdjoint.toReal_spectralRadius_complex_eq_norm, Real.spectralRadius_mem_spectrum_or, spectrum.spectralRadius_pow_le, spectrum.limsup_pow_nnnorm_pow_one_div_le_spectralRadius, NNReal.spectralRadius_mem_spectrum, SpectrumRestricts.spectralRadius_eq, spectrum.exists_nnnorm_eq_spectralRadius_of_nonempty, IsSelfAdjoint.spectralRadius_eq_nnnorm, spectrum.pow_norm_pow_one_div_tendsto_nhds_spectralRadius, spectrum.spectralRadius_pow_le', spectrum.spectralRadius_le_nnnorm, IsSelfAdjoint.toReal_spectralRadius_eq_norm, spectrum.exists_nnnorm_eq_spectralRadius, spectrum.spectralRadius_le_pow_nnnorm_pow_one_div, spectrum.spectralRadius_zero

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
upperHemicontinuous_quasispectrum 📖	mathematical	—	UpperHemicontinuous UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace NonUnitalSeminormedRing.toPseudoMetricSpace NonUnitalNormedRing.toNonUnitalSeminormedRing SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField quasispectrum Semifield.toCommSemiring Field.toSemifield NormedField.toField NonUnitalNormedRing.toNonUnitalRing NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup	—	IsScalarTower.left Unitization.quasispectrum_eq_spectrum_inr AlgEquiv.spectrum_eq AlgEquiv.instAlgEquivClass UpperHemicontinuous.comp upperHemicontinuous_spectrum WithLp.instCompleteSpace complete_of_proper Isometry.continuous WithLp.unitization_isometry_inr
upperHemicontinuous_quasispectrum_nnreal 📖	mathematical	—	UpperHemicontinuous NNReal UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace NonUnitalSeminormedRing.toPseudoMetricSpace NonUnitalNormedRing.toNonUnitalSeminormedRing NNReal.instTopologicalSpace quasispectrum instCommSemiringNNReal NonUnitalNormedRing.toNonUnitalRing NNReal.instModuleOfReal NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NormedSpace.toModule Real Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup	—	Isometry.isClosedEmbedding NNReal.instCompleteSpace isometry_subtype_coe quasispectrum.preimage_algebraMap NNReal.instIsScalarTowerOfReal IsScalarTower.left UpperHemicontinuous.isInducing_comp upperHemicontinuous_quasispectrum instProperSpaceReal
upperHemicontinuous_spectrum 📖	mathematical	—	UpperHemicontinuous UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing spectrum Semifield.toCommSemiring Field.toSemifield NormedField.toField NormedRing.toRing NormedAlgebra.toAlgebra	—	upperHemicontinuous_iff UpperHemicontinuousAt.of_sequences FirstCountableTopology.nhds_generated_countable TopologicalSpace.PseudoMetrizableSpace.firstCountableTopology PseudoEMetricSpace.pseudoMetrizableSpace IsCompact.isSeqCompact ProperSpace.isCompact_closedBall Filter.mp_mem Metric.closedBall_mem_nhds zero_lt_one Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike Filter.univ_mem' HasSubset.Subset.trans Set.instIsTransSubset spectrum.subset_closedBall_norm_mul Metric.closedBall_subset_closedBall mul_le_mul_of_nonneg_right IsOrderedRing.toMulPosMono Real.instIsOrderedRing LE.le.trans norm_le_norm_add_norm_sub' add_le_add_right IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid dist_eq_norm norm_nonneg IsClosed.mem_of_tendsto Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat nonunits.isClosed instHasSummableGeomSeriesOfCompleteSpace Filter.Tendsto.sub IsTopologicalAddGroup.to_continuousSub SeminormedAddCommGroup.toIsTopologicalAddGroup Filter.Tendsto.comp Continuous.tendsto continuous_algebraMap IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul Filter.Eventually.of_forall
upperHemicontinuous_spectrum_nnreal 📖	mathematical	—	UpperHemicontinuous NNReal UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing NNReal.instTopologicalSpace spectrum instCommSemiringNNReal NormedRing.toRing NNReal.instAlgebraOfReal Ring.toSemiring NormedAlgebra.toAlgebra Real Real.normedField	—	Isometry.isClosedEmbedding NNReal.instCompleteSpace isometry_subtype_coe UpperHemicontinuous.isInducing_comp upperHemicontinuous_spectrum instProperSpaceReal

quasispectrum

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instCompactSpace 📖	mathematical	—	CompactSpace Set.Elem quasispectrum Semifield.toCommSemiring Field.toSemifield NormedField.toField NonUnitalNormedRing.toNonUnitalRing NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing	—	isCompact_iff_compactSpace isCompact
instCompactSpaceNNReal 📖	mathematical	—	CompactSpace Set.Elem NNReal quasispectrum instCommSemiringNNReal NonUnitalNormedRing.toNonUnitalRing NNReal.instModuleOfReal NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NormedSpace.toModule Real Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing instTopologicalSpaceSubtype Set Set.instMembership NNReal.instTopologicalSpace	—	isCompact_iff_compactSpace preimage_algebraMap NNReal.instIsScalarTowerOfReal IsScalarTower.left Topology.IsClosedEmbedding.isCompact_preimage IsClosed.isClosedEmbedding_subtypeVal isClosed_nonneg instHasSolidNormReal Real.instIsOrderedAddMonoid
isCompact 📖	mathematical	—	IsCompact UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing quasispectrum Semifield.toCommSemiring Field.toSemifield NormedField.toField NonUnitalNormedRing.toNonUnitalRing NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing	—	IsScalarTower.left Unitization.quasispectrum_eq_spectrum_inr' AlgEquiv.spectrum_eq AlgEquiv.instAlgEquivClass spectrum.isCompact WithLp.instCompleteSpace complete_of_proper
isCompact_nnreal 📖	mathematical	—	IsCompact NNReal NNReal.instTopologicalSpace quasispectrum instCommSemiringNNReal NonUnitalNormedRing.toNonUnitalRing NNReal.instModuleOfReal NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NormedSpace.toModule Real Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing	—	isCompact_iff_compactSpace instCompactSpaceNNReal

spectrum

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_le_norm_of_mem 📖	mathematical	NNReal Set Set.instMembership spectrum instCommSemiringNNReal NormedRing.toRing NNReal.instAlgebraOfReal Ring.toSemiring NormedAlgebra.toAlgebra Real Real.normedField NormedRing.toSeminormedRing	Real.instLE NNReal.toReal Norm.norm NormedRing.toNorm	—	NNReal.coe_mono le_nnnorm_of_mem
eventually_isUnit_resolvent 📖	mathematical	—	Filter.Eventually IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NormedRing.toRing resolvent Semifield.toCommSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField NormedAlgebra.toAlgebra NormedRing.toSeminormedRing Bornology.cobounded PseudoMetricSpace.toBornology SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing	—	Filter.HasBasis.eventually_iff Filter.HasBasis.cobounded_of_norm Filter.atTop_basis_Ioi instIsDirectedOrder Real.instIsOrderedRing Real.instArchimedean instNoMaxOrderOfNontrivial Real.instNontrivial isUnit_resolvent mem_resolventSet_of_norm_lt_mul
exists_nnnorm_eq_spectralRadius_of_nonempty 📖	mathematical	Set.Nonempty spectrum Semifield.toCommSemiring Field.toSemifield NormedField.toField NormedRing.toRing NormedAlgebra.toAlgebra NormedRing.toSeminormedRing	Set Set.instMembership ENNReal.ofNNReal NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing spectralRadius	—	IsCompact.exists_isMaxOn instClosedIciTopology OrderTopology.to_orderClosedTopology NNReal.instOrderTopology isCompact Continuous.continuousOn continuous_nnnorm le_antisymm le_iSup₂ iSup₂_le
exp_mem_exp 📖	mathematical	Set Set.instMembership spectrum Semifield.toCommSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField NormedRing.toRing NormedAlgebra.toAlgebra NormedRing.toSeminormedRing	NormedSpace.exp UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace NonUnitalSeminormedRing.toIsTopologicalRing NonUnitalNormedRing.toNonUnitalSeminormedRing NormedRing.toNonUnitalNormedRing NormedCommRing.toNormedRing NormedField.toNormedCommRing SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing	—	RCLike.charZero_rclike NonUnitalSeminormedRing.toIsTopologicalRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing NormedSpace.algebraMap_exp_comm IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul RCLike.toCompleteSpace NormedSpace.exp_add_of_commute Algebra.commutes sub_add_cancel Summable.of_norm_bounded_eventually Real.summable_pow_div_factorial Filter.mp_mem Filter.eventually_cofinite_ne Filter.univ_mem' norm_smul NormedSpace.toNormSMulClass mul_comm norm_inv RCLike.norm_natCast div_eq_mul_inv div_le_div₀ PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono pow_nonneg IsOrderedRing.toZeroLEOneClass Real.instIsOrderedRing IsOrderedRing.toPosMulMono norm_nonneg norm_pow_le' pos_iff_ne_zero Nat.instCanonicallyOrderedAdd Nat.cast_pos' IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass NeZero.charZero_one Nat.factorial_pos Nat.mono_cast Nat.factorial_le pow_succ' mul_smul_comm Algebra.to_smulCommClass Summable.tsum_mul_left IsTopologicalRing.toIsTopologicalSemiring TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace SummationFilter.instNeBotUnconditional pow_succ Algebra.smul_mul_assoc Summable.tsum_mul_right NormedSpace.exp_eq_tsum Nat.cast_one inv_one pow_zero one_smul Summable.tsum_eq_zero_add SeminormedAddCommGroup.toIsTopologicalAddGroup NormedSpace.expSeries_summable' mem_iff IsUnit.sub_iff one_mul sub_mul Commute.isUnit_mul_iff sub_eq_iff_eq_add' not_iff_not
hasFPowerSeriesOnBall_inverse_one_sub_smul 📖	mathematical	—	HasFPowerSeriesOnBall NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace NormedRing.toNonUnitalNormedRing NormedAlgebra.toNormedSpace NormedRing.toSeminormedRing Ring.inverse Semiring.toMonoidWithZero Ring.toSemiring NormedRing.toRing SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Algebra.toSMul Semifield.toCommSemiring Field.toSemifield NormedField.toField SeminormedRing.toRing NormedAlgebra.toAlgebra ContinuousMultilinearMap.mkPiRing Fin.fintype EuclideanDomain.toCommRing Field.toEuclideanDomain ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing IsTopologicalSemiring.toContinuousMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing IsBoundedSMul.continuousSMul MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNormedCommRing.toNonUnitalCommRing NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid CommSemiring.toSemiring CommRing.toCommSemiring Module.toDistribMulAction NormedSpace.toIsBoundedSMul NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing Monoid.toNatPow ENNReal ENNReal.instInv ENNReal.ofNNReal NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup	—	IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul ENNReal.le_of_forall_nnreal_lt FormalMultilinearSeries.le_radius_of_bound_nnreal norm_toNNReal ContinuousMultilinearMap.norm_mkPiRing pow_zero mul_one le_imp_le_of_le_of_le mul_le_mul_left covariant_swap_mul_of_covariant_mul NNReal.mulLeftMono nnnorm_pow_le' le_refl le_max_left pow_succ' MulZeroClass.zero_mul NNReal.instCanonicallyOrderedAdd mul_comm pow_le_one' LT.lt.le NNReal.lt_inv_iff_mul_lt ENNReal.coe_lt_coe ENNReal.coe_inv ENNReal.inv_pos ENNReal.coe_ne_top nnnorm_eq_zero smul_zero norm_zero Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike Metric.eball_coe coe_nnnorm Real.lt_toNNReal_iff_coe_lt Real.toNNReal_one nnnorm_smul NormedSpace.toNormSMulClass Finset.prod_const Fintype.card_fin IsScalarTower.right Algebra.to_smulCommClass zero_add Summable.hasSum_iff TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace SummationFilter.instNeBotUnconditional summable_geometric_of_norm_lt_one NormedRing.inverse_one_sub
instCompactSpace 📖	mathematical	—	CompactSpace Set.Elem spectrum Semifield.toCommSemiring Field.toSemifield NormedField.toField NormedRing.toRing NormedAlgebra.toAlgebra NormedRing.toSeminormedRing instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing	—	isCompact_iff_compactSpace isCompact
instCompactSpaceNNReal 📖	mathematical	—	CompactSpace Set.Elem NNReal spectrum instCommSemiringNNReal NormedRing.toRing NNReal.instAlgebraOfReal Ring.toSemiring NormedAlgebra.toAlgebra Real Real.normedField NormedRing.toSeminormedRing instTopologicalSpaceSubtype Set Set.instMembership NNReal.instTopologicalSpace	—	isCompact_iff_compactSpace preimage_algebraMap NNReal.instIsScalarTowerOfReal IsScalarTower.left Topology.IsClosedEmbedding.isCompact_preimage IsClosed.isClosedEmbedding_subtypeVal isClosed_nonneg instHasSolidNormReal Real.instIsOrderedAddMonoid
isBounded 📖	mathematical	—	Bornology.IsBounded PseudoMetricSpace.toBornology SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing spectrum Semifield.toCommSemiring Field.toSemifield NormedField.toField NormedRing.toRing NormedAlgebra.toAlgebra NormedRing.toSeminormedRing	—	Bornology.IsBounded.subset Metric.isBounded_closedBall subset_closedBall_norm_mul
isClosed 📖	mathematical	—	IsClosed UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing spectrum Semifield.toCommSemiring Field.toSemifield NormedField.toField NormedRing.toRing NormedAlgebra.toAlgebra NormedRing.toSeminormedRing	—	IsOpen.isClosed_compl isOpen_resolventSet
isCompact 📖	mathematical	—	IsCompact UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing spectrum Semifield.toCommSemiring Field.toSemifield NormedField.toField NormedRing.toRing NormedAlgebra.toAlgebra NormedRing.toSeminormedRing	—	Metric.isCompact_of_isClosed_isBounded isClosed isBounded
isCompact_nnreal 📖	mathematical	—	IsCompact NNReal NNReal.instTopologicalSpace spectrum instCommSemiringNNReal NormedRing.toRing NNReal.instAlgebraOfReal Ring.toSemiring NormedAlgebra.toAlgebra Real Real.normedField NormedRing.toSeminormedRing	—	isCompact_iff_compactSpace instCompactSpaceNNReal
isOpen_resolventSet 📖	mathematical	—	IsOpen UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing resolventSet Semifield.toCommSemiring Field.toSemifield NormedField.toField NormedRing.toRing NormedAlgebra.toAlgebra NormedRing.toSeminormedRing	—	IsOpen.preimage Continuous.sub IsTopologicalAddGroup.to_continuousSub SeminormedAddCommGroup.toIsTopologicalAddGroup continuous_algebraMap IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul continuous_const Units.isOpen instHasSummableGeomSeriesOfCompleteSpace
isUnit_one_sub_smul_of_lt_inv_radius 📖	mathematical	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder ENNReal.ofNNReal NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField ENNReal.instInv spectralRadius NormedRing.toRing NormedAlgebra.toAlgebra NormedRing.toSeminormedRing	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Algebra.toSMul Semifield.toCommSemiring Field.toSemifield NormedField.toField SeminormedRing.toRing	—	zero_smul sub_zero Units.smul_def Algebra.algebraMap_eq_smul_one mem_resolventSet_iff mem_resolventSet_of_spectralRadius_lt Units.val_inv_eq_inv_val nnnorm_inv ENNReal.coe_inv nnnorm_ne_zero_iff Units.val_mk0 ENNReal.lt_inv_iff_lt_inv inv_inv IsUnit.smul_sub_iff_sub_inv_smul Units.instIsScalarTower IsScalarTower.right Units.smulCommClass_left Algebra.to_smulCommClass
le_nnnorm_of_mem 📖	mathematical	NNReal Set Set.instMembership spectrum instCommSemiringNNReal NormedRing.toRing NNReal.instAlgebraOfReal Ring.toSemiring NormedAlgebra.toAlgebra Real Real.normedField NormedRing.toSeminormedRing	Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing NormedRing.toNonUnitalNormedRing	—	Real.le_norm_self norm_le_norm_of_mem
mem_resolventSet_of_norm_lt 📖	mathematical	Real Real.instLT Norm.norm NormedRing.toNorm NormedField.toNorm	Set Set.instMembership resolventSet Semifield.toCommSemiring Field.toSemifield NormedField.toField NormedRing.toRing NormedAlgebra.toAlgebra NormedRing.toSeminormedRing	—	mem_resolventSet_of_norm_lt_mul NormOneClass.norm_one mul_one
mem_resolventSet_of_norm_lt_mul 📖	mathematical	Real Real.instLT Real.instMul Norm.norm NormedRing.toNorm AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedRing.toRing NormedField.toNorm	Set Set.instMembership resolventSet Semifield.toCommSemiring Field.toSemifield NormedField.toField NormedAlgebra.toAlgebra NormedRing.toSeminormedRing	—	resolventSet.eq_1 Set.mem_setOf_eq Algebra.algebraMap_eq_smul_one Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim Unique.instSubsingleton ne_zero_of_norm_ne_zero LT.lt.ne' LE.le.trans_lt mul_nonneg IsOrderedRing.toPosMulMono Real.instIsOrderedRing norm_nonneg norm_neg MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass Units.val_inv_eq_inv_val norm_algebraMap norm_inv mul_inv_rev inv_inv mul_inv_lt_iff₀' PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing inv_pos norm_pos_iff one_ne_zero NeZero.one sub_eq_add_neg instHasSummableGeomSeriesOfCompleteSpace Units.isUnit
mem_resolventSet_of_spectralRadius_lt 📖	mathematical	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder spectralRadius ENNReal.ofNNReal NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing	Set Set.instMembership resolventSet Semifield.toCommSemiring Field.toSemifield NormedField.toField	—	LT.lt.not_ge le_iSup₂
norm_le_norm_mul_of_mem 📖	mathematical	Set Set.instMembership spectrum Semifield.toCommSemiring Field.toSemifield NormedField.toField NormedRing.toRing NormedAlgebra.toAlgebra NormedRing.toSeminormedRing	Real Real.instLE Norm.norm NormedField.toNorm Real.instMul NormedRing.toNorm AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	le_of_not_gt mem_resolventSet_of_norm_lt_mul
norm_le_norm_of_mem 📖	mathematical	Set Set.instMembership spectrum Semifield.toCommSemiring Field.toSemifield NormedField.toField NormedRing.toRing NormedAlgebra.toAlgebra NormedRing.toSeminormedRing	Real Real.instLE Norm.norm NormedField.toNorm NormedRing.toNorm	—	le_of_not_gt mem_resolventSet_of_norm_lt
resolvent_isBigO_inv 📖	mathematical	—	Asymptotics.IsBigO NormedRing.toNorm NormedField.toNorm NontriviallyNormedField.toNormedField Bornology.cobounded PseudoMetricSpace.toBornology SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing resolvent Semifield.toCommSemiring Field.toSemifield NormedField.toField NormedRing.toRing NormedAlgebra.toAlgebra NormedRing.toSeminormedRing InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero	—	map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass NormedDivisionRing.to_normOneClass Asymptotics.IsBigO.comp_tendsto NormedRing.inverse_one_sub_norm instHasSummableGeomSeriesOfCompleteSpace zero_smul Filter.Tendsto.smul_const IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul Filter.tendsto_inv₀_cobounded Filter.mp_mem Bornology.isBounded_singleton Filter.univ_mem' CanLift.prf instCanLiftUnitsValIsUnit Ne.isUnit Units.val_inv_eq_inv_val inv_smul_smul₀ IsLocalRing.toNontrivial Field.instIsLocalRing units_smul_resolvent_self Asymptotics.IsBigO.of_norm_right norm_inv mul_one Asymptotics.IsBigO.smul NormedSpace.toNormSMulClass Asymptotics.IsBigO.norm_right Asymptotics.isBigO_refl
resolvent_tendsto_cobounded 📖	mathematical	—	Filter.Tendsto resolvent Semifield.toCommSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField NormedRing.toRing NormedAlgebra.toAlgebra NormedRing.toSeminormedRing Bornology.cobounded PseudoMetricSpace.toBornology SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	Asymptotics.IsBigO.trans_tendsto resolvent_isBigO_inv Filter.tendsto_inv₀_cobounded
spectralRadius_le_liminf_pow_nnnorm_pow_one_div 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder spectralRadius NormedRing.toRing NormedAlgebra.toAlgebra NormedRing.toSeminormedRing Filter.liminf ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot ENNReal.instCompleteLinearOrder Real ENNReal.instPowReal ENNReal.ofNNReal NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing NormedRing.toNonUnitalNormedRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring DivInvMonoid.toDiv Real.instDivInvMonoid Real.instOne Real.instNatCast Filter.atTop Nat.instPreorder	—	ENNReal.le_of_forall_lt_one_mul_le MulZeroClass.zero_mul one_div ENNReal.instCanonicallyOrderedAdd Filter.liminf_eq_iSup_iInf_of_nat' ENNReal.mul_le_iff_le_inv LT.lt.ne LT.lt.trans_le le_top mul_comm ENNReal.iSup_mul ENNReal.iInf_mul Nat.cast_add PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing IsOrderedRing.toPosMulMono Real.instIsOrderedRing instIsEmptyFalse Filter.eventually_atTop instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat ENNReal.eventually_pow_one_div_le ENNReal.coe_ne_top inv_one ENNReal.inv_lt_inv le_trans le_iInf LE.le.trans spectralRadius_le_pow_nnnorm_pow_one_div Nat.cast_one le_imp_le_of_le_of_le mul_le_mul_right IsOrderedMonoid.toMulLeftMono ENNReal.instIsOrderedMonoid le_refl le_iSup
spectralRadius_le_nnnorm 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder spectralRadius NormedRing.toRing NormedAlgebra.toAlgebra NormedRing.toSeminormedRing ENNReal.ofNNReal NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing NormedRing.toNonUnitalNormedRing	—	iSup₂_le norm_le_norm_of_mem
spectralRadius_le_pow_nnnorm_pow_one_div 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder spectralRadius NormedRing.toRing NormedAlgebra.toAlgebra NormedRing.toSeminormedRing Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring Real ENNReal.instPowReal ENNReal.ofNNReal NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing NormedRing.toNonUnitalNormedRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring DivInvMonoid.toDiv Real.instDivInvMonoid Real.instOne Real.instAdd Real.instNatCast AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	iSup₂_le Polynomial.aeval_monomial Algebra.algebraMap_eq_smul_one one_smul one_mul Polynomial.eval_monomial subset_polynomial_aeval norm_toNNReal nnnorm_pow NormedDivisionRing.to_normOneClass NormedDivisionRing.toNormMulClass Real.toNNReal_mul norm_nonneg ENNReal.coe_mono Real.toNNReal_mono norm_le_norm_mul_of_mem Nat.cast_zero IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass RCLike.charZero_rclike Nat.succ_pos' one_div ENNReal.pow_rpow_inv_natCast ne_of_gt Right.add_pos_of_nonneg_of_pos covariant_swap_add_of_covariant_add Nat.instIsOrderedAddMonoid zero_le Nat.instCanonicallyOrderedAdd Mathlib.Meta.Positivity.pos_of_isNat IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing Nat.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_succ ENNReal.coe_mul_rpow ENNReal.monotone_rpow_of_nonneg LT.lt.le one_div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing
spectralRadius_lt_of_forall_lt_of_nonempty 📖	mathematical	Set.Nonempty spectrum Semifield.toCommSemiring Field.toSemifield NormedField.toField NormedRing.toRing NormedAlgebra.toAlgebra NormedRing.toSeminormedRing NNReal Preorder.toLT PartialOrder.toPreorder instPartialOrderNNReal NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing	ENNReal ENNReal.instPartialOrder spectralRadius ENNReal.ofNNReal	—	Eq.trans_lt sSup_image IsCompact.sSup_lt_iff_of_continuous instClosedIciTopology OrderTopology.to_orderClosedTopology ENNReal.instOrderTopology isCompact Continuous.continuousOn continuous_enorm
spectralRadius_one 📖	mathematical	—	spectralRadius AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne ENNReal AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	—	iSup_congr_Prop one_eq iSup_iSup_eq_left nnnorm_one NormedDivisionRing.to_normOneClass
spectralRadius_pow_le 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring ENNReal.instCommSemiring spectralRadius Ring.toSemiring	—	ENNReal.iSup₂_pow_of_ne_zero iSup₂_le le_iSup₂_of_le pow_mem_pow nnnorm_pow NormedDivisionRing.to_normOneClass NormedDivisionRing.toNormMulClass
spectralRadius_pow_le' 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring ENNReal.instCommSemiring spectralRadius Ring.toSemiring	—	pow_zero spectralRadius_one spectralRadius_pow_le
spectralRadius_zero 📖	mathematical	—	spectralRadius MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing ENNReal instZeroENNReal	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim SpectralRadius.of_subsingleton iSup_congr_Prop zero_eq iSup_iSup_eq_left nnnorm_zero
subset_closedBall_norm 📖	mathematical	—	Set Set.instHasSubset spectrum Semifield.toCommSemiring Field.toSemifield NormedField.toField NormedRing.toRing NormedAlgebra.toAlgebra NormedRing.toSeminormedRing Metric.closedBall SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Norm.norm NormedRing.toNorm	—	dist_zero_right norm_le_norm_of_mem
subset_closedBall_norm_mul 📖	mathematical	—	Set Set.instHasSubset spectrum Semifield.toCommSemiring Field.toSemifield NormedField.toField NormedRing.toRing NormedAlgebra.toAlgebra NormedRing.toSeminormedRing Metric.closedBall SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real Real.instMul Norm.norm NormedRing.toNorm AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	dist_zero_right norm_le_norm_mul_of_mem

spectrum.SpectralRadius

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_subsingleton 📖	mathematical	—	spectralRadius ENNReal instZeroENNReal	—	iSup_congr_Prop spectrum.of_subsingleton iSup_neg bot_eq_zero' ENNReal.instCanonicallyOrderedAdd ciSup_const Nontrivial.to_nonempty IsLocalRing.toNontrivial Field.instIsLocalRing

---

← Back to Index