Project-declaredLean 4.32.0
Radial Angular Measure closed Ball
Space.radialAngularMeasure_closedBall
Project documentation
The measure on Space d weighted by 1 / ‖x‖ ^ (d - 1). -/ def radialAngularMeasure {d : ℕ} : Measure (Space d) := volume.withDensity (fun x : Space d => ENNReal.ofReal (1 / ‖x‖ ^ (d - 1))) /-! ### A.1. Basic equalities -/ lemma radialAngularMeasure_eq_volume_withDensity {d : ℕ} : radialAngularMeasure = volume.withDensity (fun x : Space d => ENNReal.ofR...
physicsquantum field theoryrelativity
Source project: Physlib
Person-level attribution pending.