Documentation Verification Report

Basic

📁 Source: Mathlib/MeasureTheory/Function/SpecialFunctions/Basic.lean

Statistics

Metric	Count
Definitions	0
Theorems `carg`, `ccos`, `ccosh`, `cexp`, `clog`, `complex_ofReal`, `cos`, `cosh`, `csin`, `csinh`, `exp`, `sin`, `sinh`, `hasMeasurablePow`, `measurable_arg`, `measurable_cos`, `measurable_cosh`, `measurable_exp`, `measurable_im`, `measurable_log`, `measurable_ofReal`, `measurable_re`, `measurable_sin`, `measurable_sinh`, `hasMeasurablePow`, `carg`, `ccos`, `ccosh`, `cexp`, `clog`, `complex_ofReal`, `cos`, `cosh`, `csin`, `csinh`, `exp`, `sin`, `sinh`, `hasMeasurablePow`, `aemeasurable_of_aemeasurable_exp`, `aemeasurable_of_aemeasurable_exp_mul`, `hasMeasurablePow`, `measurable_arccos`, `measurable_arcsin`, `measurable_cos`, `measurable_cosh`, `measurable_exp`, `measurable_log`, `measurable_of_measurable_exp`, `measurable_sin`, `measurable_sinh`	51
Total	51

AEMeasurable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`carg` 📖	mathematical	`AEMeasurable` `Complex` `Complex.measurableSpace`	`Real` `Real.measurableSpace` `Complex.arg`	—	`Measurable.comp_aemeasurable` `Complex.measurable_arg`
`ccos` 📖	mathematical	`AEMeasurable` `Complex` `Complex.measurableSpace`	`Complex.cos`	—	`Measurable.comp_aemeasurable` `Complex.measurable_cos`
`ccosh` 📖	mathematical	`AEMeasurable` `Complex` `Complex.measurableSpace`	`Complex.cosh`	—	`Measurable.comp_aemeasurable` `Complex.measurable_cosh`
`cexp` 📖	mathematical	`AEMeasurable` `Complex` `Complex.measurableSpace`	`Complex.exp`	—	`Measurable.comp_aemeasurable` `Complex.measurable_exp`
`clog` 📖	mathematical	`AEMeasurable` `Complex` `Complex.measurableSpace`	`Complex.log`	—	`Measurable.comp_aemeasurable` `Complex.measurable_log`
`complex_ofReal` 📖	mathematical	`AEMeasurable` `Real` `Real.measurableSpace`	`Complex` `Complex.measurableSpace` `Complex.ofReal`	—	`Measurable.comp_aemeasurable` `Complex.measurable_ofReal`
`cos` 📖	mathematical	`AEMeasurable` `Real` `Real.measurableSpace`	`Real.cos`	—	`Measurable.comp_aemeasurable` `Real.measurable_cos`
`cosh` 📖	mathematical	`AEMeasurable` `Real` `Real.measurableSpace`	`Real.cosh`	—	`Measurable.comp_aemeasurable` `Real.measurable_cosh`
`csin` 📖	mathematical	`AEMeasurable` `Complex` `Complex.measurableSpace`	`Complex.sin`	—	`Measurable.comp_aemeasurable` `Complex.measurable_sin`
`csinh` 📖	mathematical	`AEMeasurable` `Complex` `Complex.measurableSpace`	`Complex.sinh`	—	`Measurable.comp_aemeasurable` `Complex.measurable_sinh`
`exp` 📖	mathematical	`AEMeasurable` `Real` `Real.measurableSpace`	`Real.exp`	—	`Measurable.comp_aemeasurable` `Real.measurable_exp`
`sin` 📖	mathematical	`AEMeasurable` `Real` `Real.measurableSpace`	`Real.sin`	—	`Measurable.comp_aemeasurable` `Real.measurable_sin`
`sinh` 📖	mathematical	`AEMeasurable` `Real` `Real.measurableSpace`	`Real.sinh`	—	`Measurable.comp_aemeasurable` `Real.measurable_sinh`

Complex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasMeasurablePow` 📖	mathematical	—	`MeasurablePow` `Complex` `measurableSpace` `instPow`	—	`Measurable.ite` `measurable_fst` `MeasurableSingletonClass.measurableSet_singleton` `instMeasurableSingletonClassOfMeasurableEq` `instMeasurableEqOfSecondCountableTopologyOfT2Space` `BorelSpace.opensMeasurable` `borelSpace` `secondCountable_of_proper` `instProperSpace` `instT2Space` `measurable_snd` `measurable_one` `measurable_zero` `Measurable.cexp` `Measurable.mul` `ContinuousMul.measurableMul₂` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `Measurable.clog`
`measurable_arg` 📖	mathematical	—	`Measurable` `Complex` `Real` `measurableSpace` `Real.measurableSpace` `arg`	—	`Measurable.comp` `Real.measurable_arcsin` `Measurable.div` `measurableDiv₂_of_mul_inv` `ContinuousMul.measurableMul₂` `Real.borelSpace` `instSecondCountableTopologyReal` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `ContinuousInv₀.measurableInv` `T5Space.toT1Space` `T6Space.toT5Space` `instT6SpaceOfMetrizableSpace` `EMetricSpace.metrizableSpace` `IsTopologicalDivisionRing.toContinuousInv₀` `instIsTopologicalDivisionRingReal` `measurable_im` `measurable_norm` `BorelSpace.opensMeasurable` `borelSpace` `MeasurableNeg.measurable_neg` `ContinuousNeg.measurableNeg` `IsTopologicalRing.toContinuousNeg` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `Measurable.ite` `IsClosed.measurableSet` `isClosed_le` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid` `continuous_const` `continuous_re` `continuous_im` `Measurable.add_const` `ContinuousAdd.measurableAdd` `IsTopologicalSemiring.toContinuousAdd` `Measurable.sub_const` `ContinuousSub.measurableSub` `IsTopologicalAddGroup.to_continuousSub` `instIsTopologicalAddGroupReal`
`measurable_cos` 📖	mathematical	—	`Measurable` `Complex` `measurableSpace` `cos`	—	`Continuous.measurable` `BorelSpace.opensMeasurable` `borelSpace` `continuous_cos`
`measurable_cosh` 📖	mathematical	—	`Measurable` `Complex` `measurableSpace` `cosh`	—	`Continuous.measurable` `BorelSpace.opensMeasurable` `borelSpace` `continuous_cosh`
`measurable_exp` 📖	mathematical	—	`Measurable` `Complex` `measurableSpace` `exp`	—	`Continuous.measurable` `BorelSpace.opensMeasurable` `borelSpace` `continuous_exp`
`measurable_im` 📖	mathematical	—	`Measurable` `Complex` `Real` `measurableSpace` `Real.measurableSpace` `im`	—	`Continuous.measurable` `BorelSpace.opensMeasurable` `borelSpace` `Real.borelSpace` `continuous_im`
`measurable_log` 📖	mathematical	—	`Measurable` `Complex` `measurableSpace` `log`	—	`Measurable.add` `ContinuousAdd.measurableMul₂` `borelSpace` `secondCountable_of_proper` `instProperSpace` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `Measurable.comp` `measurable_ofReal` `Real.measurable_log` `measurable_norm` `BorelSpace.opensMeasurable` `Measurable.mul_const` `ContinuousMul.measurableMul` `IsTopologicalSemiring.toContinuousMul` `measurable_arg`
`measurable_ofReal` 📖	mathematical	—	`Measurable` `Real` `Complex` `Real.measurableSpace` `measurableSpace` `ofReal`	—	`Continuous.measurable` `BorelSpace.opensMeasurable` `Real.borelSpace` `borelSpace` `continuous_ofReal`
`measurable_re` 📖	mathematical	—	`Measurable` `Complex` `Real` `measurableSpace` `Real.measurableSpace` `re`	—	`Continuous.measurable` `BorelSpace.opensMeasurable` `borelSpace` `Real.borelSpace` `continuous_re`
`measurable_sin` 📖	mathematical	—	`Measurable` `Complex` `measurableSpace` `sin`	—	`Continuous.measurable` `BorelSpace.opensMeasurable` `borelSpace` `continuous_sin`
`measurable_sinh` 📖	mathematical	—	`Measurable` `Complex` `measurableSpace` `sinh`	—	`Continuous.measurable` `BorelSpace.opensMeasurable` `borelSpace` `continuous_sinh`

ENNReal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasMeasurablePow` 📖	mathematical	—	`MeasurablePow` `ENNReal` `Real` `measurableSpace` `Real.measurableSpace` `instPowReal`	—	`measurable_of_measurable_nnreal_prod` `Measurable.ite` `MeasurableSet.inter` `measurable_fst` `MeasurableSingletonClass.measurableSet_singleton` `instMeasurableSingletonClassOfMeasurableEq` `instMeasurableEqOfSecondCountableTopologyOfT2Space` `BorelSpace.opensMeasurable` `NNReal.borelSpace` `NNReal.instSecondCountableTopology` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `measurable_snd` `measurableSet_Iio` `Real.borelSpace` `instClosedIciTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid` `measurable_const` `Measurable.coe_nnreal_ennreal` `Measurable.pow` `NNReal.hasMeasurablePow` `measurableSet_Ioi` `instClosedIicTopology` `instSecondCountableTopologyReal`

Measurable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`carg` 📖	mathematical	`Measurable` `Complex` `Complex.measurableSpace`	`Real` `Real.measurableSpace` `Complex.arg`	—	`comp` `Complex.measurable_arg`
`ccos` 📖	mathematical	`Measurable` `Complex` `Complex.measurableSpace`	`Complex.cos`	—	`comp` `Complex.measurable_cos`
`ccosh` 📖	mathematical	`Measurable` `Complex` `Complex.measurableSpace`	`Complex.cosh`	—	`comp` `Complex.measurable_cosh`
`cexp` 📖	mathematical	`Measurable` `Complex` `Complex.measurableSpace`	`Complex.exp`	—	`comp` `Complex.measurable_exp`
`clog` 📖	mathematical	`Measurable` `Complex` `Complex.measurableSpace`	`Complex.log`	—	`comp` `Complex.measurable_log`
`complex_ofReal` 📖	mathematical	`Measurable` `Real` `Real.measurableSpace`	`Complex` `Complex.measurableSpace` `Complex.ofReal`	—	`comp` `Complex.measurable_ofReal`
`cos` 📖	mathematical	`Measurable` `Real` `Real.measurableSpace`	`Real.cos`	—	`comp` `Real.measurable_cos`
`cosh` 📖	mathematical	`Measurable` `Real` `Real.measurableSpace`	`Real.cosh`	—	`comp` `Real.measurable_cosh`
`csin` 📖	mathematical	`Measurable` `Complex` `Complex.measurableSpace`	`Complex.sin`	—	`comp` `Complex.measurable_sin`
`csinh` 📖	mathematical	`Measurable` `Complex` `Complex.measurableSpace`	`Complex.sinh`	—	`comp` `Complex.measurable_sinh`
`exp` 📖	mathematical	`Measurable` `Real` `Real.measurableSpace`	`Real.exp`	—	`comp` `Real.measurable_exp`
`sin` 📖	mathematical	`Measurable` `Real` `Real.measurableSpace`	`Real.sin`	—	`comp` `Real.measurable_sin`
`sinh` 📖	mathematical	`Measurable` `Real` `Real.measurableSpace`	`Real.sinh`	—	`comp` `Real.measurable_sinh`

NNReal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasMeasurablePow` 📖	mathematical	—	`MeasurablePow` `NNReal` `Real` `measurableSpace` `Real.measurableSpace` `instPowReal`	—	`Measurable.pow` `Real.hasMeasurablePow` `Measurable.coe_nnreal_real` `measurable_fst` `measurable_snd`

Real

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`aemeasurable_of_aemeasurable_exp` 📖	—	`AEMeasurable` `Real` `measurableSpace` `exp`	—	—	`log_exp` `Measurable.comp_aemeasurable` `measurable_log`
`aemeasurable_of_aemeasurable_exp_mul` 📖	—	`AEMeasurable` `Real` `measurableSpace` `exp` `instMul`	—	—	`mul_div_cancel_left₀` `GroupWithZero.toMulDivCancelClass` `AEMeasurable.div` `measurableDiv₂_of_mul_inv` `ContinuousMul.measurableMul₂` `borelSpace` `instSecondCountableTopologyReal` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `ContinuousInv₀.measurableInv` `T5Space.toT1Space` `T6Space.toT5Space` `instT6SpaceOfMetrizableSpace` `EMetricSpace.metrizableSpace` `IsTopologicalDivisionRing.toContinuousInv₀` `instIsTopologicalDivisionRingReal` `aemeasurable_of_aemeasurable_exp` `aemeasurable_const`
`hasMeasurablePow` 📖	mathematical	—	`MeasurablePow` `Real` `measurableSpace` `instPow`	—	`Measurable.comp` `Complex.measurable_re` `Measurable.pow` `Complex.hasMeasurablePow` `Complex.measurable_ofReal` `measurable_fst` `measurable_snd`
`measurable_arccos` 📖	mathematical	—	`Measurable` `Real` `measurableSpace` `arccos`	—	`Continuous.measurable` `BorelSpace.opensMeasurable` `borelSpace` `continuous_arccos`
`measurable_arcsin` 📖	mathematical	—	`Measurable` `Real` `measurableSpace` `arcsin`	—	`Continuous.measurable` `BorelSpace.opensMeasurable` `borelSpace` `continuous_arcsin`
`measurable_cos` 📖	mathematical	—	`Measurable` `Real` `measurableSpace` `cos`	—	`Continuous.measurable` `BorelSpace.opensMeasurable` `borelSpace` `continuous_cos`
`measurable_cosh` 📖	mathematical	—	`Measurable` `Real` `measurableSpace` `cosh`	—	`Continuous.measurable` `BorelSpace.opensMeasurable` `borelSpace` `continuous_cosh`
`measurable_exp` 📖	mathematical	—	`Measurable` `Real` `measurableSpace` `exp`	—	`Continuous.measurable` `BorelSpace.opensMeasurable` `borelSpace` `continuous_exp`
`measurable_log` 📖	mathematical	—	`Measurable` `Real` `measurableSpace` `log`	—	`measurable_of_measurable_on_compl_singleton` `instMeasurableSingletonClassOfMeasurableEq` `instMeasurableEqOfSecondCountableTopologyOfT2Space` `BorelSpace.opensMeasurable` `borelSpace` `instSecondCountableTopologyReal` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `Continuous.measurable` `Subtype.opensMeasurableSpace` `continuousOn_iff_continuous_restrict` `continuousOn_log`
`measurable_of_measurable_exp` 📖	—	`Measurable` `Real` `measurableSpace` `exp`	—	—	`log_exp` `Measurable.comp` `measurable_log`
`measurable_sin` 📖	mathematical	—	`Measurable` `Real` `measurableSpace` `sin`	—	`Continuous.measurable` `BorelSpace.opensMeasurable` `borelSpace` `continuous_sin`
`measurable_sinh` 📖	mathematical	—	`Measurable` `Real` `measurableSpace` `sinh`	—	`Continuous.measurable` `BorelSpace.opensMeasurable` `borelSpace` `continuous_sinh`

---

← Back to Index