Documentation Verification Report

RadialAngularMeasure

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

Statistics

Metric	Count
Definitions `radialAngularMeasure`	1
Theorems `instHasTemperateGrowthRadialAngularMeasure`, `integrable_radialAngularMeasure_iff`, `integral_radialAngularMeasure`, `radialAngularMeasure_eq_volume_withDensity`, `radialAngularMeasure_integrable_pow_neg_two`, `radialAngularMeasure_zero_eq_volume`	6
Total	7

Space

Definitions

Name	Category	Theorems
`radialAngularMeasure` 📖	CompOp	6 math math: `radialAngularMeasure_zero_eq_volume`, `integrable_radialAngularMeasure_iff`, `radialAngularMeasure_integrable_pow_neg_two`, `radialAngularMeasure_eq_volume_withDensity`, `integral_radialAngularMeasure`, `instHasTemperateGrowthRadialAngularMeasure`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instHasTemperateGrowthRadialAngularMeasure` 📖	mathematical	—	`Space` `instNormedAddCommGroup` `instMeasurableSpace` `radialAngularMeasure`	—	`radialAngularMeasure_integrable_pow_neg_two`
`integrable_radialAngularMeasure_iff` 📖	mathematical	—	`Space` `instMeasurableSpace` `radialAngularMeasure` `instNormedAddCommGroup` `instInnerProductSpaceReal` `instFiniteDimensionalReal` `instBorelSpace` `instNorm`	—	`instFiniteDimensionalReal` `instBorelSpace`
`integral_radialAngularMeasure` 📖	mathematical	—	`Space` `instMeasurableSpace` `radialAngularMeasure` `instNormedAddCommGroup` `instInnerProductSpaceReal` `instFiniteDimensionalReal` `instBorelSpace` `instNorm`	—	`instFiniteDimensionalReal` `instBorelSpace`
`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` `finrank_eq_dim` `instNontrivialSucc`
`radialAngularMeasure_zero_eq_volume` 📖	mathematical	—	`radialAngularMeasure` `Space` `instNormedAddCommGroup` `instInnerProductSpaceReal` `instFiniteDimensionalReal` `instMeasurableSpace` `instBorelSpace`	—	`instFiniteDimensionalReal` `instBorelSpace`

---

← Back to Index