Documentation Verification Report

RadialAngularMeasure

📁 Source: PhysLean/SpaceAndTime/Space/Integrals/RadialAngularMeasure.lean

Statistics

Metric	Count
Definitions `radialAngularMeasure`	1
Theorems `instHasTemperateGrowthRadialAngularMeasure`, `instSFiniteRadialAngularMeasure`, `integrable_radialAngularMeasure_iff`, `integrable_radialAngularMeasure_of_spherical`, `integral_radialAngularMeasure`, `lintegral_radialMeasure`, `lintegral_radialMeasure_eq_spherical_mul`, `radialAngularMeasure_closedBall`, `radialAngularMeasure_eq_volume_withDensity`, `radialAngularMeasure_integrable_pow_neg_two`, `radialAngularMeasure_real_closedBall`, `radialAngularMeasure_zero_eq_volume`	12
Total	13

Space

Definitions

Name	Category	Theorems
`radialAngularMeasure` 📖	CompOp	12 math math: `instSFiniteRadialAngularMeasure`, `radialAngularMeasure_zero_eq_volume`, `lintegral_radialMeasure_eq_spherical_mul`, `lintegral_radialMeasure`, `integrable_radialAngularMeasure_iff`, `radialAngularMeasure_real_closedBall`, `radialAngularMeasure_integrable_pow_neg_two`, `radialAngularMeasure_eq_volume_withDensity`, `integral_radialAngularMeasure`, `integrable_radialAngularMeasure_of_spherical`, `instHasTemperateGrowthRadialAngularMeasure`, `radialAngularMeasure_closedBall`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instHasTemperateGrowthRadialAngularMeasure` 📖	mathematical	—	`Space` `instNormedAddCommGroup` `instMeasurableSpace` `radialAngularMeasure`	—	`radialAngularMeasure_integrable_pow_neg_two`
`instSFiniteRadialAngularMeasure` 📖	mathematical	—	`Space` `instMeasurableSpace` `radialAngularMeasure`	—	`instFiniteDimensionalReal` `instBorelSpace`
`integrable_radialAngularMeasure_iff` 📖	mathematical	—	`Space` `instMeasurableSpace` `radialAngularMeasure` `instNormedAddCommGroup` `instInnerProductSpaceReal` `instFiniteDimensionalReal` `instBorelSpace` `instNorm`	—	`instFiniteDimensionalReal` `instBorelSpace`
`integrable_radialAngularMeasure_of_spherical` 📖	mathematical	`Space` `instMeasurableSpace` `instNormedAddCommGroup` `instInnerProductSpaceReal` `instFiniteDimensionalReal` `instBorelSpace` `instSMulReal`	`Space` `instMeasurableSpace` `radialAngularMeasure`	—	`instFiniteDimensionalReal` `instBorelSpace` `lintegral_radialMeasure_eq_spherical_mul`
`integral_radialAngularMeasure` 📖	mathematical	—	`Space` `instMeasurableSpace` `radialAngularMeasure` `instNormedAddCommGroup` `instInnerProductSpaceReal` `instFiniteDimensionalReal` `instBorelSpace` `instNorm`	—	`instFiniteDimensionalReal` `instBorelSpace`
`lintegral_radialMeasure` 📖	mathematical	`Space` `instMeasurableSpace`	`Space` `instMeasurableSpace` `radialAngularMeasure` `instNormedAddCommGroup` `instInnerProductSpaceReal` `instFiniteDimensionalReal` `instBorelSpace` `instNorm`	—	`instFiniteDimensionalReal` `instBorelSpace`
`lintegral_radialMeasure_eq_spherical_mul` 📖	mathematical	`Space` `instMeasurableSpace`	`Space` `instMeasurableSpace` `radialAngularMeasure` `instNormedAddCommGroup` `instInnerProductSpaceReal` `instFiniteDimensionalReal` `instBorelSpace` `instSMulReal`	—	`instFiniteDimensionalReal` `instBorelSpace` `lintegral_radialMeasure` `lintegral_volume_eq_spherical_mul`
`radialAngularMeasure_closedBall` 📖	mathematical	—	`Space` `instMeasurableSpace` `radialAngularMeasure` `instPseudoMetricSpace` `instZero`	—	`instBorelSpace` `instFiniteDimensionalReal` `lintegral_radialMeasure_eq_spherical_mul` `instSFiniteElemRealIoiOfNatComapValMemSetVolume` `finrank_eq_dim` `volume_metricBall_three`
`radialAngularMeasure_eq_volume_withDensity` 📖	mathematical	—	`radialAngularMeasure` `Space` `instNormedAddCommGroup` `instInnerProductSpaceReal` `instFiniteDimensionalReal` `instMeasurableSpace` `instBorelSpace` `instNorm`	—	—
`radialAngularMeasure_integrable_pow_neg_two` 📖	mathematical	—	`Space` `instMeasurableSpace` `instNorm` `radialAngularMeasure`	—	`instFiniteDimensionalReal` `instBorelSpace` `radialAngularMeasure_zero_eq_volume` `instSubsingletonOfNatNat` `integrable_radialAngularMeasure_of_spherical`
`radialAngularMeasure_real_closedBall` 📖	mathematical	—	`Space` `instMeasurableSpace` `radialAngularMeasure` `instPseudoMetricSpace` `instZero`	—	`radialAngularMeasure_closedBall`
`radialAngularMeasure_zero_eq_volume` 📖	mathematical	—	`radialAngularMeasure` `Space` `instNormedAddCommGroup` `instInnerProductSpaceReal` `instFiniteDimensionalReal` `instMeasurableSpace` `instBorelSpace`	—	`instFiniteDimensionalReal` `instBorelSpace`

---

← Back to Index