Theorem MeasureTheory.volume_sum_rpow_lt_one

Modification history

2024-08-12 18:29
Mathlib/MeasureTheory/Measure/Lebesgue/VolumeOfBalls.lean
chore: move to v4.11.0-rc2 (new `variable` command) (#15726)
Modified MeasureTheory.volume_sum_rpow_lt_oneView on Github →
2023-12-07 17:41
Mathlib/MeasureTheory/Measure/Lebesgue/VolumeOfBalls.lean
feat: Compute volume of balls of higher dimension for Lp norms (#8030) …
Added MeasureTheory.volume_sum_rpow_lt_oneView on Github →