The radial angular measure on Space

i. Overview

The normal measure on Space d is r^(d-1) dr dΩ in spherical coordinates, where dΩ is the angular measure on the unit sphere. The radial angular measure is the measure dr dΩ, cancelling the radius contribution from the measure in spherical coordinates.

This file is equivalent to invPowMeasure, which will slowly be deprecated.

ii. Key results

• radialAngularMeasure: The radial angular measure on Space d.

iii. Table of contents

• A. The definition of the radial angular measure
  • A.1. Basic equalities
• B. Integrals with respect to radialAngularMeasure
• C. The radialAngularMeasure on balls
• D. Integrability conditions
• E. HasTemperateGrowth of measures
  • E.1. Integrability of powers
  • E.2. radialAngularMeasure has temperate growth

iv. References

A. The definition of the radial angular measure

def Space.radialAngularMeasure {d : ℕ} : MeasureTheory.Measure (Space d)

The measure on Space d weighted by 1 / ‖x‖ ^ (d - 1).

Equations

• Space.radialAngularMeasure = MeasureTheory.volume.withDensity fun (x : Space d) => ENNReal.ofReal (1 / ‖x‖ ^ (d - 1))

A.1. Basic equalities

theorem Space.radialAngularMeasure_eq_volume_withDensity {d : ℕ} : radialAngularMeasure = MeasureTheory.volume.withDensity fun (x : Space d) => ENNReal.ofReal (1 / ‖x‖ ^ (d - 1))

@[simp]

theorem Space.radialAngularMeasure_zero_eq_volume : radialAngularMeasure = MeasureTheory.volume

A.2. SFinite property

instance Space.instSFiniteRadialAngularMeasure (d : ℕ) : MeasureTheory.SFinite radialAngularMeasure

B. Integrals with respect to radialAngularMeasure

theorem Space.integral_radialAngularMeasure {F : Type} [NormedAddCommGroup F] [NormedSpace ℝ F] {d : ℕ} (f : Space d → F) : ∫ (x : Space d), f x ∂radialAngularMeasure = ∫ (x : Space d), (1 / ‖x‖ ^ (d - 1)) • f x

theorem Space.lintegral_radialMeasure {d : ℕ} (f : Space d → ENNReal) (hf : Measurable f) : ∫⁻ (x : Space d), f x ∂radialAngularMeasure = ∫⁻ (x : Space d), ENNReal.ofReal (1 / ‖x‖ ^ (d - 1)) * f x

theorem Space.lintegral_radialMeasure_eq_spherical_mul (d : ℕ) (f : Space d.succ → ENNReal) (hf : Measurable f) : ∫⁻ (x : Space d.succ), f x ∂radialAngularMeasure = ∫⁻ (x : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)), f (↑x.2 • ↑x.1) ∂MeasureTheory.volume.toSphere.prod (MeasureTheory.Measure.volumeIoiPow 0)

C. The radialAngularMeasure on balls

@[simp]

theorem Space.radialAngularMeasure_closedBall (r : ℝ) : radialAngularMeasure (Metric.closedBall 0 r) = ENNReal.ofReal (4 * Real.pi * r)

theorem Space.radialAngularMeasure_real_closedBall (r : ℝ) (hr : 0 < r) : radialAngularMeasure.real (Metric.closedBall 0 r) = 4 * Real.pi * r

D. Integrability conditions

theorem Space.integrable_radialAngularMeasure_iff {F : Type} [NormedAddCommGroup F] [NormedSpace ℝ F] {d : ℕ} {f : Space d → F} : MeasureTheory.Integrable f radialAngularMeasure ↔ MeasureTheory.Integrable (fun (x : Space d) => (1 / ‖x‖ ^ (d - 1)) • f x) MeasureTheory.volume

theorem Space.integrable_radialAngularMeasure_of_spherical {F : Type} [NormedAddCommGroup F] {d : ℕ} (f : Space d.succ → F) (hae : MeasureTheory.StronglyMeasurable f) (hf : MeasureTheory.Integrable (fun (x : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)) => f (↑x.2 • ↑x.1)) (MeasureTheory.volume.toSphere.prod (MeasureTheory.Measure.volumeIoiPow 0))) : MeasureTheory.Integrable f radialAngularMeasure

E. HasTemperateGrowth of measures

E.1. Integrability of powers

theorem Space.radialAngularMeasure_integrable_pow_neg_two {d : ℕ} : MeasureTheory.Integrable (fun (x : Space d) => (1 + ‖x‖) ^ (-(↑d + 1))) radialAngularMeasure

E.2. radialAngularMeasure has temperate growth

instance Space.instHasTemperateGrowthRadialAngularMeasure (d : ℕ) : radialAngularMeasure.HasTemperateGrowth