Documentation Verification Report

InnerProductSpace

📁 Source: Mathlib/MeasureTheory/Measure/Haar/InnerProductSpace.lean

Statistics

Metric	Count
Definitions `measurableEquiv`, `InnerProductSpace`, `toMeasurableEquiv`, `measurableEquiv`	4
Theorems `coe_measurableEquiv`, `coe_measurableEquiv_symm`, `measurableEquiv_toEquiv`, `volume_preserving_symm_measurableEquiv_toLp`, `coe_symm_toMeasurableEquiv`, `coe_toMeasurableEquiv`, `measurePreserving`, `toMeasurableEquiv_symm`, `measure_eq_volume`, `measure_orthonormalBasis`, `addHaar_eq_volume`, `measurePreserving_measurableEquiv`, `measurePreserving_repr`, `measurePreserving_repr_symm`, `volume_parallelepiped`, `volume_preserving_ofLp`, `volume_preserving_toLp`, `volume_preserving_ofLp`, `volume_preserving_symm_measurableEquiv_toLp_prod`, `volume_preserving_toLp`, `volume_euclideanSpace_eq_dirac`	21
Total	25

EuclideanSpace

Definitions

Name	Category	Theorems
`measurableEquiv` 📖	CompOp	3 math math: `coe_measurableEquiv`, `measurableEquiv_toEquiv`, `coe_measurableEquiv_symm`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_measurableEquiv` 📖	mathematical	—	`DFunLike.coe` `MeasurableEquiv` `EuclideanSpace` `Real` `WithLp.measurableSpace` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `MeasurableSpace.pi` `Real.measurableSpace` `EquivLike.toFunLike` `MeasurableEquiv.instEquivLike` `measurableEquiv` `WithLp.ofLp`	—	—
`coe_measurableEquiv_symm` 📖	mathematical	—	`DFunLike.coe` `MeasurableEquiv` `EuclideanSpace` `Real` `MeasurableSpace.pi` `Real.measurableSpace` `WithLp.measurableSpace` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `EquivLike.toFunLike` `MeasurableEquiv.instEquivLike` `MeasurableEquiv.symm` `measurableEquiv` `WithLp.toLp` `Nat.instAtLeastTwoHAddOfNat`	—	—
`measurableEquiv_toEquiv` 📖	mathematical	—	`MeasurableEquiv.toEquiv` `EuclideanSpace` `Real` `WithLp.measurableSpace` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `MeasurableSpace.pi` `Real.measurableSpace` `measurableEquiv` `WithLp.equiv` `Nat.instAtLeastTwoHAddOfNat`	—	—
`volume_preserving_symm_measurableEquiv_toLp` 📖	mathematical	—	`MeasureTheory.MeasurePreserving` `WithLp` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Nat.instAtLeastTwoHAddOfNat` `WithLp.measurableSpace` `MeasurableSpace.pi` `Real` `Real.measurableSpace` `DFunLike.coe` `MeasurableEquiv` `EquivLike.toFunLike` `MeasurableEquiv.instEquivLike` `MeasurableEquiv.symm` `MeasurableEquiv.toLp` `MeasureTheory.MeasureSpace.volume` `measureSpaceOfInnerProductSpace` `PiLp.normedAddCommGroup` `fact_one_le_two_ennreal` `Real.normedAddCommGroup` `PiLp.innerProductSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `WithLp.instModuleFinite` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `Real.instDivisionRing` `Pi.addCommGroup` `SeminormedAddCommGroup.toAddCommGroup` `Pi.module` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `AddCommGroup.toAddCommMonoid` `NormedSpace.toModule` `FiniteDimensional.finiteDimensional_pi'` `Finite.of_fintype` `FiniteDimensional.rclike_to_real` `PiLp.borelSpace` `Finite.to_countable` `UniformSpace.toTopologicalSpace` `Real.borelSpace` `instSecondCountableTopologyReal` `MeasureTheory.MeasureSpace.pi` `Real.measureSpace`	—	`Nat.instAtLeastTwoHAddOfNat` `fact_one_le_two_ennreal` `WithLp.instModuleFinite` `FiniteDimensional.finiteDimensional_pi'` `Finite.of_fintype` `FiniteDimensional.rclike_to_real` `PiLp.borelSpace` `Finite.to_countable` `Real.borelSpace` `instSecondCountableTopologyReal` `Pi.topologicalAddGroup` `instIsTopologicalAddGroupReal` `Pi.borelSpace` `MeasureTheory.addHaarMeasure_eq_volume_pi` `Module.Basis.parallelepiped_basisFun` `Module.Basis.addHaar_def` `MeasurableEquiv.coe_toLp` `RingHomInvPair.ids` `PiLp.coe_symm_continuousLinearEquiv` `Module.Basis.map_addHaar` `PiLp.secondCountableTopology` `SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `instWeaklyLocallyCompactSpaceOfLocallyCompactSpace` `locallyCompact_of_proper` `FiniteDimensional.proper_real` `OrthonormalBasis.addHaar_eq_volume` `MeasureTheory.MeasurePreserving.symm` `Measurable.measurePreserving` `MeasurableEquiv.measurable`

LinearIsometryEquiv

Definitions

Name	Category	Theorems
`toMeasurableEquiv` 📖	CompOp	3 math math: `coe_toMeasurableEquiv`, `toMeasurableEquiv_symm`, `coe_symm_toMeasurableEquiv`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_symm_toMeasurableEquiv` 📖	mathematical	—	`DFunLike.coe` `MeasurableEquiv` `EquivLike.toFunLike` `MeasurableEquiv.instEquivLike` `MeasurableEquiv.symm` `toMeasurableEquiv` `LinearIsometryEquiv` `Real` `Real.semiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `Real.normedField` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `instEquivLike` `symm`	—	`RingHomInvPair.ids`
`coe_toMeasurableEquiv` 📖	mathematical	—	`DFunLike.coe` `MeasurableEquiv` `EquivLike.toFunLike` `MeasurableEquiv.instEquivLike` `toMeasurableEquiv` `LinearIsometryEquiv` `Real` `Real.semiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `Real.normedField` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `instEquivLike`	—	`RingHomInvPair.ids`
`measurePreserving` 📖	mathematical	—	`MeasureTheory.MeasurePreserving` `DFunLike.coe` `LinearIsometryEquiv` `Real` `Real.semiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `Real.normedField` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `EquivLike.toFunLike` `instEquivLike` `MeasureTheory.MeasureSpace.volume` `measureSpaceOfInnerProductSpace`	—	`RingHomInvPair.ids` `Continuous.measurable` `BorelSpace.opensMeasurable` `continuous` `exists_orthonormalBasis` `OrthonormalBasis.addHaar_eq_volume` `Module.Basis.map_addHaar` `secondCountable_of_proper` `FiniteDimensional.proper_real` `SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `instWeaklyLocallyCompactSpaceOfLocallyCompactSpace` `locallyCompact_of_proper`
`toMeasurableEquiv_symm` 📖	mathematical	—	`toMeasurableEquiv` `symm` `Real` `Real.semiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `Real.normedField` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `MeasurableEquiv.symm`	—	`RingHomInvPair.ids`

Orientation

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`measure_eq_volume` 📖	mathematical	—	`AlternatingMap.measure` `InnerProductSpace.toNormedSpace` `Real` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `volumeForm` `MeasureTheory.MeasureSpace.volume` `measureSpaceOfInnerProductSpace`	—	`Real.instIsStrictOrderedRing` `measure_orthonormalBasis` `IsScalarTower.right` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `MeasureTheory.Measure.addHaarMeasure_unique` `secondCountable_of_proper` `FiniteDimensional.proper_real` `MeasureTheory.sigmaFinite_of_locallyFinite` `MeasureTheory.Measure.instIsLocallyFiniteMeasureMeasure` `MeasureTheory.Measure.instIsAddLeftInvariantMeasure` `one_smul` `Module.Basis.addHaar_def`
`measure_orthonormalBasis` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `AlternatingMap.measure` `InnerProductSpace.toNormedSpace` `Real` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `volumeForm` `parallelepiped` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `OrthonormalBasis` `OrthonormalBasis.instFunLike` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal`	—	`Real.instIsStrictOrderedRing` `Fact.out` `Module.finrank_eq_card_basis` `commRing_strongRankCondition` `Real.instNontrivial` `OrthonormalBasis.coe_reindex` `Equiv.symm_apply_apply` `parallelepiped_comp_equiv` `AlternatingMap.measure_parallelepiped` `abs_volumeForm_apply_of_orthonormal` `ENNReal.ofReal_one`

OrthonormalBasis

Definitions

Name	Category	Theorems
`measurableEquiv` 📖	CompOp	1 math math: `measurePreserving_measurableEquiv`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`addHaar_eq_volume` 📖	mathematical	—	`Module.Basis.addHaar` `InnerProductSpace.toNormedSpace` `Real` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `toBasis` `MeasureTheory.MeasureSpace.volume` `measureSpaceOfInnerProductSpace`	—	`Module.Basis.addHaar_eq_iff` `secondCountable_of_proper` `FiniteDimensional.proper_real` `MeasureTheory.Measure.IsAddHaarMeasure.sigmaFinite` `instIsAddHaarMeasureVolume` `SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `instWeaklyLocallyCompactSpaceOfLocallyCompactSpace` `locallyCompact_of_proper` `MeasureTheory.Measure.IsAddHaarMeasure.toIsAddLeftInvariant` `volume_parallelepiped`
`measurePreserving_measurableEquiv` 📖	mathematical	—	`MeasureTheory.MeasurePreserving` `EuclideanSpace` `Real` `MeasureTheory.MeasureSpace.toMeasurableSpace` `measureSpaceOfInnerProductSpace` `PiLp.normedAddCommGroup` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `fact_one_le_two_ennreal` `Real.normedAddCommGroup` `PiLp.innerProductSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `WithLp.instModuleFinite` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `Real.instDivisionRing` `Pi.addCommGroup` `SeminormedAddCommGroup.toAddCommGroup` `Pi.module` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `AddCommGroup.toAddCommMonoid` `NormedSpace.toModule` `FiniteDimensional.finiteDimensional_pi'` `Finite.of_fintype` `FiniteDimensional.rclike_to_real` `WithLp.measurableSpace` `MeasurableSpace.pi` `Real.measurableSpace` `PiLp.borelSpace` `Finite.to_countable` `UniformSpace.toTopologicalSpace` `Real.borelSpace` `instSecondCountableTopologyReal` `DFunLike.coe` `MeasurableEquiv` `EquivLike.toFunLike` `MeasurableEquiv.instEquivLike` `measurableEquiv` `MeasureTheory.MeasureSpace.volume`	—	`fact_one_le_two_ennreal` `WithLp.instModuleFinite` `FiniteDimensional.finiteDimensional_pi'` `Finite.of_fintype` `FiniteDimensional.rclike_to_real` `PiLp.borelSpace` `Finite.to_countable` `Real.borelSpace` `instSecondCountableTopologyReal` `addHaar_eq_volume` `MeasurableEquiv.coe_toEquiv_symm` `RingHomInvPair.ids` `Module.Basis.map_addHaar` `secondCountable_of_proper` `FiniteDimensional.proper_real` `SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `instWeaklyLocallyCompactSpaceOfLocallyCompactSpace` `locallyCompact_of_proper` `MeasureTheory.MeasurePreserving.symm` `Measurable.measurePreserving` `MeasurableEquiv.measurable`
`measurePreserving_repr` 📖	mathematical	—	`MeasureTheory.MeasurePreserving` `EuclideanSpace` `Real` `MeasureTheory.MeasureSpace.toMeasurableSpace` `measureSpaceOfInnerProductSpace` `PiLp.normedAddCommGroup` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `fact_one_le_two_ennreal` `Real.normedAddCommGroup` `PiLp.innerProductSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `WithLp.instModuleFinite` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `Real.instDivisionRing` `Pi.addCommGroup` `SeminormedAddCommGroup.toAddCommGroup` `Pi.module` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `AddCommGroup.toAddCommMonoid` `NormedSpace.toModule` `FiniteDimensional.finiteDimensional_pi'` `Finite.of_fintype` `FiniteDimensional.rclike_to_real` `WithLp.measurableSpace` `MeasurableSpace.pi` `Real.measurableSpace` `PiLp.borelSpace` `Finite.to_countable` `UniformSpace.toTopologicalSpace` `Real.borelSpace` `instSecondCountableTopologyReal` `DFunLike.coe` `LinearIsometryEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `NormedAddCommGroup.toSeminormedAddCommGroup` `PiLp.seminormedAddCommGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `InnerProductSpace.toNormedSpace` `WithLp.instModule` `Pi.Function.module` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `SeminormedRing.toRing` `SeminormedCommRing.toSeminormedRing` `RCLike.innerProductSpace` `EquivLike.toFunLike` `LinearIsometryEquiv.instEquivLike` `repr` `MeasureTheory.MeasureSpace.volume`	—	`measurePreserving_measurableEquiv`
`measurePreserving_repr_symm` 📖	mathematical	—	`MeasureTheory.MeasurePreserving` `EuclideanSpace` `Real` `MeasureTheory.MeasureSpace.toMeasurableSpace` `measureSpaceOfInnerProductSpace` `PiLp.normedAddCommGroup` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `fact_one_le_two_ennreal` `Real.normedAddCommGroup` `PiLp.innerProductSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `WithLp.instModuleFinite` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `Real.instDivisionRing` `Pi.addCommGroup` `SeminormedAddCommGroup.toAddCommGroup` `Pi.module` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `AddCommGroup.toAddCommMonoid` `NormedSpace.toModule` `FiniteDimensional.finiteDimensional_pi'` `Finite.of_fintype` `FiniteDimensional.rclike_to_real` `WithLp.measurableSpace` `MeasurableSpace.pi` `Real.measurableSpace` `PiLp.borelSpace` `Finite.to_countable` `UniformSpace.toTopologicalSpace` `Real.borelSpace` `instSecondCountableTopologyReal` `DFunLike.coe` `LinearIsometryEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `PiLp.seminormedAddCommGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `NormedAddCommGroup.toSeminormedAddCommGroup` `WithLp.instModule` `Pi.Function.module` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `SeminormedRing.toRing` `SeminormedCommRing.toSeminormedRing` `InnerProductSpace.toNormedSpace` `RCLike.innerProductSpace` `EquivLike.toFunLike` `LinearIsometryEquiv.instEquivLike` `LinearIsometryEquiv.symm` `repr` `MeasureTheory.MeasureSpace.volume`	—	`MeasureTheory.MeasurePreserving.symm` `fact_one_le_two_ennreal` `WithLp.instModuleFinite` `FiniteDimensional.finiteDimensional_pi'` `Finite.of_fintype` `FiniteDimensional.rclike_to_real` `PiLp.borelSpace` `Finite.to_countable` `Real.borelSpace` `instSecondCountableTopologyReal` `measurePreserving_measurableEquiv`
`volume_parallelepiped` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.Measure` `MeasureTheory.MeasureSpace.toMeasurableSpace` `measureSpaceOfInnerProductSpace` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `MeasureTheory.MeasureSpace.volume` `parallelepiped` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `OrthonormalBasis` `instFunLike` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal`	—	`Real.instIsStrictOrderedRing` `Orientation.measure_eq_volume` `Orientation.measure_orthonormalBasis`

PiLp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`volume_preserving_ofLp` 📖	mathematical	—	`MeasureTheory.MeasurePreserving` `WithLp` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Nat.instAtLeastTwoHAddOfNat` `WithLp.measurableSpace` `MeasurableSpace.pi` `Real` `Real.measurableSpace` `WithLp.ofLp` `MeasureTheory.MeasureSpace.volume` `measureSpaceOfInnerProductSpace` `normedAddCommGroup` `fact_one_le_two_ennreal` `Real.normedAddCommGroup` `innerProductSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `WithLp.instModuleFinite` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `Real.instDivisionRing` `Pi.addCommGroup` `SeminormedAddCommGroup.toAddCommGroup` `Pi.module` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `AddCommGroup.toAddCommMonoid` `NormedSpace.toModule` `FiniteDimensional.finiteDimensional_pi'` `Finite.of_fintype` `FiniteDimensional.rclike_to_real` `borelSpace` `Finite.to_countable` `UniformSpace.toTopologicalSpace` `Real.borelSpace` `instSecondCountableTopologyReal` `MeasureTheory.MeasureSpace.pi` `Real.measureSpace`	—	`EuclideanSpace.volume_preserving_symm_measurableEquiv_toLp`
`volume_preserving_toLp` 📖	mathematical	—	`MeasureTheory.MeasurePreserving` `WithLp` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Nat.instAtLeastTwoHAddOfNat` `MeasurableSpace.pi` `Real` `Real.measurableSpace` `WithLp.measurableSpace` `WithLp.toLp` `MeasureTheory.MeasureSpace.volume` `MeasureTheory.MeasureSpace.pi` `Real.measureSpace` `measureSpaceOfInnerProductSpace` `normedAddCommGroup` `fact_one_le_two_ennreal` `Real.normedAddCommGroup` `innerProductSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `WithLp.instModuleFinite` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `Real.instDivisionRing` `Pi.addCommGroup` `SeminormedAddCommGroup.toAddCommGroup` `Pi.module` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `AddCommGroup.toAddCommMonoid` `NormedSpace.toModule` `FiniteDimensional.finiteDimensional_pi'` `Finite.of_fintype` `FiniteDimensional.rclike_to_real` `borelSpace` `Finite.to_countable` `UniformSpace.toTopologicalSpace` `Real.borelSpace` `instSecondCountableTopologyReal`	—	`MeasureTheory.MeasurePreserving.symm` `Nat.instAtLeastTwoHAddOfNat` `fact_one_le_two_ennreal` `WithLp.instModuleFinite` `FiniteDimensional.finiteDimensional_pi'` `Finite.of_fintype` `FiniteDimensional.rclike_to_real` `borelSpace` `Finite.to_countable` `Real.borelSpace` `instSecondCountableTopologyReal` `EuclideanSpace.volume_preserving_symm_measurableEquiv_toLp`

WithLp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`volume_preserving_ofLp` 📖	mathematical	—	`MeasureTheory.MeasurePreserving` `WithLp` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Nat.instAtLeastTwoHAddOfNat` `measurableSpace` `Prod.instMeasurableSpace` `ofLp` `MeasureTheory.MeasureSpace.volume` `measureSpaceOfInnerProductSpace` `instProdNormedAddCommGroup` `fact_one_le_two_ennreal` `instProdInnerProductSpace` `Real` `Real.instRCLike` `instModuleFinite` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `Real.instDivisionRing` `Prod.instAddCommGroup` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `Prod.instModule` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `AddCommGroup.toAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `Module.instFiniteDimensionalOfIsReflexive` `NormedAddCommGroup.toAddCommGroup` `Prod.instModuleIsReflexive` `Semifield.toCommSemiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Module.instIsReflexiveOfFiniteOfProjective` `Module.Projective.of_free` `CommSemiring.toSemiring` `Module.Free.of_divisionRing` `borelSpace` `PseudoEMetricSpace.toUniformSpace` `PseudoMetricSpace.toPseudoEMetricSpace` `secondCountableTopologyEither_of_right` `UniformSpace.secondCountable_of_separable` `EMetric.instIsCountablyGeneratedUniformity` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `secondCountable_of_proper` `FiniteDimensional.proper_real` `MeasureTheory.Measure.prod.measureSpace`	—	`volume_preserving_symm_measurableEquiv_toLp_prod`
`volume_preserving_symm_measurableEquiv_toLp_prod` 📖	mathematical	—	`MeasureTheory.MeasurePreserving` `WithLp` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Nat.instAtLeastTwoHAddOfNat` `measurableSpace` `Prod.instMeasurableSpace` `DFunLike.coe` `MeasurableEquiv` `EquivLike.toFunLike` `MeasurableEquiv.instEquivLike` `MeasurableEquiv.symm` `MeasurableEquiv.toLp` `MeasureTheory.MeasureSpace.volume` `measureSpaceOfInnerProductSpace` `instProdNormedAddCommGroup` `fact_one_le_two_ennreal` `instProdInnerProductSpace` `Real` `Real.instRCLike` `instModuleFinite` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `Real.instDivisionRing` `Prod.instAddCommGroup` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `Prod.instModule` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `AddCommGroup.toAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `Module.instFiniteDimensionalOfIsReflexive` `NormedAddCommGroup.toAddCommGroup` `Prod.instModuleIsReflexive` `Semifield.toCommSemiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Module.instIsReflexiveOfFiniteOfProjective` `Module.Projective.of_free` `CommSemiring.toSemiring` `Module.Free.of_divisionRing` `borelSpace` `PseudoEMetricSpace.toUniformSpace` `PseudoMetricSpace.toPseudoEMetricSpace` `secondCountableTopologyEither_of_right` `UniformSpace.secondCountable_of_separable` `EMetric.instIsCountablyGeneratedUniformity` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `secondCountable_of_proper` `FiniteDimensional.proper_real` `MeasureTheory.Measure.prod.measureSpace`	—	`Nat.instAtLeastTwoHAddOfNat` `fact_one_le_two_ennreal` `instModuleFinite` `Module.instFiniteDimensionalOfIsReflexive` `Prod.instModuleIsReflexive` `Module.instIsReflexiveOfFiniteOfProjective` `Module.Projective.of_free` `Module.Free.of_divisionRing` `borelSpace` `secondCountableTopologyEither_of_right` `UniformSpace.secondCountable_of_separable` `EMetric.instIsCountablyGeneratedUniformity` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `secondCountable_of_proper` `FiniteDimensional.proper_real` `MeasureTheory.MeasurePreserving.trans` `RingHomInvPair.ids` `FiniteDimensional.finiteDimensional_pi'` `Finite.instSum` `Finite.of_fintype` `FiniteDimensional.rclike_to_real` `PiLp.borelSpace` `instCountableSum` `instCountableFin` `Real.borelSpace` `instSecondCountableTopologyReal` `LinearIsometryEquiv.measurePreserving` `Finite.to_countable` `EuclideanSpace.volume_preserving_symm_measurableEquiv_toLp` `MeasureTheory.measurePreserving_sumPiEquivProdPi` `MeasureTheory.Measure.IsAddHaarMeasure.sigmaFinite` `instIsAddHaarMeasureVolume` `SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace` `instIsTopologicalAddGroupReal` `instWeaklyLocallyCompactSpaceOfLocallyCompactSpace` `locallyCompact_of_proper` `instProperSpaceReal` `MeasureTheory.MeasurePreserving.prod` `MeasureTheory.instSFiniteOfSigmaFinite` `MeasureTheory.Measure.pi.sigmaFinite` `MeasureTheory.MeasurePreserving.symm` `MeasurableEquiv.ext` `MeasurableEquiv.coe_sumPiEquivProdPi` `LinearIsometryEquiv.symm_apply_apply`
`volume_preserving_toLp` 📖	mathematical	—	`MeasureTheory.MeasurePreserving` `WithLp` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Nat.instAtLeastTwoHAddOfNat` `Prod.instMeasurableSpace` `measurableSpace` `toLp` `MeasureTheory.MeasureSpace.volume` `MeasureTheory.Measure.prod.measureSpace` `measureSpaceOfInnerProductSpace` `instProdNormedAddCommGroup` `fact_one_le_two_ennreal` `instProdInnerProductSpace` `Real` `Real.instRCLike` `instModuleFinite` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `Real.instDivisionRing` `Prod.instAddCommGroup` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `Prod.instModule` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `AddCommGroup.toAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `Module.instFiniteDimensionalOfIsReflexive` `NormedAddCommGroup.toAddCommGroup` `Prod.instModuleIsReflexive` `Semifield.toCommSemiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Module.instIsReflexiveOfFiniteOfProjective` `Module.Projective.of_free` `CommSemiring.toSemiring` `Module.Free.of_divisionRing` `borelSpace` `PseudoEMetricSpace.toUniformSpace` `PseudoMetricSpace.toPseudoEMetricSpace` `secondCountableTopologyEither_of_right` `UniformSpace.secondCountable_of_separable` `EMetric.instIsCountablyGeneratedUniformity` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `secondCountable_of_proper` `FiniteDimensional.proper_real`	—	`MeasureTheory.MeasurePreserving.symm` `Nat.instAtLeastTwoHAddOfNat` `fact_one_le_two_ennreal` `instModuleFinite` `Module.instFiniteDimensionalOfIsReflexive` `Prod.instModuleIsReflexive` `Module.instIsReflexiveOfFiniteOfProjective` `Module.Projective.of_free` `Module.Free.of_divisionRing` `borelSpace` `secondCountableTopologyEither_of_right` `UniformSpace.secondCountable_of_separable` `EMetric.instIsCountablyGeneratedUniformity` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `secondCountable_of_proper` `FiniteDimensional.proper_real` `volume_preserving_symm_measurableEquiv_toLp_prod`

(root)

Definitions

Name	Category	Theorems
`InnerProductSpace` 📖	CompData	1 math math: `nonempty_innerProductSpace`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`volume_euclideanSpace_eq_dirac` 📖	mathematical	—	`MeasureTheory.MeasureSpace.volume` `EuclideanSpace` `Real` `measureSpaceOfInnerProductSpace` `PiLp.normedAddCommGroup` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `fact_one_le_two_ennreal` `Real.normedAddCommGroup` `PiLp.innerProductSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `WithLp.instModuleFinite` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `Real.instDivisionRing` `Pi.addCommGroup` `SeminormedAddCommGroup.toAddCommGroup` `Pi.module` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `AddCommGroup.toAddCommMonoid` `NormedSpace.toModule` `FiniteDimensional.finiteDimensional_pi'` `Finite.of_fintype` `FiniteDimensional.rclike_to_real` `WithLp.measurableSpace` `MeasurableSpace.pi` `Real.measurableSpace` `PiLp.borelSpace` `Encodable.countable` `IsEmpty.toEncodable` `UniformSpace.toTopologicalSpace` `Real.borelSpace` `instSecondCountableTopologyReal` `MeasureTheory.Measure.dirac` `MeasureTheory.MeasureSpace.toMeasurableSpace` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `WithLp.instAddCommGroup` `Real.instAddCommGroup`	—	`fact_one_le_two_ennreal` `WithLp.instModuleFinite` `FiniteDimensional.finiteDimensional_pi'` `Finite.of_fintype` `FiniteDimensional.rclike_to_real` `PiLp.borelSpace` `Encodable.countable` `Real.borelSpace` `instSecondCountableTopologyReal` `Nat.instAtLeastTwoHAddOfNat` `Finite.to_countable` `MeasureTheory.MeasurePreserving.map_eq` `PiLp.volume_preserving_toLp` `MeasureTheory.Measure.volume_pi_eq_dirac` `MeasureTheory.Measure.map_dirac` `Pi.instMeasurableSingletonClass` `instMeasurableSingletonClassOfMeasurableEq` `instMeasurableEqOfSecondCountableTopologyOfT2Space` `BorelSpace.opensMeasurable` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `PiLp.secondCountableTopology` `WithLp.toLp_zero`

---

← Back to Index