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_euclideanSpace_eq_dirac	18
Total	22

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

(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 WithLp.measurable_toLp WithLp.toLp_zero

---

← Back to Index