Documentation Verification Report

Basic

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

Statistics

Metric	Count
Definitions	0
Theorems `instSFiniteElemRealIoiOfNatComapValMemSetVolume`, `integral_one_dim_eq_integral_real`, `integral_volume_eq_spherical`, `lintegral_volume_eq_spherical`, `lintegral_volume_eq_spherical_mul`, `volume_closedBall_ne_top`, `volume_closedBall_ne_zero`, `volume_eq_addHaar`, `volume_metricBall_three`, `volume_metricBall_three_real`, `volume_metricBall_two`, `volume_metricBall_two_real`	12
Total	12

Space

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instSFiniteElemRealIoiOfNatComapValMemSetVolume` 📖	—	—	—	—	—
`integral_one_dim_eq_integral_real` 📖	mathematical	—	`Space` `instNormedAddCommGroup` `instInnerProductSpaceReal` `instFiniteDimensionalReal` `instMeasurableSpace` `instBorelSpace` `instSeminormedAddCommGroup` `instModuleReal` `oneEquiv`	—	`instFiniteDimensionalReal` `instBorelSpace`
`integral_volume_eq_spherical` 📖	mathematical	—	`Space` `instNormedAddCommGroup` `instInnerProductSpaceReal` `instFiniteDimensionalReal` `instMeasurableSpace` `instBorelSpace` `instAddCommMonoid` `instModuleReal` `instSMulReal`	—	`instFiniteDimensionalReal` `instBorelSpace` `instNontrivialSucc`
`lintegral_volume_eq_spherical` 📖	mathematical	`Space` `instMeasurableSpace`	`Space` `instNormedAddCommGroup` `instInnerProductSpaceReal` `instFiniteDimensionalReal` `instMeasurableSpace` `instBorelSpace` `instAddCommMonoid` `instModuleReal` `instSMulReal`	—	`instFiniteDimensionalReal` `instBorelSpace` `instNontrivialSucc`
`lintegral_volume_eq_spherical_mul` 📖	mathematical	`Space` `instMeasurableSpace`	`Space` `instNormedAddCommGroup` `instInnerProductSpaceReal` `instFiniteDimensionalReal` `instMeasurableSpace` `instBorelSpace` `instSMulReal`	—	`instFiniteDimensionalReal` `instBorelSpace` `lintegral_volume_eq_spherical` `instSFiniteElemRealIoiOfNatComapValMemSetVolume` `finrank_eq_dim`
`volume_closedBall_ne_top` 📖	—	—	—	—	`instFiniteDimensionalReal` `instBorelSpace` `instNontrivialSucc` `finrank_eq_dim`
`volume_closedBall_ne_zero` 📖	—	—	—	—	`instFiniteDimensionalReal` `instBorelSpace` `instNontrivialSucc` `finrank_eq_dim`
`volume_eq_addHaar` 📖	mathematical	—	`Space` `instNormedAddCommGroup` `instInnerProductSpaceReal` `instFiniteDimensionalReal` `instMeasurableSpace` `instBorelSpace` `basis`	—	`instBorelSpace` `instFiniteDimensionalReal`
`volume_metricBall_three` 📖	mathematical	—	`Space` `instNormedAddCommGroup` `instInnerProductSpaceReal` `instFiniteDimensionalReal` `instMeasurableSpace` `instBorelSpace` `instPseudoMetricSpace` `instZero`	—	`instFiniteDimensionalReal` `instBorelSpace` `finrank_eq_dim`
`volume_metricBall_three_real` 📖	mathematical	—	`Space` `instNormedAddCommGroup` `instInnerProductSpaceReal` `instFiniteDimensionalReal` `instMeasurableSpace` `instBorelSpace` `instPseudoMetricSpace` `instZero`	—	`instFiniteDimensionalReal` `instBorelSpace` `volume_metricBall_three`
`volume_metricBall_two` 📖	mathematical	—	`Space` `instNormedAddCommGroup` `instInnerProductSpaceReal` `instFiniteDimensionalReal` `instMeasurableSpace` `instBorelSpace` `instPseudoMetricSpace` `instZero`	—	`instFiniteDimensionalReal` `instBorelSpace` `instNontrivialSucc` `finrank_eq_dim`
`volume_metricBall_two_real` 📖	mathematical	—	`Space` `instNormedAddCommGroup` `instInnerProductSpaceReal` `instFiniteDimensionalReal` `instMeasurableSpace` `instBorelSpace` `instPseudoMetricSpace` `instZero`	—	`instFiniteDimensionalReal` `instBorelSpace` `volume_metricBall_two`

---

← Back to Index