Documentation Verification Report

VolumeOfBalls

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

Statistics

Metric	Count
Definitions	0
Theorems `volume_ball`, `volume_closedBall`, `volume_sum_rpow_le`, `volume_sum_rpow_lt`, `volume_sum_rpow_lt_one`, `volume_ball`, `volume_ball_fin_three`, `volume_ball_fin_two`, `volume_closedBall`, `volume_closedBall_fin_three`, `volume_closedBall_fin_two`, `volume_ball`, `volume_ball_of_dim_even`, `volume_ball_of_dim_odd`, `volume_closedBall`, `volume_closedBall_of_dim_even`, `volume_closedBall_of_dim_odd`, `measure_le_eq_lt`, `measure_lt_one_eq_integral_div_gamma`, `measure_unitBall_eq_integral_div_gamma`, `volume_sum_rpow_le`, `volume_sum_rpow_lt`, `volume_sum_rpow_lt_one`	23
Total	23

Complex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`volume_ball` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.Measure` `Complex` `MeasureTheory.MeasureSpace.toMeasurableSpace` `measureSpaceOfInnerProductSpace` `instNormedAddCommGroup` `instInnerProductSpaceRealComplex` `instFiniteDimensionalReal` `measurableSpace` `borelSpace` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `MeasureTheory.MeasureSpace.volume` `Metric.ball` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `ENNReal.ofReal` `ENNReal.ofNNReal` `NNReal.pi`	—	`instFiniteDimensionalReal` `borelSpace` `InnerProductSpace.volume_ball_of_dim_even` `instNontrivial` `finrank_real_complex` `mul_one` `pow_one` `Nat.cast_one` `div_one` `ENNReal.ofReal_coe_nnreal`
`volume_closedBall` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.Measure` `Complex` `MeasureTheory.MeasureSpace.toMeasurableSpace` `measureSpaceOfInnerProductSpace` `instNormedAddCommGroup` `instInnerProductSpaceRealComplex` `instFiniteDimensionalReal` `measurableSpace` `borelSpace` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `MeasureTheory.MeasureSpace.volume` `Metric.closedBall` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `ENNReal.ofReal` `ENNReal.ofNNReal` `NNReal.pi`	—	`instFiniteDimensionalReal` `borelSpace` `MeasureTheory.Measure.addHaar_closedBall_eq_addHaar_ball` `instIsAddHaarMeasureVolume` `instNontrivial` `volume_ball`
`volume_sum_rpow_le` 📖	mathematical	`Real` `Real.instLE` `Real.instOne`	`DFunLike.coe` `MeasureTheory.Measure` `MeasureTheory.MeasureSpace.toMeasurableSpace` `MeasureTheory.MeasureSpace.pi` `Complex` `measureSpaceOfInnerProductSpace` `instNormedAddCommGroup` `instInnerProductSpaceRealComplex` `instFiniteDimensionalReal` `measurableSpace` `borelSpace` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `MeasureTheory.MeasureSpace.volume` `setOf` `Real.instPow` `Finset.sum` `Real.instAddCommMonoid` `Finset.univ` `Norm.norm` `instNorm` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `ENNReal.ofReal` `Fintype.card` `Real.instMonoid` `Real.instMul` `Real.pi` `Real.Gamma` `Real.instAdd` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`lt_of_not_ge` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.cast_zero` `Nat.cast_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `Real.instIsStrictOrderedRing` `neg_neg_of_pos` `Real.instIsOrderedAddMonoid` `Mathlib.Tactic.Linarith.zero_lt_one` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `Real.instIsOrderedRing` `ENNReal.toReal_ofReal` `le_of_lt` `PiLp.norm_eq_sum` `Finset.sum_congr` `one_div` `fact_iff` `ENNReal.ofReal_le_ofReal` `ENNReal.ofReal_one` `norm_zero` `norm_eq_zero` `WithLp.toLp_eq_zero` `norm_neg` `norm_add_le` `norm_smul_le` `PiLp.instIsBoundedSMul` `NormedSpace.toIsBoundedSMul` `instFiniteDimensionalReal` `borelSpace` `Nat.instAtLeastTwoHAddOfNat` `MeasureTheory.measure_le_eq_lt` `FiniteDimensional.finiteDimensional_pi'` `Finite.of_fintype` `Pi.topologicalAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `Pi.borelSpace` `Finite.to_countable` `secondCountable_of_proper` `instProperSpace` `Pi.t2Space` `instT2Space` `instContinuousSMulForall` `IsBoundedSMul.continuousSMul` `MeasureTheory.Measure.instIsAddHaarMeasureForallVolumeOfMeasurableAddOfSigmaFinite` `ContinuousAdd.measurableAdd` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `MeasureTheory.Measure.IsAddHaarMeasure.sigmaFinite` `instIsAddHaarMeasureVolume` `SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `instWeaklyLocallyCompactSpaceOfLocallyCompactSpace` `locallyCompact_of_proper` `Function.nontrivial` `instNontrivial` `volume_sum_rpow_lt`
`volume_sum_rpow_lt` 📖	mathematical	`Real` `Real.instLE` `Real.instOne`	`DFunLike.coe` `MeasureTheory.Measure` `MeasureTheory.MeasureSpace.toMeasurableSpace` `MeasureTheory.MeasureSpace.pi` `Complex` `measureSpaceOfInnerProductSpace` `instNormedAddCommGroup` `instInnerProductSpaceRealComplex` `instFiniteDimensionalReal` `measurableSpace` `borelSpace` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `MeasureTheory.MeasureSpace.volume` `setOf` `Real.instLT` `Real.instPow` `Finset.sum` `Real.instAddCommMonoid` `Finset.univ` `Norm.norm` `instNorm` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `ENNReal.ofReal` `Fintype.card` `Real.instMonoid` `Real.instMul` `Real.pi` `Real.Gamma` `Real.instAdd` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`Finset.sum_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.rpow_nonneg` `norm_nonneg` `instFiniteDimensionalReal` `borelSpace` `Nat.instAtLeastTwoHAddOfNat` `le_or_gt` `Set.ext` `not_le` `lt_of_lt_of_le` `Set.mem_setOf` `MeasureTheory.measure_empty` `MeasureTheory.Measure.instOuterMeasureClass` `ENNReal.zero_eq_ofReal` `zero_pow` `LT.lt.ne'` `Fintype.instNeZeroNatCardOfNonempty` `MulZeroClass.zero_mul` `volume_sum_rpow_lt_one` `ENNReal.ofReal_pow` `le_of_lt` `Set.preimage_smul_inv₀` `ne_of_gt` `Finset.sum_congr` `norm_smul` `NormedSpace.toNormSMulClass` `Real.mul_rpow` `abs_inv` `Real.instIsStrictOrderedRing` `Real.inv_rpow` `abs_nonneg` `covariant_swap_add_of_covariant_add` `abs_eq_self` `inv_mul_lt_iff₀` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.rpow_pos_of_pos` `mul_one` `Real.rpow_lt_rpow_iff` `lt_of_not_ge` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.cast_zero` `Nat.cast_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `neg_neg_of_pos` `Mathlib.Tactic.Linarith.zero_lt_one` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `Real.instIsOrderedRing` `Real.rpow_mul` `div_mul_cancel₀` `Real.rpow_one` `Module.finrank_pi_fintype` `commRing_strongRankCondition` `Real.instNontrivial` `Module.Free.of_divisionRing` `finrank_real_complex` `Finset.sum_const` `mul_comm` `MeasureTheory.Measure.addHaar_smul_of_nonneg` `Pi.borelSpace` `Finite.to_countable` `Finite.of_fintype` `PolishSpace.toSecondCountableTopology` `instPolishSpaceOfSeparableSpaceOfIsCompletelyMetrizableSpace` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `secondCountable_of_proper` `instProperSpace` `TopologicalSpace.IsCompletelyMetrizableSpace.of_completeSpace_metrizable` `instCompleteSpace` `EMetric.instIsCountablyGeneratedUniformity` `T6Space.toT0Space` `instT6SpaceOfMetrizableSpace` `EMetricSpace.metrizableSpace` `FiniteDimensional.finiteDimensional_pi'` `MeasureTheory.Measure.instIsAddHaarMeasureForallVolumeOfMeasurableAddOfSigmaFinite` `ContinuousAdd.measurableAdd` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `MeasureTheory.Measure.IsAddHaarMeasure.sigmaFinite` `instIsAddHaarMeasureVolume` `SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `instWeaklyLocallyCompactSpaceOfLocallyCompactSpace` `locallyCompact_of_proper`
`volume_sum_rpow_lt_one` 📖	mathematical	`Real` `Real.instLE` `Real.instOne`	`DFunLike.coe` `MeasureTheory.Measure` `MeasureTheory.MeasureSpace.toMeasurableSpace` `MeasureTheory.MeasureSpace.pi` `Complex` `measureSpaceOfInnerProductSpace` `instNormedAddCommGroup` `instInnerProductSpaceRealComplex` `instFiniteDimensionalReal` `measurableSpace` `borelSpace` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `MeasureTheory.MeasureSpace.volume` `setOf` `Real.instLT` `Finset.sum` `Real.instAddCommMonoid` `Finset.univ` `Real.instPow` `Norm.norm` `instNorm` `ENNReal.ofReal` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Monoid.toNatPow` `Real.instMonoid` `Real.instMul` `Real.pi` `Real.Gamma` `Real.instAdd` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Fintype.card`	—	`lt_of_not_ge` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.cast_zero` `Nat.cast_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `Real.instIsStrictOrderedRing` `neg_neg_of_pos` `Real.instIsOrderedAddMonoid` `Mathlib.Tactic.Linarith.zero_lt_one` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `Real.instIsOrderedRing` `ENNReal.toReal_ofReal` `le_of_lt` `Finset.sum_nonneg'` `IsOrderedAddMonoid.toAddLeftMono` `Real.rpow_nonneg` `norm_nonneg` `PiLp.norm_eq_sum` `Finset.sum_congr` `one_div` `fact_iff` `ENNReal.ofReal_le_ofReal` `ENNReal.ofReal_one` `norm_zero` `norm_eq_zero` `WithLp.toLp_eq_zero` `norm_neg` `norm_add_le` `norm_smul_le` `PiLp.instIsBoundedSMul` `NormedSpace.toIsBoundedSMul` `instFiniteDimensionalReal` `borelSpace` `Nat.instAtLeastTwoHAddOfNat` `Real.rpow_lt_one_iff'` `one_div_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.rpow_mul` `div_mul_cancel₀` `ne_of_gt` `Real.rpow_one` `Real.exp_sum` `MeasureTheory.integral_fintype_prod_volume_eq_pow` `MeasureTheory.Measure.IsAddHaarMeasure.sigmaFinite` `instIsAddHaarMeasureVolume` `SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `secondCountable_of_proper` `instProperSpace` `instWeaklyLocallyCompactSpaceOfLocallyCompactSpace` `locallyCompact_of_proper` `FiniteDimensional.rclike_to_real` `integral_exp_neg_rpow` `Module.finrank_pi_fintype` `commRing_strongRankCondition` `Real.instNontrivial` `Module.Free.of_divisionRing` `finrank_real_complex` `Finset.sum_const` `smul_eq_mul` `Nat.cast_mul` `Nat.cast_ofNat` `Fintype.card.eq_1` `mul_comm` `MeasureTheory.measure_lt_one_eq_integral_div_gamma` `FiniteDimensional.finiteDimensional_pi'` `Finite.of_fintype` `Pi.topologicalAddGroup` `Pi.borelSpace` `Finite.to_countable` `Pi.t2Space` `instT2Space` `instContinuousSMulForall` `IsBoundedSMul.continuousSMul` `MeasureTheory.Measure.instIsAddHaarMeasureForallVolumeOfMeasurableAddOfSigmaFinite` `ContinuousAdd.measurableAdd` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing`

EuclideanSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`volume_ball` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.Measure` `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` `Set` `MeasureTheory.Measure.instFunLike` `MeasureTheory.MeasureSpace.volume` `Metric.ball` `PiLp.instPseudoMetricSpace` `Real.pseudoMetricSpace` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `ENNReal.ofReal` `Fintype.card` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instMonoid` `Real.sqrt` `Real.pi` `Real.Gamma` `Real.instAdd` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Real.instOne`	—	`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` `Nat.instAtLeastTwoHAddOfNat` `le_total` `Metric.ball_eq_empty` `MeasureTheory.measure_empty` `MeasureTheory.Measure.instOuterMeasureClass` `ENNReal.zero_eq_ofReal` `zero_pow` `Fintype.card_ne_zero` `MulZeroClass.zero_mul` `MeasureTheory.MeasurePreserving.measure_preimage` `PiLp.volume_preserving_toLp` `MeasurableSet.nullMeasurableSet` `measurableSet_ball` `BorelSpace.opensMeasurable` `ball_zero_eq` `zero_le_one` `Real.instZeroLEOneClass` `Finset.sum_congr` `one_pow` `Real.rpow_ofNat` `sq_abs` `Real.Gamma_add_one` `one_div` `RCLike.charZero_rclike` `Real.Gamma_one_half_eq` `mul_assoc` `mul_div_cancel₀` `two_ne_zero` `CharZero.NeZero.two` `one_mul` `MeasureTheory.volume_sum_rpow_lt_one` `one_le_two` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `MeasureTheory.Measure.addHaar_ball` `instIsAddHaarMeasureVolume` `WithLp.instNontrivial` `Function.nontrivial` `Real.instNontrivial` `ENNReal.ofReal_pow` `finrank_euclideanSpace`
`volume_ball_fin_three` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.Measure` `EuclideanSpace` `Real` `MeasureTheory.MeasureSpace.toMeasurableSpace` `measureSpaceOfInnerProductSpace` `PiLp.normedAddCommGroup` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `fact_one_le_two_ennreal` `Fin.fintype` `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` `instCountableFin` `UniformSpace.toTopologicalSpace` `Real.borelSpace` `instSecondCountableTopologyReal` `Set` `MeasureTheory.Measure.instFunLike` `MeasureTheory.MeasureSpace.volume` `Metric.ball` `PiLp.instPseudoMetricSpace` `Real.pseudoMetricSpace` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `ENNReal.ofReal` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instMul` `Real.pi` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`fact_one_le_two_ennreal` `WithLp.instModuleFinite` `FiniteDimensional.finiteDimensional_pi'` `Finite.of_fintype` `FiniteDimensional.rclike_to_real` `PiLp.borelSpace` `instCountableFin` `Real.borelSpace` `instSecondCountableTopologyReal` `Nat.instAtLeastTwoHAddOfNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `InnerProductSpace.volume_ball_of_dim_odd` `finrank_euclideanSpace` `Fintype.card_fin` `mul_one` `pow_one` `Mathlib.Meta.NormNum.IsNat.to_eq` `Mathlib.Meta.NormNum.isNat_pow` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.isNat_add` `Mathlib.Meta.NormNum.IsNatPowT.run` `Mathlib.Meta.NormNum.IsNatPowT.bit0`
`volume_ball_fin_two` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.Measure` `EuclideanSpace` `Real` `MeasureTheory.MeasureSpace.toMeasurableSpace` `measureSpaceOfInnerProductSpace` `PiLp.normedAddCommGroup` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `fact_one_le_two_ennreal` `Fin.fintype` `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` `instCountableFin` `UniformSpace.toTopologicalSpace` `Real.borelSpace` `instSecondCountableTopologyReal` `Set` `MeasureTheory.Measure.instFunLike` `MeasureTheory.MeasureSpace.volume` `Metric.ball` `PiLp.instPseudoMetricSpace` `Real.pseudoMetricSpace` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `ENNReal.ofReal` `Real.pi`	—	`fact_one_le_two_ennreal` `WithLp.instModuleFinite` `FiniteDimensional.finiteDimensional_pi'` `Finite.of_fintype` `FiniteDimensional.rclike_to_real` `PiLp.borelSpace` `instCountableFin` `Real.borelSpace` `instSecondCountableTopologyReal` `InnerProductSpace.volume_ball_of_dim_even` `WithLp.instNontrivial` `Function.nontrivial` `Real.instNontrivial` `finrank_euclideanSpace` `Fintype.card_fin` `mul_one` `pow_one` `Nat.cast_one` `div_one`
`volume_closedBall` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.Measure` `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` `Set` `MeasureTheory.Measure.instFunLike` `MeasureTheory.MeasureSpace.volume` `Metric.closedBall` `PiLp.instPseudoMetricSpace` `Real.pseudoMetricSpace` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `ENNReal.ofReal` `Fintype.card` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instMonoid` `Real.sqrt` `Real.pi` `Real.Gamma` `Real.instAdd` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Real.instOne`	—	`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` `Nat.instAtLeastTwoHAddOfNat` `MeasureTheory.Measure.addHaar_closedBall_eq_addHaar_ball` `instIsAddHaarMeasureVolume` `WithLp.instNontrivial` `Function.nontrivial` `Real.instNontrivial` `volume_ball`
`volume_closedBall_fin_three` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.Measure` `EuclideanSpace` `Real` `MeasureTheory.MeasureSpace.toMeasurableSpace` `measureSpaceOfInnerProductSpace` `PiLp.normedAddCommGroup` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `fact_one_le_two_ennreal` `Fin.fintype` `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` `instCountableFin` `UniformSpace.toTopologicalSpace` `Real.borelSpace` `instSecondCountableTopologyReal` `Set` `MeasureTheory.Measure.instFunLike` `MeasureTheory.MeasureSpace.volume` `Metric.closedBall` `PiLp.instPseudoMetricSpace` `Real.pseudoMetricSpace` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `ENNReal.ofReal` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instMul` `Real.pi` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`fact_one_le_two_ennreal` `WithLp.instModuleFinite` `FiniteDimensional.finiteDimensional_pi'` `Finite.of_fintype` `FiniteDimensional.rclike_to_real` `PiLp.borelSpace` `instCountableFin` `Real.borelSpace` `instSecondCountableTopologyReal` `Nat.instAtLeastTwoHAddOfNat` `MeasureTheory.Measure.addHaar_closedBall_eq_addHaar_ball` `instIsAddHaarMeasureVolume` `WithLp.instNontrivial` `Function.nontrivial` `Real.instNontrivial` `volume_ball_fin_three`
`volume_closedBall_fin_two` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.Measure` `EuclideanSpace` `Real` `MeasureTheory.MeasureSpace.toMeasurableSpace` `measureSpaceOfInnerProductSpace` `PiLp.normedAddCommGroup` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `fact_one_le_two_ennreal` `Fin.fintype` `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` `instCountableFin` `UniformSpace.toTopologicalSpace` `Real.borelSpace` `instSecondCountableTopologyReal` `Set` `MeasureTheory.Measure.instFunLike` `MeasureTheory.MeasureSpace.volume` `Metric.closedBall` `PiLp.instPseudoMetricSpace` `Real.pseudoMetricSpace` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `ENNReal.ofReal` `Real.pi`	—	`fact_one_le_two_ennreal` `WithLp.instModuleFinite` `FiniteDimensional.finiteDimensional_pi'` `Finite.of_fintype` `FiniteDimensional.rclike_to_real` `PiLp.borelSpace` `instCountableFin` `Real.borelSpace` `instSecondCountableTopologyReal` `MeasureTheory.Measure.addHaar_closedBall_eq_addHaar_ball` `instIsAddHaarMeasureVolume` `WithLp.instNontrivial` `Function.nontrivial` `Real.instNontrivial` `volume_ball_fin_two`

InnerProductSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`volume_ball` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.Measure` `MeasureTheory.MeasureSpace.toMeasurableSpace` `measureSpaceOfInnerProductSpace` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `MeasureTheory.MeasureSpace.volume` `Metric.ball` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `ENNReal.ofReal` `Module.finrank` `Real` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `toNormedSpace` `Real.instRCLike` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instMonoid` `Real.sqrt` `Real.pi` `Real.Gamma` `Real.instAdd` `Real.instNatCast` `instOfNatAtLeastTwo` `Nat.instAtLeastTwoHAddOfNat` `Real.instOne`	—	`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` `RingHomInvPair.ids` `MeasureTheory.MeasurePreserving.measure_preimage` `OrthonormalBasis.measurePreserving_repr_symm` `MeasurableSet.nullMeasurableSet` `measurableSet_ball` `BorelSpace.opensMeasurable` `Module.finrank_pos` `commRing_strongRankCondition` `Real.instNontrivial` `Real.instIsDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `EuclideanSpace.volume_ball` `LinearIsometryEquiv.preimage_ball` `Fintype.card_fin`
`volume_ball_of_dim_even` 📖	mathematical	`Module.finrank` `Real` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `toNormedSpace` `Real.instRCLike`	`DFunLike.coe` `MeasureTheory.Measure` `MeasureTheory.MeasureSpace.toMeasurableSpace` `measureSpaceOfInnerProductSpace` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `MeasureTheory.MeasureSpace.volume` `Metric.ball` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `ENNReal.ofReal` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instMonoid` `Real.pi` `Real.instNatCast` `Nat.factorial`	—	`Nat.instAtLeastTwoHAddOfNat` `volume_ball` `pow_mul` `Real.sq_sqrt` `Real.pi_nonneg` `Nat.cast_mul` `mul_div_cancel_left₀` `EuclideanDomain.toMulDivCancelClass` `RCLike.charZero_rclike` `Real.Gamma_nat_eq_factorial`
`volume_ball_of_dim_odd` 📖	mathematical	`Module.finrank` `Real` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `toNormedSpace` `Real.instRCLike`	`DFunLike.coe` `MeasureTheory.Measure` `MeasureTheory.MeasureSpace.toMeasurableSpace` `measureSpaceOfInnerProductSpace` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `MeasureTheory.MeasureSpace.volume` `Metric.ball` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `ENNReal.ofReal` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instMul` `Real.instMonoid` `Real.pi` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Nat.doubleFactorial`	—	`Module.nontrivial_of_finrank_pos` `Real.instNontrivial` `Nat.instAtLeastTwoHAddOfNat` `volume_ball` `pow_succ` `pow_mul` `Real.sq_sqrt` `Real.pi_nonneg` `mul_div_assoc` `Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq` `IsCancelMulZero.toIsLeftCancelMulZero` `instIsCancelMulZero` `Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.atom_eq_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁` `one_mul` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃` `div_one` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₂` `Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero` `Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero` `ne_of_gt` `Real.sqrt_pos_of_pos` `Real.pi_pos` `Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁` `Mathlib.Tactic.FieldSimp.NF.cons_ne_zero` `pow_pos` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `IsStrictOrderedRing.toZeroLEOneClass` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instIsOrderedRing` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Nat.cast_pos'` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `Nat.doubleFactorial_pos` `one_ne_zero` `NeZero.one` `GroupWithZero.toNontrivial` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.cast_pos` `Nat.cast_one` `Nat.cast_add` `Nat.cast_mul` `add_div` `mul_div_cancel_left₀` `EuclideanDomain.toMulDivCancelClass` `add_right_comm` `Real.Gamma_nat_add_one_add_half`
`volume_closedBall` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.Measure` `MeasureTheory.MeasureSpace.toMeasurableSpace` `measureSpaceOfInnerProductSpace` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `MeasureTheory.MeasureSpace.volume` `Metric.closedBall` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `ENNReal.ofReal` `Module.finrank` `Real` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `toNormedSpace` `Real.instRCLike` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instMonoid` `Real.sqrt` `Real.pi` `Real.Gamma` `Real.instAdd` `Real.instNatCast` `instOfNatAtLeastTwo` `Nat.instAtLeastTwoHAddOfNat` `Real.instOne`	—	`Nat.instAtLeastTwoHAddOfNat` `MeasureTheory.Measure.addHaar_closedBall_eq_addHaar_ball` `instIsAddHaarMeasureVolume` `volume_ball`
`volume_closedBall_of_dim_even` 📖	mathematical	`Module.finrank` `Real` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `toNormedSpace` `Real.instRCLike`	`DFunLike.coe` `MeasureTheory.Measure` `MeasureTheory.MeasureSpace.toMeasurableSpace` `measureSpaceOfInnerProductSpace` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `MeasureTheory.MeasureSpace.volume` `Metric.closedBall` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `ENNReal.ofReal` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instMonoid` `Real.pi` `Real.instNatCast` `Nat.factorial`	—	`MeasureTheory.Measure.addHaar_closedBall_eq_addHaar_ball` `instIsAddHaarMeasureVolume` `volume_ball_of_dim_even`
`volume_closedBall_of_dim_odd` 📖	mathematical	`Module.finrank` `Real` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `toNormedSpace` `Real.instRCLike`	`DFunLike.coe` `MeasureTheory.Measure` `MeasureTheory.MeasureSpace.toMeasurableSpace` `measureSpaceOfInnerProductSpace` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `MeasureTheory.MeasureSpace.volume` `Metric.closedBall` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `ENNReal.ofReal` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instMul` `Real.instMonoid` `Real.pi` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Nat.doubleFactorial`	—	`Module.nontrivial_of_finrank_pos` `Real.instNontrivial` `Nat.instAtLeastTwoHAddOfNat` `MeasureTheory.Measure.addHaar_closedBall_eq_addHaar_ball` `instIsAddHaarMeasureVolume` `volume_ball_of_dim_odd`

MeasureTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`measure_le_eq_lt` 📖	mathematical	`NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Real` `Real.instZero` `NegZeroClass.toNeg` `Real.instLE` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `Real.instAdd` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Real.semiring` `Real.instMul` `abs` `Real.lattice` `Real.instAddGroup`	`DFunLike.coe` `Measure` `Set` `ENNReal` `Measure.instFunLike` `setOf` `Real.instLT`	—	`RingHomInvPair.ids` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `Real.instCompleteSpace` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `Measure.map_apply` `Continuous.measurable` `BorelSpace.opensMeasurable` `ContinuousLinearEquiv.continuous` `measurableSet_closedBall` `dist_zero_right` `measurableSet_ball` `Measure.addHaar_closedBall_eq_addHaar_ball` `ContinuousLinearEquiv.isAddHaarMeasure_map`
`measure_lt_one_eq_integral_div_gamma` 📖	mathematical	`NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Real` `Real.instZero` `NegZeroClass.toNeg` `Real.instLE` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `Real.instAdd` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Real.semiring` `Real.instMul` `abs` `Real.lattice` `Real.instAddGroup` `Real.instLT`	`DFunLike.coe` `Measure` `Set` `ENNReal` `Measure.instFunLike` `setOf` `Real.instOne` `ENNReal.ofReal` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `integral` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `Real.exp` `Real.instNeg` `Real.instPow` `Real.Gamma` `Real.instNatCast` `Module.finrank`	—	`RingHomInvPair.ids` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `Real.instCompleteSpace` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `Measure.map_apply` `Continuous.measurable` `BorelSpace.opensMeasurable` `ContinuousLinearEquiv.continuous` `measurableSet_ball` `dist_zero_right` `Measurable.measurePreserving` `MeasurableEquiv.measurable` `MeasurePreserving.integral_comp'` `measure_unitBall_eq_integral_div_gamma` `ContinuousLinearEquiv.isAddHaarMeasure_map`
`measure_unitBall_eq_integral_div_gamma` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`DFunLike.coe` `Measure` `Set` `ENNReal` `Measure.instFunLike` `Metric.ball` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `Real.instOne` `ENNReal.ofReal` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `integral` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `Real.exp` `Real.instNeg` `Real.instPow` `Norm.norm` `NormedAddCommGroup.toNorm` `Real.Gamma` `Real.instAdd` `Real.instNatCast` `Module.finrank` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real.normedField`	—	`subsingleton_or_nontrivial` `Set.Nonempty.eq_zero` `Metric.nonempty_ball` `zero_lt_one` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `setIntegral_univ` `Set.univ_nonempty` `AddTorsor.nonempty` `integral_singleton` `Real.instCompleteSpace` `instMeasurableSingletonClassOfMeasurableEq` `instMeasurableEqOfSecondCountableTopologyOfT2Space` `BorelSpace.opensMeasurable` `PolishSpace.toSecondCountableTopology` `instPolishSpaceOfSeparableSpaceOfIsCompletelyMetrizableSpace` `TopologicalSpace.Countable.to_separableSpace` `Finite.to_countable` `Finite.of_subsingleton` `TopologicalSpace.IsCompletelyMetrizableSpace.of_completeSpace_metrizable` `complete_of_proper` `FiniteDimensional.proper_real` `EMetric.instIsCountablyGeneratedUniformity` `T6Space.toT0Space` `instT6SpaceOfMetrizableSpace` `EMetricSpace.metrizableSpace` `TopologicalSpace.t2Space_of_metrizableSpace` `Module.finrank_zero_of_subsingleton` `Real.instNontrivial` `Nat.cast_zero` `zero_div` `zero_add` `Real.Gamma_one` `div_one` `norm_zero` `Real.zero_rpow` `LT.lt.ne'` `neg_zero` `Real.exp_zero` `smul_eq_mul` `mul_one` `measureReal_def` `ENNReal.ofReal_toReal` `measure_ne_top` `CompactSpace.isFiniteMeasure` `TopologicalSpace.NoetherianSpace.compactSpace` `TopologicalSpace.Finite.to_noetherianSpace` `Measure.IsAddHaarMeasure.toIsFiniteMeasureOnCompacts` `Nat.cast_pos` `Real.instIsOrderedRing` `Module.finrank_pos` `commRing_strongRankCondition` `Real.instIsDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `Real.rpow_natCast` `Nat.cast_sub` `Nat.cast_one` `integral_rpow_mul_exp_neg_rpow` `lt_of_not_ge` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.cast_zero` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `Real.instIsStrictOrderedRing` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `sub_add_cancel` `Real.Gamma_add_one` `ne_of_gt` `div_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq` `IsCancelMulZero.toIsLeftCancelMulZero` `instIsCancelMulZero` `Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.one_eq_eval` `Mathlib.Tactic.FieldSimp.NF.atom_eq_eval` `Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₂` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero` `one_mul` `Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero` `Real.Gamma_pos_of_pos` `Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst` `one_ne_zero` `NeZero.one` `GroupWithZero.toNontrivial` `integral_fun_norm_addHaar` `nsmul_eq_mul` `mul_div_assoc` `mul_comm` `mul_assoc` `ofReal_measureReal` `ne_of_lt` `measure_ball_lt_top`
`volume_sum_rpow_le` 📖	mathematical	`Real` `Real.instLE` `Real.instOne`	`DFunLike.coe` `Measure` `MeasureSpace.toMeasurableSpace` `MeasureSpace.pi` `Real.measureSpace` `Set` `ENNReal` `Measure.instFunLike` `MeasureSpace.volume` `setOf` `Real.instPow` `Finset.sum` `Real.instAddCommMonoid` `Finset.univ` `abs` `Real.lattice` `Real.instAddGroup` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `ENNReal.ofReal` `Fintype.card` `Real.instMonoid` `Real.instMul` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Real.Gamma` `Real.instAdd`	—	`lt_of_not_ge` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.cast_zero` `Nat.cast_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `Real.instIsStrictOrderedRing` `neg_neg_of_pos` `Real.instIsOrderedAddMonoid` `Mathlib.Tactic.Linarith.zero_lt_one` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `Real.instIsOrderedRing` `ENNReal.toReal_ofReal` `le_of_lt` `PiLp.norm_eq_sum` `Finset.sum_congr` `one_div` `fact_iff` `ENNReal.ofReal_le_ofReal` `ENNReal.ofReal_one` `norm_zero` `norm_eq_zero` `WithLp.toLp_eq_zero` `norm_neg` `norm_add_le` `norm_smul_le` `PiLp.instIsBoundedSMul` `Real.isBoundedSMul` `Nat.instAtLeastTwoHAddOfNat` `measure_le_eq_lt` `FiniteDimensional.finiteDimensional_pi'` `Finite.of_fintype` `FiniteDimensional.rclike_to_real` `Pi.topologicalAddGroup` `instIsTopologicalAddGroupReal` `Pi.borelSpace` `Finite.to_countable` `instSecondCountableTopologyReal` `Real.borelSpace` `Pi.t2Space` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `instContinuousSMulForall` `IsModuleTopology.toContinuousSMul` `IsTopologicalSemiring.toIsModuleTopology` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `Measure.instIsAddHaarMeasureForallVolumeOfMeasurableAddOfSigmaFinite` `ContinuousAdd.measurableAdd` `IsTopologicalSemiring.toContinuousAdd` `Measure.IsAddHaarMeasure.sigmaFinite` `instIsAddHaarMeasureVolume` `SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `instWeaklyLocallyCompactSpaceOfLocallyCompactSpace` `locallyCompact_of_proper` `instProperSpaceReal` `Function.nontrivial` `Real.instNontrivial` `volume_sum_rpow_lt`
`volume_sum_rpow_lt` 📖	mathematical	`Real` `Real.instLE` `Real.instOne`	`DFunLike.coe` `Measure` `MeasureSpace.toMeasurableSpace` `MeasureSpace.pi` `Real.measureSpace` `Set` `ENNReal` `Measure.instFunLike` `MeasureSpace.volume` `setOf` `Real.instLT` `Real.instPow` `Finset.sum` `Real.instAddCommMonoid` `Finset.univ` `abs` `Real.lattice` `Real.instAddGroup` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `ENNReal.ofReal` `Fintype.card` `Real.instMonoid` `Real.instMul` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Real.Gamma` `Real.instAdd`	—	`Finset.sum_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.rpow_nonneg` `abs_nonneg` `covariant_swap_add_of_covariant_add` `Nat.instAtLeastTwoHAddOfNat` `le_or_gt` `Set.ext` `not_le` `lt_of_lt_of_le` `Set.mem_setOf` `measure_empty` `Measure.instOuterMeasureClass` `ENNReal.zero_eq_ofReal` `zero_pow` `LT.lt.ne'` `Fintype.instNeZeroNatCardOfNonempty` `MulZeroClass.zero_mul` `volume_sum_rpow_lt_one` `ENNReal.ofReal_pow` `le_of_lt` `Module.finrank_pi` `commRing_strongRankCondition` `Real.instNontrivial` `Set.preimage_smul_inv₀` `ne_of_gt` `Finset.sum_congr` `abs_mul` `Real.instIsOrderedRing` `Real.mul_rpow` `abs_inv` `Real.instIsStrictOrderedRing` `Real.inv_rpow` `abs_eq_self` `inv_mul_lt_iff₀` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.rpow_pos_of_pos` `mul_one` `Real.rpow_lt_rpow_iff` `lt_of_not_ge` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.cast_zero` `Nat.cast_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `neg_neg_of_pos` `Mathlib.Tactic.Linarith.zero_lt_one` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `Real.rpow_mul` `div_mul_cancel₀` `Real.rpow_one` `Measure.addHaar_smul_of_nonneg` `Pi.borelSpace` `Finite.to_countable` `Finite.of_fintype` `instSecondCountableTopologyReal` `Real.borelSpace` `FiniteDimensional.finiteDimensional_pi'` `FiniteDimensional.rclike_to_real` `Measure.instIsAddHaarMeasureForallVolumeOfMeasurableAddOfSigmaFinite` `ContinuousAdd.measurableAdd` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `Measure.IsAddHaarMeasure.sigmaFinite` `instIsAddHaarMeasureVolume` `SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace` `instIsTopologicalAddGroupReal` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `instWeaklyLocallyCompactSpaceOfLocallyCompactSpace` `locallyCompact_of_proper` `instProperSpaceReal`
`volume_sum_rpow_lt_one` 📖	mathematical	`Real` `Real.instLE` `Real.instOne`	`DFunLike.coe` `Measure` `MeasureSpace.toMeasurableSpace` `MeasureSpace.pi` `Real.measureSpace` `Set` `ENNReal` `Measure.instFunLike` `MeasureSpace.volume` `setOf` `Real.instLT` `Finset.sum` `Real.instAddCommMonoid` `Finset.univ` `Real.instPow` `abs` `Real.lattice` `Real.instAddGroup` `ENNReal.ofReal` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Monoid.toNatPow` `Real.instMonoid` `Real.instMul` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Real.Gamma` `Real.instAdd` `Fintype.card`	—	`lt_of_not_ge` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.cast_zero` `Nat.cast_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `Real.instIsStrictOrderedRing` `neg_neg_of_pos` `Real.instIsOrderedAddMonoid` `Mathlib.Tactic.Linarith.zero_lt_one` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `Real.instIsOrderedRing` `ENNReal.toReal_ofReal` `le_of_lt` `Finset.sum_nonneg'` `IsOrderedAddMonoid.toAddLeftMono` `Real.rpow_nonneg` `abs_nonneg` `covariant_swap_add_of_covariant_add` `PiLp.norm_eq_sum` `Finset.sum_congr` `one_div` `fact_iff` `ENNReal.ofReal_le_ofReal` `ENNReal.ofReal_one` `norm_zero` `norm_eq_zero` `WithLp.toLp_eq_zero` `norm_neg` `norm_add_le` `norm_smul_le` `PiLp.instIsBoundedSMul` `Real.isBoundedSMul` `Nat.instAtLeastTwoHAddOfNat` `Real.rpow_lt_one_iff'` `one_div_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.rpow_mul` `div_mul_cancel₀` `ne_of_gt` `Real.rpow_one` `Real.exp_sum` `integral_fintype_prod_volume_eq_pow` `Measure.IsAddHaarMeasure.sigmaFinite` `instIsAddHaarMeasureVolume` `FiniteDimensional.rclike_to_real` `Real.borelSpace` `SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace` `instIsTopologicalAddGroupReal` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `instSecondCountableTopologyReal` `instWeaklyLocallyCompactSpaceOfLocallyCompactSpace` `locallyCompact_of_proper` `instProperSpaceReal` `integral_comp_abs` `integral_exp_neg_rpow` `Module.finrank_fintype_fun_eq_card` `commRing_strongRankCondition` `Real.instNontrivial` `measure_lt_one_eq_integral_div_gamma` `FiniteDimensional.finiteDimensional_pi'` `Finite.of_fintype` `Pi.topologicalAddGroup` `Pi.borelSpace` `Finite.to_countable` `Pi.t2Space` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `instContinuousSMulForall` `IsModuleTopology.toContinuousSMul` `IsTopologicalSemiring.toIsModuleTopology` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `Measure.instIsAddHaarMeasureForallVolumeOfMeasurableAddOfSigmaFinite` `ContinuousAdd.measurableAdd` `IsTopologicalSemiring.toContinuousAdd`

---

← Back to Index