Documentation Verification Report

Complex

📁 Source: Mathlib/MeasureTheory/Measure/Lebesgue/Complex.lean

Statistics

Metric	Count
Definitions `measurableEquivPi`, `measurableEquivRealProd`	2
Theorems `measurableEquivPi_apply`, `measurableEquivPi_symm_apply`, `measurableEquivRealProd_apply`, `measurableEquivRealProd_symm_apply`, `volume_preserving_equiv_pi`, `volume_preserving_equiv_real_prod`	6
Total	8

Complex

Definitions

Name	Category	Theorems
`measurableEquivPi` 📖	CompOp	4 math math: `measurableEquivPi_apply`, `NumberField.mixedEmbedding.fundamentalDomain_stdBasis`, `measurableEquivPi_symm_apply`, `volume_preserving_equiv_pi`
`measurableEquivRealProd` 📖	CompOp	4 math math: `measurableEquivRealProd_apply`, `measurableEquivRealProd_symm_polarCoord_symm_apply`, `volume_preserving_equiv_real_prod`, `measurableEquivRealProd_symm_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`measurableEquivPi_apply` 📖	mathematical	—	`DFunLike.coe` `MeasurableEquiv` `Complex` `measurableSpace` `MeasurableSpace.pi` `Real` `Real.measurableSpace` `EquivLike.toFunLike` `MeasurableEquiv.instEquivLike` `measurableEquivPi` `Matrix.vecCons` `re` `im` `Matrix.vecEmpty`	—	—
`measurableEquivPi_symm_apply` 📖	mathematical	—	`DFunLike.coe` `MeasurableEquiv` `Complex` `MeasurableSpace.pi` `Real` `Real.measurableSpace` `measurableSpace` `EquivLike.toFunLike` `MeasurableEquiv.instEquivLike` `MeasurableEquiv.symm` `measurableEquivPi` `instAdd` `ofReal` `instMul` `I`	—	—
`measurableEquivRealProd_apply` 📖	mathematical	—	`DFunLike.coe` `MeasurableEquiv` `Complex` `Real` `measurableSpace` `Prod.instMeasurableSpace` `Real.measurableSpace` `EquivLike.toFunLike` `MeasurableEquiv.instEquivLike` `measurableEquivRealProd` `re` `im`	—	—
`measurableEquivRealProd_symm_apply` 📖	mathematical	—	`DFunLike.coe` `MeasurableEquiv` `Real` `Complex` `Prod.instMeasurableSpace` `Real.measurableSpace` `measurableSpace` `EquivLike.toFunLike` `MeasurableEquiv.instEquivLike` `MeasurableEquiv.symm` `measurableEquivRealProd`	—	—
`volume_preserving_equiv_pi` 📖	mathematical	—	`MeasureTheory.MeasurePreserving` `Complex` `measurableSpace` `MeasurableSpace.pi` `Real` `Real.measurableSpace` `DFunLike.coe` `MeasurableEquiv` `EquivLike.toFunLike` `MeasurableEquiv.instEquivLike` `measurableEquivPi` `MeasureTheory.MeasureSpace.volume` `measureSpaceOfInnerProductSpace` `instNormedAddCommGroup` `instInnerProductSpaceRealComplex` `FiniteDimensional.rclike_to_real` `instRCLike` `borelSpace` `MeasureTheory.MeasureSpace.pi` `Fin.fintype` `Real.measureSpace`	—	`FiniteDimensional.rclike_to_real` `borelSpace` `Pi.topologicalAddGroup` `instIsTopologicalAddGroupReal` `Pi.borelSpace` `Finite.to_countable` `Finite.of_fintype` `instSecondCountableTopologyReal` `Real.borelSpace` `MeasureTheory.addHaarMeasure_eq_volume_pi` `Module.Basis.parallelepiped_basisFun` `Module.Basis.addHaar_def` `Real.instCompleteSpace` `instT2Space` `measurableEquivPi.eq_1` `Homeomorph.toMeasurableEquiv_symm_coe` `ContinuousLinearEquiv.coe_symm_toHomeomorph` `RingHomInvPair.ids` `Module.Basis.map_addHaar` `UniformSpace.secondCountable_of_separable` `EMetric.instIsCountablyGeneratedUniformity` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `secondCountable_of_proper` `instProperSpace` `SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `instWeaklyLocallyCompactSpaceOfLocallyCompactSpace` `locallyCompact_of_proper` `Module.Basis.addHaar_eq_iff` `MeasureTheory.Measure.IsAddHaarMeasure.sigmaFinite` `instIsAddHaarMeasureVolume` `MeasureTheory.Measure.IsAddHaarMeasure.toIsAddLeftInvariant` `OrthonormalBasis.volume_parallelepiped` `MeasureTheory.MeasurePreserving.symm` `Measurable.measurePreserving` `MeasurableEquiv.measurable`
`volume_preserving_equiv_real_prod` 📖	mathematical	—	`MeasureTheory.MeasurePreserving` `Complex` `Real` `measurableSpace` `Prod.instMeasurableSpace` `Real.measurableSpace` `DFunLike.coe` `MeasurableEquiv` `EquivLike.toFunLike` `MeasurableEquiv.instEquivLike` `measurableEquivRealProd` `MeasureTheory.MeasureSpace.volume` `measureSpaceOfInnerProductSpace` `instNormedAddCommGroup` `instInnerProductSpaceRealComplex` `FiniteDimensional.rclike_to_real` `instRCLike` `borelSpace` `MeasureTheory.Measure.prod.measureSpace` `Real.measureSpace`	—	`MeasureTheory.MeasurePreserving.comp` `FiniteDimensional.rclike_to_real` `borelSpace` `MeasureTheory.volume_preserving_finTwoArrow` `MeasureTheory.Measure.IsAddHaarMeasure.sigmaFinite` `instIsAddHaarMeasureVolume` `Real.borelSpace` `SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace` `instIsTopologicalAddGroupReal` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `instSecondCountableTopologyReal` `instWeaklyLocallyCompactSpaceOfLocallyCompactSpace` `locallyCompact_of_proper` `instProperSpaceReal` `volume_preserving_equiv_pi`

---

← Back to Index