Documentation Verification Report

Basic

📁 Source: Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/ExpLog/Basic.lean

Statistics

Metric	Count
Definitions	0
Theorems `complex_exp_eq_normedSpace_exp`, `continuousOn_log`, `exp_eq_normedSpace_exp`, `exp_log`, `log_algebraMap`, `log_exp`, `log_one`, `log_pow`, `log_pow'`, `log_smul`, `log_smul'`, `log_zero`, `real_exp_eq_normedSpace_exp`, `exp_nonneg`, `exp_continuousMap_eq`	15
Total	15

CFC

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`complex_exp_eq_normedSpace_exp` 📖	mathematical	—	`cfc` `Complex` `Complex.instCommSemiring` `Complex.instStarRing` `NormedField.toMetricSpace` `Complex.instNormedField` `IsTopologicalRing.toIsTopologicalSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NonUnitalCommCStarAlgebra.toNonUnitalNormedCommRing` `CommCStarAlgebra.toNonUnitalCommCStarAlgebra` `instCommCStarAlgebraComplex` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `Complex.instContinuousStar` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `NormedRing.toRing` `NormedAlgebra.toAlgebra` `Complex.exp` `NormedSpace.exp` `NonUnitalSeminormedRing.toIsTopologicalRing` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `NormedRing.toNonUnitalNormedRing`	—	`IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `Complex.instContinuousStar` `NonUnitalSeminormedRing.toIsTopologicalRing` `exp_eq_normedSpace_exp` `Complex.exp_eq_exp_ℂ`
`continuousOn_log` 📖	mathematical	—	`ContinuousOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `log` `IsometricContinuousFunctionalCalculus.toContinuousFunctionalCalculus` `Real` `IsSelfAdjoint` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing` `StarRing.toStarAddMonoid` `Real.instCommSemiring` `instStarRingReal` `Real.metricSpace` `IsTopologicalRing.toIsTopologicalSemiring` `MetricSpace.toPseudoMetricSpace` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `Real.normedCommRing` `instIsTopologicalRingReal` `instContinuousStarReal` `NormedRing.toMetricSpace` `NormedAlgebra.toAlgebra` `Real.normedField` `setOf` `IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring`	—	`IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `instContinuousStarReal` `ContinuousOn.cfc_of_mem_nhdsSet` `Set.iUnion_congr_Prop` `T5Space.toT1Space` `OrderTopology.t5Space` `instOrderTopologyReal` `spectrum.zero_notMem` `continuousOn_id` `ContinuousOn.log` `continuousOn_id'`
`exp_eq_normedSpace_exp` 📖	mathematical	—	`cfc` `Semifield.toCommSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RCLike.toStarRing` `NormedField.toMetricSpace` `IsTopologicalRing.toIsTopologicalSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `RCLike.instContinuousStar` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `NormedRing.toRing` `NormedAlgebra.toAlgebra` `NormedSpace.exp` `NormedCommRing.toNormedRing` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing`	—	`IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `RCLike.instContinuousStar` `ContinuousOn.restrict` `continuousOn_id'` `cfc_id` `cfc_apply` `Topology.IsClosedEmbedding.continuous` `cfcHom_isClosedEmbedding` `Continuous.continuousOn` `NonUnitalSeminormedRing.toIsTopologicalRing` `NormedSpace.exp_continuous` `RCLike.charZero_rclike` `RCLike.toCompleteSpace` `ContinuousFunctionalCalculus.compactSpace_spectrum` `NormedSpace.map_exp` `ContinuousMap.instCompleteSpaceOfCompactlyCoherentSpace` `CompactlyCoherentSpace.of_sequentialSpace` `FrechetUrysohnSpace.to_sequentialSpace` `Subtype.instFrechetUrysohnSpace` `FirstCountableTopology.frechetUrysohnSpace` `TopologicalSpace.PseudoMetrizableSpace.firstCountableTopology` `PseudoEMetricSpace.pseudoMetrizableSpace` `AlgHomClass.toRingHomClass` `StarAlgHom.instAlgHomClass` `ContinuousMap.ext` `Continuous.comp` `ContinuousMap.continuous` `NormedSpace.exp_continuousMap_eq`
`exp_log` 📖	mathematical	`IsStrictlyPositive` `Preorder.toLE` `PartialOrder.toPreorder` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `NormedRing.toRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	`NormedSpace.exp` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `NonUnitalSeminormedRing.toIsTopologicalRing` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `NormedRing.toNonUnitalNormedRing` `log`	—	`IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `instContinuousStarReal` `NonUnitalSeminormedRing.toIsTopologicalRing` `real_exp_eq_normedSpace_exp` `IsSelfAdjoint.log` `log.eq_1` `cfc_comp'` `Real.instContinuousMapUniqueHom` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `ContinuousOn.rexp` `continuousOn_id'` `ContinuousOn.log` `IsSelfAdjoint.of_nonneg` `IsStrictlyPositive.nonneg` `cfc_id` `cfc_congr`
`log_algebraMap` 📖	mathematical	—	`log` `DFunLike.coe` `RingHom` `Real` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Real.instCommSemiring` `Ring.toSemiring` `NormedRing.toRing` `RingHom.instFunLike` `algebraMap` `NormedAlgebra.toAlgebra` `Real.normedField` `NormedRing.toSeminormedRing` `Real.log`	—	`IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `instContinuousStarReal` `cfc_algebraMap`
`log_exp` 📖	mathematical	`IsSelfAdjoint` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing` `StarRing.toStarAddMonoid`	`log` `NormedSpace.exp` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `NonUnitalSeminormedRing.toIsTopologicalRing` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `NormedRing.toNonUnitalNormedRing`	—	`IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `instContinuousStarReal` `ContinuousOn.log` `continuousOn_id'` `NonUnitalSeminormedRing.toIsTopologicalRing` `log.eq_1` `real_exp_eq_normedSpace_exp` `cfc_comp'` `Real.instContinuousMapUniqueHom` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `ContinuousOn.rexp` `cfc.congr_simp` `Real.log_exp` `cfc_id'`
`log_one` 📖	mathematical	—	`log` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `NormedRing.toRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	`IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `instContinuousStarReal` `cfc_apply_one` `Real.log_one` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass`
`log_pow` 📖	mathematical	`IsSelfAdjoint` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing` `StarRing.toStarAddMonoid`	`log` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `AddMonoid.toNatSMul` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NormedRing.toNonUnitalNormedRing` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid`	—	`IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `instContinuousStarReal` `ContinuousOn.log` `continuousOn_id'` `isReduced_of_noZeroDivisors` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass` `Real.instNontrivial` `log.eq_1` `cfc_pow_id` `cfc_comp'` `Real.instContinuousMapUniqueHom` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `ContinuousOn.pow` `IsTopologicalSemiring.toContinuousMul` `cfc.congr_simp` `Real.log_pow` `Nat.cast_smul_eq_nsmul` `cfc_const_mul`
`log_pow'` 📖	mathematical	`IsStrictlyPositive` `Preorder.toLE` `PartialOrder.toPreorder` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `NormedRing.toRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	`log` `Monoid.toNatPow` `AddMonoid.toNatSMul` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NormedRing.toNonUnitalNormedRing` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid`	—	`IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `instContinuousStarReal`
`log_smul` 📖	mathematical	`IsSelfAdjoint` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing` `StarRing.toStarAddMonoid`	`log` `Real` `Algebra.toSMul` `Semifield.toCommSemiring` `Field.toSemifield` `NormedField.toField` `Real.normedField` `Ring.toSemiring` `SeminormedRing.toRing` `NormedRing.toSeminormedRing` `NormedAlgebra.toAlgebra` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Real.instCommSemiring` `RingHom.instFunLike` `algebraMap` `Real.log`	—	`IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `instContinuousStarReal` `log.eq_1` `cfc_smul_id` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `IsScalarTower.left` `Pi.isScalarTower` `IsScalarTower.right` `cfc_comp` `Real.instContinuousMapUniqueHom` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `ContinuousOn.log` `continuousOn_id'` `Set.image_congr` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass` `ContinuousOn.const_smul` `cfc_congr` `Real.log_mul` `cfc_const_add`
`log_smul'` 📖	mathematical	`Real` `Real.instLT` `Real.instZero` `IsStrictlyPositive` `Preorder.toLE` `PartialOrder.toPreorder` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `NormedRing.toRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	`log` `Algebra.toSMul` `Semifield.toCommSemiring` `Field.toSemifield` `NormedField.toField` `Real.normedField` `SeminormedRing.toRing` `NormedRing.toSeminormedRing` `NormedAlgebra.toAlgebra` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Real.instCommSemiring` `RingHom.instFunLike` `algebraMap` `Real.log`	—	`IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `instContinuousStarReal`
`log_zero` 📖	mathematical	—	`log` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing`	—	`IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `instContinuousStarReal` `cfc_apply_zero` `Real.log_zero` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass`
`real_exp_eq_normedSpace_exp` 📖	mathematical	`IsSelfAdjoint` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing` `StarRing.toStarAddMonoid`	`cfc` `Real` `Real.instCommSemiring` `instStarRingReal` `Real.metricSpace` `IsTopologicalRing.toIsTopologicalSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `Real.normedCommRing` `instIsTopologicalRingReal` `instContinuousStarReal` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `NormedAlgebra.toAlgebra` `Real.normedField` `Real.exp` `NormedSpace.exp`	—	`IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `instContinuousStarReal` `exp_eq_normedSpace_exp` `Real.exp_eq_exp_ℝ`

IsSelfAdjoint

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exp_nonneg` 📖	mathematical	`IsSelfAdjoint` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing` `StarRing.toStarAddMonoid`	`Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NormedSpace.exp` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing`	—	`IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `instContinuousStarReal` `CFC.real_exp_eq_normedSpace_exp` `cfc_nonneg` `Real.instStarOrderedRing` `Real.exp_nonneg`

NormedSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exp_continuousMap_eq` 📖	mathematical	—	`exp` `ContinuousMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `ContinuousMap.instRing` `NormedRing.toRing` `NormedCommRing.toNormedRing` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `ContinuousMap.compactOpen` `NonUnitalSeminormedRing.toIsTopologicalRing` `ContinuousMap.instNonUnitalSeminormedRing` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `DFunLike.coe` `ContinuousMap.instFunLike` `Continuous.comp` `NormedRing.toSeminormedRing` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `NormedRing.toNonUnitalNormedRing` `exp_continuous` `normedAlgebraRat` `RCLike.charZero_rclike` `RCLike.toNormedAlgebra` `RCLike.toCompleteSpace` `ContinuousMap.continuous`	—	`ContinuousMap.ext` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `NonUnitalSeminormedRing.toIsTopologicalRing` `Continuous.comp` `exp_continuous` `RCLike.charZero_rclike` `RCLike.toCompleteSpace` `ContinuousMap.continuous` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalSemiring.toContinuousAdd` `SMulCommClass.continuousConstSMul` `Algebra.to_smulCommClass` `IsTopologicalSemiring.toContinuousMul` `exp_eq_expSeries_sum` `expSeries_summable` `IsBoundedSMul.continuousSMul` `toIsBoundedSMul` `ContinuousMap.instCompleteSpaceOfCompactlyCoherentSpace` `CompactlyCoherentSpace.of_weaklyLocallyCompactSpace` `instWeaklyLocallyCompactSpaceOfCompactSpace` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `ContinuousMap.tsum_apply` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `SummationFilter.instNeBotUnconditional` `expSeries_apply_eq` `exp_eq_tsum`

---

← Back to Index