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. HasTemperateGrowth of measures
  • C.1. Integrability of powers
  • C.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

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

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

C. HasTemperateGrowth of measures

C.1. Integrability of powers

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

C.2. radialAngularMeasure has temperate growth

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