Documentation Verification Report

HaarToSphere

📁 Source: Mathlib/MeasureTheory/Constructions/HaarToSphere.lean

Statistics

Metric	Count
Definitions `finiteSpanningSetsIn_volumeIoiPow_range_Iio`, `toSphere`, `toSphereBallBound`, `volumeIoiPow`	4
Theorems `instIsFiniteMeasureElemSphereOfNatRealToSphere`, `instSigmaFiniteElemRealIoiOfNatVolumeIoiPow`, `measurePreserving_homeomorphUnitSphereProd`, `instIsOpenPosMeasure`, `toSphereBallBound_mul_measureReal_unitBall_le_toSphere_ball`, `toSphereBallBound_mul_measure_unitBall_le_toSphere_ball`, `toSphereBallBound_pos`, `toSphere_apply'`, `toSphere_apply_aux`, `toSphere_apply_univ`, `toSphere_apply_univ'`, `toSphere_eq_zero_iff`, `toSphere_eq_zero_iff_finrank`, `toSphere_ne_zero`, `toSphere_real_apply_univ`, `volumeIoiPow_apply_Iio`, `integrable_fun_norm_addHaar`, `integral_fun_norm_addHaar`	18
Total	22

MeasureTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`integrable_fun_norm_addHaar` 📖	mathematical	—	`Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `Norm.norm` `NormedAddCommGroup.toNorm` `IntegrableOn` `Real` `MeasureSpace.toMeasurableSpace` `Real.measureSpace` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `Monoid.toNatPow` `Module.finrank` `Set.Ioi` `Real.instPreorder` `Real.instZero` `MeasureSpace.volume`	—	`MeasurePreserving.integrable_comp_emb` `Measure.measurePreserving_homeomorphUnitSphereProd` `Homeomorph.measurableEmbedding` `Subtype.borelSpace` `Prod.borelSpace` `Real.borelSpace` `secondCountableTopologyEither_of_right` `TopologicalSpace.Subtype.secondCountableTopology` `instSecondCountableTopologyReal` `restrict_compl_singleton` `Measure.IsAddHaarMeasure.noAtoms` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `T5Space.toT1Space` `T6Space.toT5Space` `instT6SpaceOfMetrizableSpace` `EMetricSpace.metrizableSpace` `instWeaklyLocallyCompactSpaceOfLocallyCompactSpace` `locallyCompact_of_proper` `FiniteDimensional.proper_real` `PerfectSpace.not_isolated` `instPerfectSpaceOfT1SpaceOfConnectedSpaceOfNontrivial` `PathConnectedSpace.connectedSpace` `NormedSpace.instPathConnectedSpace` `IntegrableOn.eq_1` `integrableOn_iff_comap_subtypeVal` `instMeasurableSingletonClassOfMeasurableEq` `instMeasurableEqOfSecondCountableTopologyOfT2Space` `BorelSpace.opensMeasurable` `secondCountable_of_proper` `TopologicalSpace.t2Space_of_metrizableSpace` `homeomorphUnitSphereProd_apply_snd_coe` `Integrable.comp_snd_iff` `instSFiniteOfSigmaFinite` `Measure.instSigmaFiniteElemRealIoiOfNatVolumeIoiPow` `Measure.instIsFiniteMeasureElemSphereOfNatRealToSphere` `instClosedIicTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid` `Measure.volumeIoiPow.eq_1` `integrable_withDensity_iff_integrable_smul'` `Measurable.ennreal_ofReal` `Measurable.pow_const` `Monoid.measurablePow` `ContinuousMul.measurableMul₂` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `Measurable.subtype_coe` `measurable_id'` `Measure.instOuterMeasureClass` `integrable_congr` `Filter.Eventually.of_forall` `ENNReal.ofReal_pow` `le_of_lt` `ENNReal.toReal_pow` `ENNReal.toReal_ofReal`
`integral_fun_norm_addHaar` 📖	mathematical	—	`integral` `Norm.norm` `NormedAddCommGroup.toNorm` `AddMonoid.toNatSMul` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Module.finrank` `Real` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Measure.real` `Metric.ball` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `Real.instOne` `MeasureSpace.toMeasurableSpace` `Real.measureSpace` `Measure.restrict` `MeasureSpace.volume` `Set.Ioi` `Real.instPreorder` `Real.instZero` `Monoid.toNatPow`	—	`integral_subtype_comap` `MeasurableSet.compl` `MeasurableSingletonClass.measurableSet_singleton` `instMeasurableSingletonClassOfMeasurableEq` `instMeasurableEqOfSecondCountableTopologyOfT2Space` `BorelSpace.opensMeasurable` `secondCountable_of_proper` `FiniteDimensional.proper_real` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `restrict_compl_singleton` `Measure.IsAddHaarMeasure.noAtoms` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `T5Space.toT1Space` `T6Space.toT5Space` `instT6SpaceOfMetrizableSpace` `instWeaklyLocallyCompactSpaceOfLocallyCompactSpace` `locallyCompact_of_proper` `PerfectSpace.not_isolated` `instPerfectSpaceOfT1SpaceOfConnectedSpaceOfNontrivial` `PathConnectedSpace.connectedSpace` `NormedSpace.instPathConnectedSpace` `homeomorphUnitSphereProd_apply_snd_coe` `MeasurePreserving.integral_comp` `Measure.measurePreserving_homeomorphUnitSphereProd` `Homeomorph.measurableEmbedding` `Subtype.borelSpace` `Prod.borelSpace` `Real.borelSpace` `secondCountableTopologyEither_of_right` `TopologicalSpace.Subtype.secondCountableTopology` `instSecondCountableTopologyReal` `integral_fun_snd` `instSFiniteOfSigmaFinite` `Measure.instSigmaFiniteElemRealIoiOfNatVolumeIoiPow` `sigmaFinite_of_locallyFinite` `IsFiniteMeasure.toIsLocallyFiniteMeasure` `Measure.instIsFiniteMeasureElemSphereOfNatRealToSphere` `integral_withDensity_eq_integral_smul` `Measurable.real_toNNReal` `Measurable.pow_const` `Monoid.measurablePow` `ContinuousMul.measurableMul₂` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `measurable_subtype_coe` `Measure.toSphere_real_apply_univ` `nsmul_eq_mul` `smul_assoc` `AddCommMonoid.nat_isScalarTower` `measurableSet_Ioi` `instClosedIicTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid` `setIntegral_congr_fun` `NNReal.smul_def` `Real.coe_toNNReal` `pow_nonneg` `Real.instZeroLEOneClass` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `LT.lt.le` `Membership.mem.out`

MeasureTheory.Measure

Definitions

Name	Category	Theorems
`finiteSpanningSetsIn_volumeIoiPow_range_Iio` 📖	CompOp	—
`toSphere` 📖	CompOp	11 math math: `toSphere_real_apply_univ`, `toSphere_apply_univ`, `instIsFiniteMeasureElemSphereOfNatRealToSphere`, `toSphere_apply'`, `measurePreserving_homeomorphUnitSphereProd`, `toSphereBallBound_mul_measureReal_unitBall_le_toSphere_ball`, `toSphereBallBound_mul_measure_unitBall_le_toSphere_ball`, `toSphere_eq_zero_iff_finrank`, `toSphere.instIsOpenPosMeasure`, `toSphere_apply_univ'`, `toSphere_eq_zero_iff`
`toSphereBallBound` 📖	CompOp	3 math math: `toSphereBallBound_mul_measureReal_unitBall_le_toSphere_ball`, `toSphereBallBound_mul_measure_unitBall_le_toSphere_ball`, `toSphereBallBound_pos`
`volumeIoiPow` 📖	CompOp	3 math math: `measurePreserving_homeomorphUnitSphereProd`, `instSigmaFiniteElemRealIoiOfNatVolumeIoiPow`, `volumeIoiPow_apply_Iio`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsFiniteMeasureElemSphereOfNatRealToSphere` 📖	mathematical	—	`MeasureTheory.IsFiniteMeasure` `Set.Elem` `Metric.sphere` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `Real` `Real.instOne` `Subtype.instMeasurableSpace` `Set` `Set.instMembership` `toSphere`	—	`toSphere_apply_univ'` `ENNReal.mul_lt_top` `ENNReal.natCast_lt_top` `LT.lt.trans_le'` `MeasureTheory.measure_ball_lt_top` `FiniteDimensional.proper_real` `IsAddHaarMeasure.toIsFiniteMeasureOnCompacts` `MeasureTheory.measure_mono` `instOuterMeasureClass` `Set.diff_subset`
`instSigmaFiniteElemRealIoiOfNatVolumeIoiPow` 📖	mathematical	—	`MeasureTheory.SigmaFinite` `Set.Elem` `Real` `Set.Ioi` `Real.instPreorder` `Real.instZero` `Subtype.instMeasurableSpace` `Set` `Set.instMembership` `Real.measurableSpace` `volumeIoiPow`	—	`FiniteSpanningSetsIn.sigmaFinite`
`measurePreserving_homeomorphUnitSphereProd` 📖	mathematical	—	`MeasureTheory.MeasurePreserving` `Set.Elem` `Compl.compl` `Set` `Set.instCompl` `Set.instSingletonSet` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `Metric.sphere` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Real` `Real.instOne` `Set.Ioi` `Real.instPreorder` `Real.instZero` `Subtype.instMeasurableSpace` `Set.instMembership` `Prod.instMeasurableSpace` `Real.measurableSpace` `DFunLike.coe` `Homeomorph` `instTopologicalSpaceSubtype` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `instTopologicalSpaceProd` `Real.pseudoMetricSpace` `EquivLike.toFunLike` `Homeomorph.instEquivLike` `homeomorphUnitSphereProd` `comap` `prod` `toSphere` `volumeIoiPow` `Module.finrank` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real.normedField`	—	`Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim` `Module.finrank_zero_of_subsingleton` `Real.instNontrivial` `zero_tsub` `Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub` `Prod.isEmpty_left` `Metric.sphere_isEmpty_of_subsingleton` `NeZero.charZero_one` `RCLike.charZero_rclike` `Homeomorph.measurable` `Subtype.opensMeasurableSpace` `BorelSpace.opensMeasurable` `Prod.borelSpace` `Subtype.borelSpace` `Real.borelSpace` `secondCountableTopologyEither_of_right` `TopologicalSpace.Subtype.secondCountableTopology` `instSecondCountableTopologyReal` `prod_eq_generateFrom` `MeasurableSpace.generateFrom_measurableSet` `borel_eq_generateFrom_Iio` `orderTopology_of_ordConnected` `instOrderTopologyReal` `Set.ordConnected_Ioi` `BorelSpace.measurable_eq` `MeasurableSpace.isPiSystem_measurableSet` `isPiSystem_Iio` `MeasureTheory.sigmaFinite_of_locallyFinite` `secondCountable_of_proper` `FiniteDimensional.proper_real` `MeasureTheory.IsFiniteMeasure.toIsLocallyFiniteMeasure` `instIsFiniteMeasureElemSphereOfNatRealToSphere` `Set.forall_mem_range` `LinearOrderedField.smul_Ioo` `Real.instIsStrictOrderedRing` `Membership.mem.out` `MulZeroClass.mul_zero` `mul_one` `Module.finrank_pos` `commRing_strongRankCondition` `Real.instIsDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `MeasurableEmbedding.map_apply` `Homeomorph.measurableEmbedding` `toSphere_apply'` `volumeIoiPow_apply_Iio` `comap_subtype_coe_apply` `MeasurableSet.compl` `MeasurableSingletonClass.measurableSet_singleton` `instMeasurableSingletonClassOfMeasurableEq` `instMeasurableEqOfSecondCountableTopologyOfT2Space` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `toSphere_apply_aux` `smul_assoc` `Set.isScalarTower'` `IsScalarTower.left` `addHaar_smul_of_nonneg` `LT.lt.le` `Nat.cast_pred` `sub_add_cancel` `mul_right_comm` `ENNReal.ofReal_natCast` `ENNReal.ofReal_mul` `Nat.cast_nonneg` `Real.instIsOrderedRing` `mul_div_cancel₀` `LT.lt.ne'` `Nat.cast_pos`
`toSphereBallBound_mul_measureReal_unitBall_le_toSphere_ball` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`Real.instLE` `Real.instMul` `NNReal.toReal` `toSphereBallBound` `Module.finrank` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `real` `Metric.ball` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `Real.instOne` `Set.Elem` `Metric.sphere` `Subtype.instMeasurableSpace` `Set` `Set.instMembership` `toSphere` `Subtype.pseudoMetricSpace`	—	`real.eq_1` `le_imp_le_of_le_of_le` `le_refl` `ENNReal.toReal_mono` `instIsFiniteMeasureElemSphereOfNatRealToSphere` `toSphereBallBound_mul_measure_unitBall_le_toSphere_ball` `ENNReal.toReal_mul` `ENNReal.coe_toReal`
`toSphereBallBound_mul_measure_unitBall_le_toSphere_ball` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.ofNNReal` `toSphereBallBound` `Module.finrank` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `DFunLike.coe` `MeasureTheory.Measure` `Set` `instFunLike` `Metric.ball` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `Real.instOne` `Set.Elem` `Metric.sphere` `Subtype.instMeasurableSpace` `Set.instMembership` `toSphere` `Subtype.pseudoMetricSpace`	—	`norm_eq_of_mem_sphere` `norm_zero` `NeZero.charZero_one` `RCLike.charZero_rclike` `Nat.instAtLeastTwoHAddOfNat` `toSphere_apply'` `measurableSet_ball` `Subtype.opensMeasurableSpace` `BorelSpace.opensMeasurable` `Subtype.image_ball` `Set.setOf_mem_eq` `le_imp_le_of_le_of_le` `le_refl` `mul_le_mul_right` `IsOrderedMonoid.toMulLeftMono` `ENNReal.instIsOrderedMonoid` `MeasureTheory.measure_mono` `instOuterMeasureClass` `LT.lt.ne'` `Module.finrank_pos` `commRing_strongRankCondition` `Real.instNontrivial` `Real.instIsDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `toSphereBallBound.eq_1` `ENNReal.coe_div` `ne_of_gt` `Mathlib.Meta.Positivity.pos_of_isNat` `NNReal.instIsOrderedRing` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `mul_assoc` `addHaar_ball_of_pos` `div_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `Real.instIsOrderedRing` `ENNReal.ofReal_pow` `le_of_lt` `ENNReal.ofReal_div_of_pos` `ENNReal.ofReal_ofNat` `Monotone.map_min` `Real.toNNReal_monotone` `Real.toNNReal_ofNat` `inf_of_le_left` `Metric.ball_subset_ball`
`toSphereBallBound_pos` 📖	mathematical	—	`NNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instZeroNNReal` `toSphereBallBound`	—	`mul_pos` `LinearOrderedCommMonoidWithZero.toPosMulStrictMono` `Nat.cast_pos'` `NNReal.addLeftMono` `LinearOrderedCommMonoidWithZero.toZeroLeOneClass` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `NNReal.instIsStrictOrderedRing` `lt_of_le_of_ne'` `zero_le` `Nat.instCanonicallyOrderedAdd` `pow_pos` `IsStrictOrderedRing.toPosMulStrictMono` `IsStrictOrderedRing.toZeroLEOneClass` `div_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `lt_min` `Real.toNNReal_pos` `Mathlib.Meta.Positivity.pos_of_isNat` `NNReal.instIsOrderedRing` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Nat.cast_one`
`toSphere_apply'` 📖	mathematical	`MeasurableSet` `Set.Elem` `Metric.sphere` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `Real` `Real.instOne` `Subtype.instMeasurableSpace` `Set` `Set.instMembership`	`DFunLike.coe` `MeasureTheory.Measure` `ENNReal` `instFunLike` `toSphere` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Module.finrank` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `Set.smul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Set.Ioo` `Real.instPreorder` `Real.instZero` `Set.image`	—	`toSphere.eq_1` `smul_apply` `fst_apply` `restrict_apply` `measurable_fst` `MeasurableEmbedding.comap_apply` `MeasurableEmbedding.comp` `MeasurableEmbedding.subtype_coe` `MeasurableSet.compl` `MeasurableSingletonClass.measurableSet_singleton` `OpensMeasurableSpace.toMeasurableSingletonClass` `BorelSpace.opensMeasurable` `T5Space.toT1Space` `T6Space.toT5Space` `instT6SpaceOfMetrizableSpace` `EMetricSpace.metrizableSpace` `Homeomorph.measurableEmbedding` `Prod.borelSpace` `Subtype.borelSpace` `Real.borelSpace` `secondCountableTopologyEither_of_right` `TopologicalSpace.Subtype.secondCountableTopology` `instSecondCountableTopologyReal` `Set.image_comp` `Homeomorph.image_symm` `Set.univ_prod` `Set.prod_eq` `nsmul_eq_mul` `toSphere_apply_aux`
`toSphere_apply_aux` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `instFunLike` `Set.image` `Set.Elem` `Compl.compl` `Set.instCompl` `Set.instSingletonSet` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `Set.instMembership` `Set.preimage` `Metric.sphere` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Real` `Real.instOne` `Set.Ioi` `Real.instPreorder` `Real.instZero` `Homeomorph` `instTopologicalSpaceSubtype` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `instTopologicalSpaceProd` `Real.pseudoMetricSpace` `EquivLike.toFunLike` `Homeomorph.instEquivLike` `homeomorphUnitSphereProd` `SProd.sprod` `Set.instSProd` `Set.Iio` `Subtype.preorder` `Set.smul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `Set.Ioo`	—	`Set.image2_smul` `Set.image2_image_right` `Homeomorph.image_symm` `Set.image_image` `Set.image_subtype_val_Ioi_Iio` `Set.image2_image_left` `Set.image2_swap` `Set.image_prod`
`toSphere_apply_univ` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.Measure` `Set.Elem` `Metric.sphere` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `Real` `Real.instOne` `Subtype.instMeasurableSpace` `Set` `Set.instMembership` `ENNReal` `instFunLike` `toSphere` `Set.univ` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Module.finrank` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `Metric.ball`	—	`Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim` `apply_eq_zero_of_isEmpty` `Metric.sphere_isEmpty_of_subsingleton` `NeZero.charZero_one` `RCLike.charZero_rclike` `Module.finrank_zero_of_subsingleton` `Real.instNontrivial` `CharP.cast_eq_zero` `CharP.ofCharZero` `ENNReal.instCharZero` `MulZeroClass.zero_mul` `toSphere_apply_univ'` `MeasureTheory.measure_diff_null` `instOuterMeasureClass` `MeasureTheory.NoAtoms.measure_singleton` `IsAddHaarMeasure.noAtoms` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `T5Space.toT1Space` `T6Space.toT5Space` `instT6SpaceOfMetrizableSpace` `EMetricSpace.metrizableSpace` `instWeaklyLocallyCompactSpaceOfLocallyCompactSpace` `locallyCompact_of_proper` `FiniteDimensional.proper_real` `PerfectSpace.not_isolated` `instPerfectSpaceOfT1SpaceOfConnectedSpaceOfNontrivial` `PathConnectedSpace.connectedSpace` `NormedSpace.instPathConnectedSpace`
`toSphere_apply_univ'` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.Measure` `Set.Elem` `Metric.sphere` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `Real` `Real.instOne` `Subtype.instMeasurableSpace` `Set` `Set.instMembership` `ENNReal` `instFunLike` `toSphere` `Set.univ` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Module.finrank` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `Set.instSDiff` `Metric.ball` `Set.instSingletonSet`	—	`toSphere_apply'` `MeasurableSet.univ` `Set.image_univ` `Subtype.range_coe` `Ioo_smul_sphere_zero` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `mul_one` `Metric.closedBall_zero`
`toSphere_eq_zero_iff` 📖	mathematical	—	`toSphere` `MeasureTheory.Measure` `Set.Elem` `Metric.sphere` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `Real` `Real.instOne` `Subtype.instMeasurableSpace` `Set` `Set.instMembership` `instZero`	—	`toSphere_eq_zero_iff_finrank` `Module.finrank_zero_iff` `commRing_strongRankCondition` `Real.instNontrivial` `Real.instIsDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors`
`toSphere_eq_zero_iff_finrank` 📖	mathematical	—	`toSphere` `MeasureTheory.Measure` `Set.Elem` `Metric.sphere` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `Real` `Real.instOne` `Subtype.instMeasurableSpace` `Set` `Set.instMembership` `instZero` `Module.finrank` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real.normedField`	—	`measure_univ_eq_zero` `toSphere_apply_univ` `ENNReal.instNoZeroDivisors` `ENNReal.instCharZero` `IsAddHaarMeasure.toIsOpenPosMeasure` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike`
`toSphere_ne_zero` 📖	—	—	—	—	—
`toSphere_real_apply_univ` 📖	mathematical	—	`real` `Set.Elem` `Metric.sphere` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `Real` `Real.instOne` `Subtype.instMeasurableSpace` `Set` `Set.instMembership` `toSphere` `Set.univ` `Real.instMul` `Real.instNatCast` `Module.finrank` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `Metric.ball`	—	`toSphere_apply_univ` `ENNReal.toReal_mul` `ENNReal.toReal_natCast`
`volumeIoiPow_apply_Iio` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.Measure` `Set.Elem` `Real` `Set.Ioi` `Real.instPreorder` `Real.instZero` `Subtype.instMeasurableSpace` `Set` `Set.instMembership` `Real.measurableSpace` `ENNReal` `instFunLike` `volumeIoiPow` `Set.Iio` `Subtype.preorder` `ENNReal.ofReal` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Monoid.toNatPow` `Real.instMonoid` `Real.instAdd` `Real.instNatCast` `Real.instOne`	—	`le_of_lt` `volumeIoiPow.eq_1` `MeasureTheory.withDensity_apply` `measurableSet_Iio` `Subtype.opensMeasurableSpace` `BorelSpace.opensMeasurable` `Real.borelSpace` `instClosedIciTopology` `Subtype.instOrderClosedTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid` `MeasureTheory.setLIntegral_subtype` `measurableSet_Ioi` `instClosedIicTopology` `Set.image_subtype_val_Ioi_Iio` `restrict_congr_set` `MeasureTheory.Ioo_ae_eq_Ioc` `Real.noAtoms_volume` `MeasureTheory.ofReal_integral_eq_lintegral_ofReal` `intervalIntegral.intervalIntegrable_pow` `Real.locallyFinite_volume` `Filter.mp_mem` `instOuterMeasureClass` `MeasureTheory.ae_restrict_mem` `measurableSet_Ioc` `Filter.univ_mem'` `pow_nonneg` `Real.instZeroLEOneClass` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `LT.lt.le` `intervalIntegral.integral_of_le` `integral_pow` `zero_pow` `sub_zero`

MeasureTheory.Measure.toSphere

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsOpenPosMeasure` 📖	mathematical	—	`MeasureTheory.Measure.IsOpenPosMeasure` `Set.Elem` `Metric.sphere` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `Real` `Real.instOne` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Subtype.instMeasurableSpace` `MeasureTheory.Measure.toSphere`	—	`Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim` `instDiscreteTopologySubtype` `Finite.instDiscreteTopology` `T5Space.toT1Space` `T6Space.toT5Space` `instT6SpaceOfMetrizableSpace` `EMetricSpace.metrizableSpace` `Finite.of_subsingleton` `MeasureTheory.Measure.apply_eq_zero_of_isEmpty` `Metric.sphere_isEmpty_of_subsingleton` `NeZero.charZero_one` `RCLike.charZero_rclike` `Unique.instSubsingleton` `MeasureTheory.Measure.toSphere_apply'` `IsOpen.measurableSet` `Subtype.opensMeasurableSpace` `BorelSpace.opensMeasurable` `mul_ne_zero` `ENNReal.instNoZeroDivisors` `ENNReal.instCharZero` `LT.lt.ne'` `Module.finrank_pos` `commRing_strongRankCondition` `Real.instNontrivial` `Real.instIsDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `IsOpen.measure_ne_zero` `IsOpen.smul_sphere` `one_ne_zero` `isOpen_Ioo` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid` `Real.instZeroLEOneClass` `LinearOrderedSemiField.toDenselyOrdered` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing`

---

← Back to Index