Documentation Verification Report

GelfandFormula

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

Statistics

Metric	Count
Definitions `algEquivComplexOfComplete`	1
Theorems `algEquivComplexOfComplete_apply`, `algEquivComplexOfComplete_symm_apply`, `algebraMap_eq_of_mem`, `differentiableOn_inverse_one_sub_smul`, `exists_nnnorm_eq_spectralRadius`, `gelfand_formula`, `hasDerivAt_resolvent`, `limsup_pow_nnnorm_pow_one_div_le_spectralRadius`, `map_polynomial_aeval`, `map_pow`, `nonempty`, `pow_nnnorm_pow_one_div_tendsto_nhds_spectralRadius`, `pow_norm_pow_one_div_tendsto_nhds_spectralRadius`, `spectralRadius_lt_of_forall_lt`	14
Total	15

NormedRing

Definitions

Name	Category	Theorems
`algEquivComplexOfComplete` 📖	CompOp	2 math math: `algEquivComplexOfComplete_symm_apply`, `algEquivComplexOfComplete_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`algEquivComplexOfComplete_apply` 📖	mathematical	`IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `toRing`	`DFunLike.coe` `AlgEquiv` `Complex` `Complex.instCommSemiring` `Complex.instSemiring` `Algebra.id` `NormedAlgebra.toAlgebra` `Complex.instNormedField` `toSeminormedRing` `AlgEquiv.instFunLike` `algEquivComplexOfComplete` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `algebraMap`	—	—
`algEquivComplexOfComplete_symm_apply` 📖	mathematical	`IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `toRing`	`DFunLike.coe` `AlgEquiv` `Complex` `Complex.instCommSemiring` `Complex.instSemiring` `NormedAlgebra.toAlgebra` `Complex.instNormedField` `toSeminormedRing` `Algebra.id` `AlgEquiv.instFunLike` `AlgEquiv.symm` `algEquivComplexOfComplete` `Set.Nonempty.some` `spectrum` `spectrum.nonempty`	—	—

spectrum

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`algebraMap_eq_of_mem` 📖	mathematical	`IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `NormedRing.toRing` `Complex` `Set` `Set.instMembership` `spectrum` `Complex.instCommSemiring` `NormedAlgebra.toAlgebra` `Complex.instNormedField` `NormedRing.toSeminormedRing`	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `algebraMap`	—	`sub_eq_zero` `mem_iff`
`differentiableOn_inverse_one_sub_smul` 📖	mathematical	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `ENNReal.ofNNReal` `ENNReal.instInv` `spectralRadius` `NontriviallyNormedField.toNormedField` `NormedRing.toRing` `NormedAlgebra.toAlgebra` `NormedRing.toSeminormedRing`	`DifferentiableOn` `NormedAddCommGroup.toAddCommGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NormedSpace.toModule` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedRing.toNonUnitalNormedRing` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `NormedAlgebra.toNormedSpace` `Ring.inverse` `Semiring.toMonoidWithZero` `Ring.toSemiring` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Algebra.toSMul` `Semifield.toCommSemiring` `Field.toSemifield` `NormedField.toField` `SeminormedRing.toRing` `Metric.closedBall` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NNReal.toReal`	—	`DifferentiableAt.differentiableWithinAt` `isUnit_one_sub_smul_of_lt_inv_radius` `lt_of_le_of_lt` `ENNReal.coe_mono` `norm_toNNReal` `Real.toNNReal_coe` `Real.toNNReal_mono` `mem_closedBall_zero_iff` `Differentiable.const_sub` `Differentiable.smul_const` `NormedSpace.toIsBoundedSMul` `IsScalarTower.left` `differentiable_id` `DifferentiableAt.comp` `differentiableAt_inverse` `instHasSummableGeomSeriesOfCompleteSpace` `Differentiable.differentiableAt`
`exists_nnnorm_eq_spectralRadius` 📖	mathematical	—	`Complex` `Set` `Set.instMembership` `spectrum` `Complex.instCommSemiring` `NormedRing.toRing` `NormedAlgebra.toAlgebra` `Complex.instNormedField` `NormedRing.toSeminormedRing` `ENNReal.ofNNReal` `NNNorm.nnnorm` `SeminormedAddGroup.toNNNorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `spectralRadius`	—	`exists_nnnorm_eq_spectralRadius_of_nonempty` `Complex.instProperSpace` `nonempty`
`gelfand_formula` 📖	mathematical	—	`Filter.Tendsto` `ENNReal` `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` `NormedRing.toRing` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instOne` `Real.instNatCast` `Filter.atTop` `Nat.instPreorder` `nhds` `ENNReal.instTopologicalSpace` `spectralRadius` `Complex` `Complex.instNormedField` `NormedAlgebra.toAlgebra` `NormedRing.toSeminormedRing`	—	`pow_nnnorm_pow_one_div_tendsto_nhds_spectralRadius`
`hasDerivAt_resolvent` 📖	mathematical	`Set` `Set.instMembership` `resolventSet` `Semifield.toCommSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `NormedRing.toRing` `NormedAlgebra.toAlgebra` `NormedRing.toSeminormedRing`	`HasDerivAt` `NormedAddCommGroup.toAddCommGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NormedRing.toNonUnitalNormedRing` `NormedSpace.toModule` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `NormedAlgebra.toNormedSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `IsBoundedSMul.continuousSMul` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `NormedSpace.toIsBoundedSMul` `resolvent` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Monoid.toNatPow` `Ring.toSemiring`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalSeminormedRing.toIsTopologicalRing` `smulCommClass_self` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `ContinuousLinearMap.topologicalAddGroup` `ContinuousLinearMap.smulCommClass` `ContinuousLinearMap.continuousConstSMul` `IsScalarTower.right` `Algebra.to_smulCommClass` `hasFDerivAt_ringInverse` `instHasSummableGeomSeriesOfCompleteSpace` `IsBoundedSMul.continuousSMul` `HasDerivAt.congr_simp` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `HasDerivAt.sub_const` `LinearMap.hasDerivAt` `sq` `Ring.inverse_unit` `mul_one` `HasFDerivAt.comp_hasDerivAt`
`limsup_pow_nnnorm_pow_one_div_le_spectralRadius` 📖	mathematical	—	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `Filter.limsup` `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` `NormedRing.toRing` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instOne` `Real.instNatCast` `Filter.atTop` `Nat.instPreorder` `spectralRadius` `Complex` `Complex.instNormedField` `NormedAlgebra.toAlgebra` `NormedRing.toSeminormedRing`	—	`ENNReal.inv_le_inv` `ENNReal.le_of_forall_pos_nnreal_lt` `ENNReal.inv_limsup` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `NonUnitalSeminormedRing.toIsTopologicalRing` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `IsBoundedSMul.continuousSMul` `DifferentiableOn.hasFPowerSeriesOnBall` `differentiableOn_inverse_one_sub_smul` `HasFPowerSeriesOnBall.r_le` `HasFPowerSeriesOnBall.exchange_radius` `hasFPowerSeriesOnBall_inverse_one_sub_smul` `instHasSummableGeomSeriesOfCompleteSpace` `FormalMultilinearSeries.radius_eq_liminf` `ContinuousMultilinearMap.norm_mkPiRing` `norm_toNNReal` `ENNReal.coe_rpow_def` `lt_self_iff_false` `LT.lt.trans_le` `one_div_nonneg` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `Nat.cast_nonneg` `Real.instIsOrderedRing`
`map_polynomial_aeval` 📖	mathematical	—	`spectrum` `Complex` `Complex.instCommSemiring` `NormedRing.toRing` `NormedAlgebra.toAlgebra` `Complex.instNormedField` `NormedRing.toSeminormedRing` `DFunLike.coe` `AlgHom` `Polynomial` `CommSemiring.toSemiring` `Polynomial.semiring` `Ring.toSemiring` `Polynomial.algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `Polynomial.aeval` `Set.image` `Polynomial.eval` `Complex.instSemiring`	—	`map_polynomial_aeval_of_nonempty` `Complex.isAlgClosed` `nonempty`
`map_pow` 📖	mathematical	—	`spectrum` `Complex` `Complex.instCommSemiring` `NormedRing.toRing` `NormedAlgebra.toAlgebra` `Complex.instNormedField` `NormedRing.toSeminormedRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Set.image` `Complex.instSemiring`	—	`Polynomial.aeval_X_pow` `Set.image_congr` `Polynomial.eval_X_pow` `map_polynomial_aeval`
`nonempty` 📖	mathematical	—	`Set.Nonempty` `Complex` `spectrum` `Complex.instCommSemiring` `NormedRing.toRing` `NormedAlgebra.toAlgebra` `Complex.instNormedField` `NormedRing.toSeminormedRing`	—	`Set.compl_empty_iff` `eq_1` `HasDerivAt.differentiableAt` `hasDerivAt_resolvent` `Set.mem_univ` `Differentiable.apply_eq_of_tendsto_cocompact` `Complex.instNontrivial` `Metric.cobounded_eq_cocompact` `Complex.instProperSpace` `resolvent_tendsto_cobounded` `not_isUnit_zero` `isUnit_resolvent`
`pow_nnnorm_pow_one_div_tendsto_nhds_spectralRadius` 📖	mathematical	—	`Filter.Tendsto` `ENNReal` `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` `NormedRing.toRing` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instOne` `Real.instNatCast` `Filter.atTop` `Nat.instPreorder` `nhds` `ENNReal.instTopologicalSpace` `spectralRadius` `Complex` `Complex.instNormedField` `NormedAlgebra.toAlgebra` `NormedRing.toSeminormedRing`	—	`tendsto_of_le_liminf_of_limsup_le` `ENNReal.instOrderTopology` `spectralRadius_le_liminf_pow_nnnorm_pow_one_div` `limsup_pow_nnnorm_pow_one_div_le_spectralRadius` `Filter.isBounded_le_of_top` `Filter.isBounded_ge_of_bot`
`pow_norm_pow_one_div_tendsto_nhds_spectralRadius` 📖	mathematical	—	`Filter.Tendsto` `ENNReal` `ENNReal.ofReal` `Real` `Real.instPow` `Norm.norm` `NormedRing.toNorm` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `NormedRing.toRing` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instOne` `Real.instNatCast` `Filter.atTop` `Nat.instPreorder` `nhds` `ENNReal.instTopologicalSpace` `spectralRadius` `Complex` `Complex.instNormedField` `NormedAlgebra.toAlgebra` `NormedRing.toSeminormedRing`	—	`ENNReal.ofReal_rpow_of_nonneg` `norm_nonneg` `one_div_nonneg` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `Nat.cast_zero` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.instZeroLEOneClass` `RCLike.charZero_rclike` `zero_le` `Nat.instCanonicallyOrderedAdd` `coe_nnnorm` `ENNReal.coe_nnreal_eq` `pow_nnnorm_pow_one_div_tendsto_nhds_spectralRadius`
`spectralRadius_lt_of_forall_lt` 📖	mathematical	`NNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderNNReal` `NNNorm.nnnorm` `Complex` `SeminormedAddGroup.toNNNorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField`	`ENNReal` `ENNReal.instPartialOrder` `spectralRadius` `NormedRing.toRing` `NormedAlgebra.toAlgebra` `NormedRing.toSeminormedRing` `ENNReal.ofNNReal`	—	`spectralRadius_lt_of_forall_lt_of_nonempty` `Complex.instProperSpace` `nonempty`

---

← Back to Index