Physlib.SpaceAndTime.Space.Integrals.RadialAngularMeasure — Physlib

Physlib
SpaceAndTime
Space
Integrals
RadialAngularMeasure

Imports

/-
Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
module

public import Physlib.SpaceAndTime.Space.Integrals.Basic

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

@[expose] public section

A. The definition of the radial angular measure

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.ofReal (1 / ‖x‖ ^ (d - 1))) := byd:ℕ⊢ radialAngularMeasure = volume.withDensity fun x => ENNReal.ofReal (1 / ‖x‖ ^ (d - 1))
  rflAll goals completed! 🐙

@[simp]
lemma radialAngularMeasure_zero_eq_volume :
    radialAngularMeasure (d := 0) = volume := by⊢ radialAngularMeasure = volume
  simp [radialAngularMeasure]All goals completed! 🐙

A.2. SFinite property

instance (d : ℕ) : SFinite (radialAngularMeasure (d := d)) := by𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ Fd:ℕ⊢ SFinite radialAngularMeasure
  dsimp [radialAngularMeasure]𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ Fd:ℕ⊢ SFinite (volume.withDensity fun x => ENNReal.ofReal (1 / ‖x‖ ^ (d - 1)))
  infer_instanceAll goals completed! 🐙

B. Integrals with respect to radialAngularMeasure

              

lemma integral_radialAngularMeasure {d : ℕ} (f : Space d → F) :
    ∫ x, f x ∂radialAngularMeasure = ∫ x, (1 / ‖x‖ ^ (d - 1)) • f x := byF:Typeinst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Fd:ℕf:Space d → F⊢ ∫ (x : Space d), f x ∂radialAngularMeasure = ∫ (x : Space d), (1 / ‖x‖ ^ (d - 1)) • f x
  dsimp [radialAngularMeasure]F:Typeinst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Fd:ℕf:Space d → F⊢ (∫ (x : Space d), f x ∂volume.withDensity fun x => ENNReal.ofReal (1 / ‖x‖ ^ (d - 1))) =
  ∫ (x : Space d), (1 / ‖x‖ ^ (d - 1)) • f x
  erw [integral_withDensity_eq_integral_smul (byF:Typeinst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Fd:ℕf:Space d → F⊢ Measurable fun x => (1 / ‖x‖ ^ (d - 1)).toNNReal fun_propAll goals completed! 🐙)]F:Typeinst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Fd:ℕf:Space d → F⊢ ∫ (x : Space d), (1 / ‖x‖ ^ (d - 1)).toNNReal • f x ∂volume = ∫ (x : Space d), (1 / ‖x‖ ^ (d - 1)) • f x
  congre_fF:Typeinst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Fd:ℕf:Space d → F⊢ (fun x => (1 / ‖x‖ ^ (d - 1)).toNNReal • f x) = fun x => (1 / ‖x‖ ^ (d - 1)) • f x
  funext xe_fF:Typeinst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Fd:ℕf:Space d → Fx:Space d⊢ (1 / ‖x‖ ^ (d - 1)).toNNReal • f x = (1 / ‖x‖ ^ (d - 1)) • f x
  simp only [one_div]e_fF:Typeinst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Fd:ℕf:Space d → Fx:Space d⊢ (‖x‖ ^ (d - 1))⁻¹.toNNReal • f x = (‖x‖ ^ (d - 1))⁻¹ • f x
  rw [NNReal.smul_def,e_fF:Typeinst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Fd:ℕf:Space d → Fx:Space d⊢ ↑(‖x‖ ^ (d - 1))⁻¹.toNNReal • f x = (‖x‖ ^ (d - 1))⁻¹ • f xAll goals completed! 🐙 Real.coe_toNNReal _ (byF:Typeinst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Fd:ℕf:Space d → Fx:Space d⊢ 0 ≤ (‖x‖ ^ (d - 1))⁻¹All goals completed! 🐙 positivityAll goals completed! 🐙All goals completed! 🐙)]All goals completed! 🐙

lemma lintegral_radialMeasure {d : ℕ} (f : Space d → ENNReal) (hf : Measurable f) :
    ∫⁻ x, f x ∂radialAngularMeasure = ∫⁻ x, ENNReal.ofReal (1 / ‖x‖ ^ (d - 1)) * f x := byd:ℕf:Space d → ENNRealhf:Measurable f⊢ ∫⁻ (x : Space d), f x ∂radialAngularMeasure = ∫⁻ (x : Space d), ENNReal.ofReal (1 / ‖x‖ ^ (d - 1)) * f x
  dsimp [radialAngularMeasure]d:ℕf:Space d → ENNRealhf:Measurable f⊢ (∫⁻ (x : Space d), f x ∂volume.withDensity fun x => ENNReal.ofReal (1 / ‖x‖ ^ (d - 1))) =
  ∫⁻ (x : Space d), ENNReal.ofReal (1 / ‖x‖ ^ (d - 1)) * f x
  rw [lintegral_withDensity_eq_lintegral_muld:ℕf:Space d → ENNRealhf:Measurable f⊢ ∫⁻ (a : Space d), ((fun x => ENNReal.ofReal (1 / ‖x‖ ^ (d - 1))) * f) a ∂volume =
  ∫⁻ (x : Space d), ENNReal.ofReal (1 / ‖x‖ ^ (d - 1)) * f xh_mfd:ℕf:Space d → ENNRealhf:Measurable f⊢ Measurable fun x => ENNReal.ofReal (1 / ‖x‖ ^ (d - 1))ad:ℕf:Space d → ENNRealhf:Measurable f⊢ Measurable fd:ℕf:Space d → ENNRealhf:Measurable f⊢ ∫⁻ (a : Space d), ((fun x => ENNReal.ofReal (1 / ‖x‖ ^ (d - 1))) * f) a ∂volume =
  ∫⁻ (x : Space d), ENNReal.ofReal (1 / ‖x‖ ^ (d - 1)) * f xh_mfd:ℕf:Space d → ENNRealhf:Measurable f⊢ Measurable fun x => ENNReal.ofReal (1 / ‖x‖ ^ (d - 1))ad:ℕf:Space d → ENNRealhf:Measurable f⊢ Measurable f]d:ℕf:Space d → ENNRealhf:Measurable f⊢ ∫⁻ (a : Space d), ((fun x => ENNReal.ofReal (1 / ‖x‖ ^ (d - 1))) * f) a ∂volume =
  ∫⁻ (x : Space d), ENNReal.ofReal (1 / ‖x‖ ^ (d - 1)) * f xh_mfd:ℕf:Space d → ENNRealhf:Measurable f⊢ Measurable fun x => ENNReal.ofReal (1 / ‖x‖ ^ (d - 1))ad:ℕf:Space d → ENNRealhf:Measurable f⊢ Measurable f
  simp only [one_div, Pi.mul_apply]h_mfd:ℕf:Space d → ENNRealhf:Measurable f⊢ Measurable fun x => ENNReal.ofReal (1 / ‖x‖ ^ (d - 1))ad:ℕf:Space d → ENNRealhf:Measurable f⊢ Measurable f
  all_goals fun_propAll goals completed! 🐙

lemma lintegral_radialMeasure_eq_spherical_mul (d : ℕ) [NeZero d]
    (f : Space d → ENNReal) (hf : Measurable f) :
    ∫⁻ x, f x ∂radialAngularMeasure = ∫⁻ x, f (x.2.1 • x.1.1)
      ∂(volume (α := Space d).toSphere.prod (Measure.volumeIoiPow 0)) := byd:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ ∫⁻ (x : Space d), f x ∂radialAngularMeasure =
  ∫⁻ (x : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)), f (↑x.2 • ↑x.1) ∂volume.toSphere.prod (Measure.volumeIoiPow 0)
  rw [lintegral_radialMeasure,d:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ ∫⁻ (x : Space d), ENNReal.ofReal (1 / ‖x‖ ^ (d - 1)) * f x =
  ∫⁻ (x : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)), f (↑x.2 • ↑x.1) ∂volume.toSphere.prod (Measure.volumeIoiPow 0)hfd:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable fd:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ ∫⁻ (x : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)),
    ENNReal.ofReal (1 / ‖↑x.2 • ↑x.1‖ ^ (d - 1)) * f (↑x.2 • ↑x.1) *
      ENNReal.ofReal (↑x.2 ^ (d - 1)) ∂volume.toSphere.prod (Measure.volumeIoiPow 0) =
  ∫⁻ (x : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)), f (↑x.2 • ↑x.1) ∂volume.toSphere.prod (Measure.volumeIoiPow 0)hfd:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable fun x => ENNReal.ofReal (1 / ‖x‖ ^ (d - 1)) * f xhfd:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable f lintegral_volume_eq_spherical_muld:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ ∫⁻ (x : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)),
    ENNReal.ofReal (1 / ‖↑x.2 • ↑x.1‖ ^ (d - 1)) * f (↑x.2 • ↑x.1) *
      ENNReal.ofReal (↑x.2 ^ (d - 1)) ∂volume.toSphere.prod (Measure.volumeIoiPow 0) =
  ∫⁻ (x : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)), f (↑x.2 • ↑x.1) ∂volume.toSphere.prod (Measure.volumeIoiPow 0)hfd:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable fun x => ENNReal.ofReal (1 / ‖x‖ ^ (d - 1)) * f xhfd:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable fd:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ ∫⁻ (x : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)),
    ENNReal.ofReal (1 / ‖↑x.2 • ↑x.1‖ ^ (d - 1)) * f (↑x.2 • ↑x.1) *
      ENNReal.ofReal (↑x.2 ^ (d - 1)) ∂volume.toSphere.prod (Measure.volumeIoiPow 0) =
  ∫⁻ (x : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)), f (↑x.2 • ↑x.1) ∂volume.toSphere.prod (Measure.volumeIoiPow 0)hfd:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable fun x => ENNReal.ofReal (1 / ‖x‖ ^ (d - 1)) * f xhfd:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable f]d:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ ∫⁻ (x : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)),
    ENNReal.ofReal (1 / ‖↑x.2 • ↑x.1‖ ^ (d - 1)) * f (↑x.2 • ↑x.1) *
      ENNReal.ofReal (↑x.2 ^ (d - 1)) ∂volume.toSphere.prod (Measure.volumeIoiPow 0) =
  ∫⁻ (x : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)), f (↑x.2 • ↑x.1) ∂volume.toSphere.prod (Measure.volumeIoiPow 0)hfd:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable fun x => ENNReal.ofReal (1 / ‖x‖ ^ (d - 1)) * f xhfd:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable f
  apply lintegral_congr_aed:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ (fun a =>
    ENNReal.ofReal (1 / ‖↑a.2 • ↑a.1‖ ^ (d - 1)) * f (↑a.2 • ↑a.1) *
      ENNReal.ofReal (↑a.2 ^ (d - 1))) =ᵐ[volume.toSphere.prod (Measure.volumeIoiPow 0)]
  fun a => f (↑a.2 • ↑a.1)hfd:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable fun x => ENNReal.ofReal (1 / ‖x‖ ^ (d - 1)) * f xhfd:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable f
  filter_upwards with xd:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable fx:↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)⊢ ENNReal.ofReal (1 / ‖↑x.2 • ↑x.1‖ ^ (d - 1)) * f (↑x.2 • ↑x.1) * ENNReal.ofReal (↑x.2 ^ (d - 1)) = f (↑x.2 • ↑x.1)hfd:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable fun x => ENNReal.ofReal (1 / ‖x‖ ^ (d - 1)) * f xhfd:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable f
  have hpos : (0 : ℝ) < x.2 := x.2.2d:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable fx:↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)hpos:0 < ↑x.2⊢ ENNReal.ofReal (1 / ‖↑x.2 • ↑x.1‖ ^ (d - 1)) * f (↑x.2 • ↑x.1) * ENNReal.ofReal (↑x.2 ^ (d - 1)) = f (↑x.2 • ↑x.1)hfd:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable fun x => ENNReal.ofReal (1 / ‖x‖ ^ (d - 1)) * f xhfd:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable f
  have hnorm : ‖(x.2 : ℝ) • (x.1 : Space d)‖ = x.2 := byd:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ ∫⁻ (x : Space d), f x ∂radialAngularMeasure =
  ∫⁻ (x : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)), f (↑x.2 • ↑x.1) ∂volume.toSphere.prod (Measure.volumeIoiPow 0)d:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable fx:↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)hpos:0 < ↑x.2hnorm:‖↑x.2 • ↑x.1‖ = ↑x.2⊢ ENNReal.ofReal (1 / ‖↑x.2 • ↑x.1‖ ^ (d - 1)) * f (↑x.2 • ↑x.1) * ENNReal.ofReal (↑x.2 ^ (d - 1)) = f (↑x.2 • ↑x.1)hfd:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable fun x => ENNReal.ofReal (1 / ‖x‖ ^ (d - 1)) * f xhfd:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable f
    rw [norm_smul,d:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable fx:↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)hpos:0 < ↑x.2⊢ ‖↑x.2‖ * ‖↑x.1‖ = ↑x.2d:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable fx:↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)hpos:0 < ↑x.2hnorm:‖↑x.2 • ↑x.1‖ = ↑x.2⊢ ENNReal.ofReal (1 / ‖↑x.2 • ↑x.1‖ ^ (d - 1)) * f (↑x.2 • ↑x.1) * ENNReal.ofReal (↑x.2 ^ (d - 1)) = f (↑x.2 • ↑x.1)hfd:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable fun x => ENNReal.ofReal (1 / ‖x‖ ^ (d - 1)) * f xhfd:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable f mem_sphere_zero_iff_norm.mp x.1.2,d:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable fx:↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)hpos:0 < ↑x.2⊢ ‖↑x.2‖ * 1 = ↑x.2d:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable fx:↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)hpos:0 < ↑x.2hnorm:‖↑x.2 • ↑x.1‖ = ↑x.2⊢ ENNReal.ofReal (1 / ‖↑x.2 • ↑x.1‖ ^ (d - 1)) * f (↑x.2 • ↑x.1) * ENNReal.ofReal (↑x.2 ^ (d - 1)) = f (↑x.2 • ↑x.1)hfd:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable fun x => ENNReal.ofReal (1 / ‖x‖ ^ (d - 1)) * f xhfd:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable f mul_one,d:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable fx:↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)hpos:0 < ↑x.2⊢ ‖↑x.2‖ = ↑x.2d:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable fx:↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)hpos:0 < ↑x.2hnorm:‖↑x.2 • ↑x.1‖ = ↑x.2⊢ ENNReal.ofReal (1 / ‖↑x.2 • ↑x.1‖ ^ (d - 1)) * f (↑x.2 • ↑x.1) * ENNReal.ofReal (↑x.2 ^ (d - 1)) = f (↑x.2 • ↑x.1)hfd:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable fun x => ENNReal.ofReal (1 / ‖x‖ ^ (d - 1)) * f xhfd:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable f Real.norm_eq_abs,d:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable fx:↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)hpos:0 < ↑x.2⊢ |↑x.2| = ↑x.2d:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable fx:↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)hpos:0 < ↑x.2hnorm:‖↑x.2 • ↑x.1‖ = ↑x.2⊢ ENNReal.ofReal (1 / ‖↑x.2 • ↑x.1‖ ^ (d - 1)) * f (↑x.2 • ↑x.1) * ENNReal.ofReal (↑x.2 ^ (d - 1)) = f (↑x.2 • ↑x.1)hfd:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable fun x => ENNReal.ofReal (1 / ‖x‖ ^ (d - 1)) * f xhfd:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable f
      abs_of_nonneg hpos.led:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable fx:↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)hpos:0 < ↑x.2⊢ ↑x.2 = ↑x.2d:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable fx:↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)hpos:0 < ↑x.2hnorm:‖↑x.2 • ↑x.1‖ = ↑x.2⊢ ENNReal.ofReal (1 / ‖↑x.2 • ↑x.1‖ ^ (d - 1)) * f (↑x.2 • ↑x.1) * ENNReal.ofReal (↑x.2 ^ (d - 1)) = f (↑x.2 • ↑x.1)hfd:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable fun x => ENNReal.ofReal (1 / ‖x‖ ^ (d - 1)) * f xhfd:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable f]d:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable fx:↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)hpos:0 < ↑x.2hnorm:‖↑x.2 • ↑x.1‖ = ↑x.2⊢ ENNReal.ofReal (1 / ‖↑x.2 • ↑x.1‖ ^ (d - 1)) * f (↑x.2 • ↑x.1) * ENNReal.ofReal (↑x.2 ^ (d - 1)) = f (↑x.2 • ↑x.1)hfd:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable fun x => ENNReal.ofReal (1 / ‖x‖ ^ (d - 1)) * f xhfd:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable fd:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable fx:↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)hpos:0 < ↑x.2hnorm:‖↑x.2 • ↑x.1‖ = ↑x.2⊢ ENNReal.ofReal (1 / ‖↑x.2 • ↑x.1‖ ^ (d - 1)) * f (↑x.2 • ↑x.1) * ENNReal.ofReal (↑x.2 ^ (d - 1)) = f (↑x.2 • ↑x.1)hfd:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable fun x => ENNReal.ofReal (1 / ‖x‖ ^ (d - 1)) * f xhfd:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable f
  rw [hnorm,d:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable fx:↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)hpos:0 < ↑x.2hnorm:‖↑x.2 • ↑x.1‖ = ↑x.2⊢ ENNReal.ofReal (1 / ↑x.2 ^ (d - 1)) * f (↑x.2 • ↑x.1) * ENNReal.ofReal (↑x.2 ^ (d - 1)) = f (↑x.2 • ↑x.1)hfd:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable fun x => ENNReal.ofReal (1 / ‖x‖ ^ (d - 1)) * f xhfd:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable fhfd:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable fun x => ENNReal.ofReal (1 / ‖x‖ ^ (d - 1)) * f xhfd:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable f mul_right_comm,d:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable fx:↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)hpos:0 < ↑x.2hnorm:‖↑x.2 • ↑x.1‖ = ↑x.2⊢ ENNReal.ofReal (1 / ↑x.2 ^ (d - 1)) * ENNReal.ofReal (↑x.2 ^ (d - 1)) * f (↑x.2 • ↑x.1) = f (↑x.2 • ↑x.1)hfd:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable fun x => ENNReal.ofReal (1 / ‖x‖ ^ (d - 1)) * f xhfd:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable fhfd:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable fun x => ENNReal.ofReal (1 / ‖x‖ ^ (d - 1)) * f xhfd:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable f ← ENNReal.ofReal_mul (byd:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable fx:↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)hpos:0 < ↑x.2hnorm:‖↑x.2 • ↑x.1‖ = ↑x.2⊢ 0 ≤ 1 / ↑x.2 ^ (d - 1)hfd:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable fun x => ENNReal.ofReal (1 / ‖x‖ ^ (d - 1)) * f xhfd:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable f positivityAll goals completed! 🐙hfd:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable fun x => ENNReal.ofReal (1 / ‖x‖ ^ (d - 1)) * f xhfd:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable f), one_div,d:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable fx:↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)hpos:0 < ↑x.2hnorm:‖↑x.2 • ↑x.1‖ = ↑x.2⊢ ENNReal.ofReal ((↑x.2 ^ (d - 1))⁻¹ * ↑x.2 ^ (d - 1)) * f (↑x.2 • ↑x.1) = f (↑x.2 • ↑x.1)hfd:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable fun x => ENNReal.ofReal (1 / ‖x‖ ^ (d - 1)) * f xhfd:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable fhfd:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable fun x => ENNReal.ofReal (1 / ‖x‖ ^ (d - 1)) * f xhfd:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable f
    inv_mul_cancel₀ (byd:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable fx:↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)hpos:0 < ↑x.2hnorm:‖↑x.2 • ↑x.1‖ = ↑x.2⊢ ↑x.2 ^ (d - 1) ≠ 0hfd:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable fun x => ENNReal.ofReal (1 / ‖x‖ ^ (d - 1)) * f xhfd:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable f positivityAll goals completed! 🐙hfd:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable fun x => ENNReal.ofReal (1 / ‖x‖ ^ (d - 1)) * f xhfd:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable f), ENNReal.ofReal_one,d:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable fx:↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)hpos:0 < ↑x.2hnorm:‖↑x.2 • ↑x.1‖ = ↑x.2⊢ 1 * f (↑x.2 • ↑x.1) = f (↑x.2 • ↑x.1)hfd:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable fun x => ENNReal.ofReal (1 / ‖x‖ ^ (d - 1)) * f xhfd:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable fhfd:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable fun x => ENNReal.ofReal (1 / ‖x‖ ^ (d - 1)) * f xhfd:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable f one_muld:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable fx:↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)hpos:0 < ↑x.2hnorm:‖↑x.2 • ↑x.1‖ = ↑x.2⊢ f (↑x.2 • ↑x.1) = f (↑x.2 • ↑x.1)hfd:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable fun x => ENNReal.ofReal (1 / ‖x‖ ^ (d - 1)) * f xhfd:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable fhfd:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable fun x => ENNReal.ofReal (1 / ‖x‖ ^ (d - 1)) * f xhfd:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable f]hfd:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable fun x => ENNReal.ofReal (1 / ‖x‖ ^ (d - 1)) * f xhfd:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable f
  all_goals fun_propAll goals completed! 🐙

C. The radialAngularMeasure on balls



@[simp]
lemma radialAngularMeasure_closedBall (r : ℝ) :
    radialAngularMeasure (Metric.closedBall (0 : Space 3) r) = ENNReal.ofReal (4 * π * r) := byr:ℝ⊢ radialAngularMeasure (Metric.closedBall 0 r) = ENNReal.ofReal (4 * π * r)
  rw [← setLIntegral_one,r:ℝ⊢ ∫⁻ (x : Space) in Metric.closedBall 0 r, 1 ∂radialAngularMeasure = ENNReal.ofReal (4 * π * r)r:ℝ⊢ ∫⁻ (x : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)),
    (Metric.closedBall 0 r).indicator (fun x => 1) (↑x.2 • ↑x.1) ∂volume.toSphere.prod (Measure.volumeIoiPow 0) =
  ENNReal.ofReal (4 * π * r) ← MeasureTheory.lintegral_indicator measurableSet_closedBall,r:ℝ⊢ ∫⁻ (a : Space), (Metric.closedBall 0 r).indicator (fun x => 1) a ∂radialAngularMeasure = ENNReal.ofReal (4 * π * r)r:ℝ⊢ ∫⁻ (x : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)),
    (Metric.closedBall 0 r).indicator (fun x => 1) (↑x.2 • ↑x.1) ∂volume.toSphere.prod (Measure.volumeIoiPow 0) =
  ENNReal.ofReal (4 * π * r)
    lintegral_radialMeasure_eq_spherical_mul _ _
    ((measurable_indicator_const_iff 1).mpr measurableSet_closedBall)r:ℝ⊢ ∫⁻ (x : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)),
    (Metric.closedBall 0 r).indicator (fun x => 1) (↑x.2 • ↑x.1) ∂volume.toSphere.prod (Measure.volumeIoiPow 0) =
  ENNReal.ofReal (4 * π * r)r:ℝ⊢ ∫⁻ (x : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)),
    (Metric.closedBall 0 r).indicator (fun x => 1) (↑x.2 • ↑x.1) ∂volume.toSphere.prod (Measure.volumeIoiPow 0) =
  ENNReal.ofReal (4 * π * r)]r:ℝ⊢ ∫⁻ (x : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)),
    (Metric.closedBall 0 r).indicator (fun x => 1) (↑x.2 • ↑x.1) ∂volume.toSphere.prod (Measure.volumeIoiPow 0) =
  ENNReal.ofReal (4 * π * r)
  have h1 (x : (Metric.sphere (0 : Space) 1) × ↑(Set.Ioi (0 : ℝ))) :
      (Metric.closedBall (0 : Space) r).indicator (fun x => (1 : ENNReal)) (x.2.1 • x.1.1) =
      (Set.univ ×ˢ {a | a.1 ≤ r}).indicator (fun x => 1) x :=
      Set.indicator_const_eq_indicator_const <| byr:ℝx:↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)⊢ ↑x.2 • ↑x.1 ∈ Metric.closedBall 0 r ↔ x ∈ Set.univ ×ˢ {a | ↑a ≤ r}r:ℝh1:∀ (x : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)),
  (Metric.closedBall 0 r).indicator (fun x => 1) (↑x.2 • ↑x.1) = (Set.univ ×ˢ {a | ↑a ≤ r}).indicator (fun x => 1) x⊢ ∫⁻ (x : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)),
    (Metric.closedBall 0 r).indicator (fun x => 1) (↑x.2 • ↑x.1) ∂volume.toSphere.prod (Measure.volumeIoiPow 0) =
  ENNReal.ofReal (4 * π * r)
    simp [norm_smul]r:ℝx:↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)⊢ |↑x.2| ≤ r ↔ ↑x.2 ≤ rr:ℝh1:∀ (x : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)),
  (Metric.closedBall 0 r).indicator (fun x => 1) (↑x.2 • ↑x.1) = (Set.univ ×ˢ {a | ↑a ≤ r}).indicator (fun x => 1) x⊢ ∫⁻ (x : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)),
    (Metric.closedBall 0 r).indicator (fun x => 1) (↑x.2 • ↑x.1) ∂volume.toSphere.prod (Measure.volumeIoiPow 0) =
  ENNReal.ofReal (4 * π * r)
    rw [abs_of_nonneg (le_of_lt x.2.2)r:ℝx:↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)⊢ ↑x.2 ≤ r ↔ ↑x.2 ≤ rr:ℝh1:∀ (x : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)),
  (Metric.closedBall 0 r).indicator (fun x => 1) (↑x.2 • ↑x.1) = (Set.univ ×ˢ {a | ↑a ≤ r}).indicator (fun x => 1) x⊢ ∫⁻ (x : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)),
    (Metric.closedBall 0 r).indicator (fun x => 1) (↑x.2 • ↑x.1) ∂volume.toSphere.prod (Measure.volumeIoiPow 0) =
  ENNReal.ofReal (4 * π * r)]r:ℝh1:∀ (x : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)),
  (Metric.closedBall 0 r).indicator (fun x => 1) (↑x.2 • ↑x.1) = (Set.univ ×ˢ {a | ↑a ≤ r}).indicator (fun x => 1) x⊢ ∫⁻ (x : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)),
    (Metric.closedBall 0 r).indicator (fun x => 1) (↑x.2 • ↑x.1) ∂volume.toSphere.prod (Measure.volumeIoiPow 0) =
  ENNReal.ofReal (4 * π * r)r:ℝh1:∀ (x : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)),
  (Metric.closedBall 0 r).indicator (fun x => 1) (↑x.2 • ↑x.1) = (Set.univ ×ˢ {a | ↑a ≤ r}).indicator (fun x => 1) x⊢ ∫⁻ (x : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)),
    (Metric.closedBall 0 r).indicator (fun x => 1) (↑x.2 • ↑x.1) ∂volume.toSphere.prod (Measure.volumeIoiPow 0) =
  ENNReal.ofReal (4 * π * r)
  simp [h1]r:ℝh1:∀ (x : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)),
  (Metric.closedBall 0 r).indicator (fun x => 1) (↑x.2 • ↑x.1) = (Set.univ ×ˢ {a | ↑a ≤ r}).indicator (fun x => 1) x⊢ ∫⁻ (x : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)),
    (Set.univ ×ˢ {a | ↑a ≤ r}).indicator (fun x => 1) x ∂volume.toSphere.prod (Measure.volumeIoiPow 0) =
  ENNReal.ofReal (4 * π * r)
  rw [MeasureTheory.lintegral_indicator <|
    MeasurableSet.prod MeasurableSet.univ (measurableSet_setOf.mpr (byr:ℝh1:∀ (x : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)),
  (Metric.closedBall 0 r).indicator (fun x => 1) (↑x.2 • ↑x.1) = (Set.univ ×ˢ {a | ↑a ≤ r}).indicator (fun x => 1) x⊢ Measurable fun a => ↑a ≤ rr:ℝh1:∀ (x : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)),
  (Metric.closedBall 0 r).indicator (fun x => 1) (↑x.2 • ↑x.1) = (Set.univ ×ˢ {a | ↑a ≤ r}).indicator (fun x => 1) x⊢ ∫⁻ (a : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)) in Set.univ ×ˢ {a | ↑a ≤ r},
    1 ∂volume.toSphere.prod (Measure.volumeIoiPow 0) =
  ENNReal.ofReal (4 * π * r) fun_propAll goals completed! 🐙r:ℝh1:∀ (x : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)),
  (Metric.closedBall 0 r).indicator (fun x => 1) (↑x.2 • ↑x.1) = (Set.univ ×ˢ {a | ↑a ≤ r}).indicator (fun x => 1) x⊢ ∫⁻ (a : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)) in Set.univ ×ˢ {a | ↑a ≤ r},
    1 ∂volume.toSphere.prod (Measure.volumeIoiPow 0) =
  ENNReal.ofReal (4 * π * r)))]r:ℝh1:∀ (x : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)),
  (Metric.closedBall 0 r).indicator (fun x => 1) (↑x.2 • ↑x.1) = (Set.univ ×ˢ {a | ↑a ≤ r}).indicator (fun x => 1) x⊢ ∫⁻ (a : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)) in Set.univ ×ˢ {a | ↑a ≤ r},
    1 ∂volume.toSphere.prod (Measure.volumeIoiPow 0) =
  ENNReal.ofReal (4 * π * r)
  simp [MeasureTheory.Measure.prod_prod, Measure.volumeIoiPow]r:ℝh1:∀ (x : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)),
  (Metric.closedBall 0 r).indicator (fun x => 1) (↑x.2 • ↑x.1) = (Set.univ ×ˢ {a | ↑a ≤ r}).indicator (fun x => 1) x⊢ 3 * ENNReal.ofReal (4 / 3 * π) * (Measure.comap Subtype.val volume) {a | ↑a ≤ r} = ENNReal.ofReal (4 * π * r)
  rw [MeasureTheory.Measure.comap_apply _ Subtype.val_injective
    (fun s hs => MeasurableSet.subtype_image measurableSet_Ioi hs)
    _ (measurableSet_setOf.mpr (byr:ℝh1:∀ (x : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)),
  (Metric.closedBall 0 r).indicator (fun x => 1) (↑x.2 • ↑x.1) = (Set.univ ×ˢ {a | ↑a ≤ r}).indicator (fun x => 1) x⊢ Measurable fun a => ↑a ≤ rr:ℝh1:∀ (x : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)),
  (Metric.closedBall 0 r).indicator (fun x => 1) (↑x.2 • ↑x.1) = (Set.univ ×ˢ {a | ↑a ≤ r}).indicator (fun x => 1) x⊢ 3 * ENNReal.ofReal (4 / 3 * π) * volume (Subtype.val '' {a | ↑a ≤ r}) = ENNReal.ofReal (4 * π * r) fun_propAll goals completed! 🐙r:ℝh1:∀ (x : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)),
  (Metric.closedBall 0 r).indicator (fun x => 1) (↑x.2 • ↑x.1) = (Set.univ ×ˢ {a | ↑a ≤ r}).indicator (fun x => 1) x⊢ 3 * ENNReal.ofReal (4 / 3 * π) * volume (Subtype.val '' {a | ↑a ≤ r}) = ENNReal.ofReal (4 * π * r)))]r:ℝh1:∀ (x : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)),
  (Metric.closedBall 0 r).indicator (fun x => 1) (↑x.2 • ↑x.1) = (Set.univ ×ˢ {a | ↑a ≤ r}).indicator (fun x => 1) x⊢ 3 * ENNReal.ofReal (4 / 3 * π) * volume (Subtype.val '' {a | ↑a ≤ r}) = ENNReal.ofReal (4 * π * r)
  trans 3 * ENNReal.ofReal (4 / 3 * π) * volume (α := ℝ) (Set.Ioc 0 r)r:ℝh1:∀ (x : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)),
  (Metric.closedBall 0 r).indicator (fun x => 1) (↑x.2 • ↑x.1) = (Set.univ ×ˢ {a | ↑a ≤ r}).indicator (fun x => 1) x⊢ 3 * ENNReal.ofReal (4 / 3 * π) * volume (Subtype.val '' {a | ↑a ≤ r}) =
  3 * ENNReal.ofReal (4 / 3 * π) * volume (Set.Ioc 0 r)r:ℝh1:∀ (x : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)),
  (Metric.closedBall 0 r).indicator (fun x => 1) (↑x.2 • ↑x.1) = (Set.univ ×ˢ {a | ↑a ≤ r}).indicator (fun x => 1) x⊢ 3 * ENNReal.ofReal (4 / 3 * π) * volume (Set.Ioc 0 r) = ENNReal.ofReal (4 * π * r)
  ·r:ℝh1:∀ (x : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)),
  (Metric.closedBall 0 r).indicator (fun x => 1) (↑x.2 • ↑x.1) = (Set.univ ×ˢ {a | ↑a ≤ r}).indicator (fun x => 1) x⊢ 3 * ENNReal.ofReal (4 / 3 * π) * volume (Subtype.val '' {a | ↑a ≤ r}) =
  3 * ENNReal.ofReal (4 / 3 * π) * volume (Set.Ioc 0 r) congre_a.e_6r:ℝh1:∀ (x : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)),
  (Metric.closedBall 0 r).indicator (fun x => 1) (↑x.2 • ↑x.1) = (Set.univ ×ˢ {a | ↑a ≤ r}).indicator (fun x => 1) x⊢ Subtype.val '' {a | ↑a ≤ r} = Set.Ioc 0 r
    ext xe_a.e_6r:ℝh1:∀ (x : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)),
  (Metric.closedBall 0 r).indicator (fun x => 1) (↑x.2 • ↑x.1) = (Set.univ ×ˢ {a | ↑a ≤ r}).indicator (fun x => 1) xx:ℝ⊢ x ∈ Subtype.val '' {a | ↑a ≤ r} ↔ x ∈ Set.Ioc 0 r
    simp only [Set.mem_image, Set.mem_setOf_eq, Subtype.exists, Set.mem_Ioi, exists_and_left,
      exists_prop, exists_eq_right_right, Set.mem_Ioc]e_a.e_6r:ℝh1:∀ (x : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)),
  (Metric.closedBall 0 r).indicator (fun x => 1) (↑x.2 • ↑x.1) = (Set.univ ×ˢ {a | ↑a ≤ r}).indicator (fun x => 1) xx:ℝ⊢ x ≤ r ∧ 0 < x ↔ 0 < x ∧ x ≤ r
    grindAll goals completed! 🐙
  simp only [volume_Ioc, sub_zero]r:ℝh1:∀ (x : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)),
  (Metric.closedBall 0 r).indicator (fun x => 1) (↑x.2 • ↑x.1) = (Set.univ ×ˢ {a | ↑a ≤ r}).indicator (fun x => 1) x⊢ 3 * ENNReal.ofReal (4 / 3 * π) * ENNReal.ofReal r = ENNReal.ofReal (4 * π * r)
  trans ENNReal.ofReal (3 * ((4 / 3 * π))) * ENNReal.ofReal rr:ℝh1:∀ (x : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)),
  (Metric.closedBall 0 r).indicator (fun x => 1) (↑x.2 • ↑x.1) = (Set.univ ×ˢ {a | ↑a ≤ r}).indicator (fun x => 1) x⊢ 3 * ENNReal.ofReal (4 / 3 * π) * ENNReal.ofReal r = ENNReal.ofReal (3 * (4 / 3 * π)) * ENNReal.ofReal rr:ℝh1:∀ (x : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)),
  (Metric.closedBall 0 r).indicator (fun x => 1) (↑x.2 • ↑x.1) = (Set.univ ×ˢ {a | ↑a ≤ r}).indicator (fun x => 1) x⊢ ENNReal.ofReal (3 * (4 / 3 * π)) * ENNReal.ofReal r = ENNReal.ofReal (4 * π * r)
  ·r:ℝh1:∀ (x : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)),
  (Metric.closedBall 0 r).indicator (fun x => 1) (↑x.2 • ↑x.1) = (Set.univ ×ˢ {a | ↑a ≤ r}).indicator (fun x => 1) x⊢ 3 * ENNReal.ofReal (4 / 3 * π) * ENNReal.ofReal r = ENNReal.ofReal (3 * (4 / 3 * π)) * ENNReal.ofReal r simp [ENNReal.ofReal_mul]All goals completed! 🐙
  field_simpr:ℝh1:∀ (x : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)),
  (Metric.closedBall 0 r).indicator (fun x => 1) (↑x.2 • ↑x.1) = (Set.univ ×ˢ {a | ↑a ≤ r}).indicator (fun x => 1) x⊢ ENNReal.ofReal (4 * π) * ENNReal.ofReal r = ENNReal.ofReal (4 * π * r)
  rw [← ENNReal.ofReal_mul (byr:ℝh1:∀ (x : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)),
  (Metric.closedBall 0 r).indicator (fun x => 1) (↑x.2 • ↑x.1) = (Set.univ ×ˢ {a | ↑a ≤ r}).indicator (fun x => 1) x⊢ 0 ≤ 4 * πAll goals completed! 🐙 positivityAll goals completed! 🐙All goals completed! 🐙)]All goals completed! 🐙

lemma radialAngularMeasure_real_closedBall (r : ℝ) (hr : 0 < r) :
    radialAngularMeasure.real (Metric.closedBall (0 : Space 3) r) = 4 * π * r := byr:ℝhr:0 < r⊢ radialAngularMeasure.real (Metric.closedBall 0 r) = 4 * π * r
  change (radialAngularMeasure (Metric.closedBall (0 : Space 3) r)).toReal = _r:ℝhr:0 < r⊢ (radialAngularMeasure (Metric.closedBall 0 r)).toReal = 4 * π * r
  simp only [radialAngularMeasure_closedBall, ENNReal.toReal_ofReal_eq_iff]r:ℝhr:0 < r⊢ 0 ≤ 4 * π * r
  positivityAll goals completed! 🐙

D. Integrability conditions



lemma integrable_radialAngularMeasure_iff {d : ℕ} {f : Space d → F} :
    Integrable f (radialAngularMeasure (d := d)) ↔
      Integrable (fun x => (1 / ‖x‖ ^ (d - 1)) • f x) volume := byF:Typeinst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Fd:ℕf:Space d → F⊢ Integrable f radialAngularMeasure ↔ Integrable (fun x => (1 / ‖x‖ ^ (d - 1)) • f x) volume
  dsimp [radialAngularMeasure]F:Typeinst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Fd:ℕf:Space d → F⊢ Integrable f (volume.withDensity fun x => ENNReal.ofReal (1 / ‖x‖ ^ (d - 1))) ↔
  Integrable (fun x => (1 / ‖x‖ ^ (d - 1)) • f x) volume
  erw [integrable_withDensity_iff_integrable_smul₀ (byF:Typeinst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Fd:ℕf:Space d → F⊢ AEMeasurable (fun x => (1 / ‖x‖ ^ (d - 1)).toNNReal) volume fun_propAll goals completed! 🐙)]F:Typeinst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Fd:ℕf:Space d → F⊢ Integrable (fun x => (1 / ‖x‖ ^ (d - 1)).toNNReal • f x) volume ↔ Integrable (fun x => (1 / ‖x‖ ^ (d - 1)) • f x) volume
  simp only [one_div]F:Typeinst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Fd:ℕf:Space d → F⊢ Integrable (fun x => (‖x‖ ^ (d - 1))⁻¹.toNNReal • f x) volume ↔ Integrable (fun x => (‖x‖ ^ (d - 1))⁻¹ • f x) volume
  refine integrable_congr ?_F:Typeinst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Fd:ℕf:Space d → F⊢ (fun x => (‖x‖ ^ (d - 1))⁻¹.toNNReal • f x) =ᵐ[volume] fun x => (‖x‖ ^ (d - 1))⁻¹ • f x
  filter_upwards with xF:Typeinst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Fd:ℕf:Space d → Fx:Space d⊢ (‖x‖ ^ (d - 1))⁻¹.toNNReal • f x = (‖x‖ ^ (d - 1))⁻¹ • f x
  rw [Real.toNNReal_of_nonneg (byF:Typeinst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Fd:ℕf:Space d → Fx:Space d⊢ 0 ≤ (‖x‖ ^ (d - 1))⁻¹All goals completed! 🐙 positivityAll goals completed! 🐙All goals completed! 🐙), NNReal.smul_def,F:Typeinst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Fd:ℕf:Space d → Fx:Space d⊢ ↑(NNReal.mk (‖x‖ ^ (d - 1))⁻¹ ⋯) • f x = (‖x‖ ^ (d - 1))⁻¹ • f xAll goals completed! 🐙 coe_mkF:Typeinst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Fd:ℕf:Space d → Fx:Space d⊢ (‖x‖ ^ (d - 1))⁻¹ • f x = (‖x‖ ^ (d - 1))⁻¹ • f xAll goals completed! 🐙]All goals completed! 🐙



omit [NormedSpace ℝ F] in
lemma integrable_radialAngularMeasure_of_spherical {d : ℕ} [NeZero d] (f : Space d → F)
    (hae : StronglyMeasurable f)
    (hf : Integrable (fun x => f (x.2.1 • x.1.1))
    (volume (α := Space d).toSphere.prod (Measure.volumeIoiPow 0))) :
    Integrable f radialAngularMeasure := byF:Typeinst✝¹:NormedAddCommGroup Fd:ℕinst✝:NeZero df:Space d → Fhae:StronglyMeasurable fhf:Integrable (fun x => f (↑x.2 • ↑x.1)) (volume.toSphere.prod (Measure.volumeIoiPow 0))⊢ Integrable f radialAngularMeasure
  refine ⟨StronglyMeasurable.aestronglyMeasurable hae, ?_⟩F:Typeinst✝¹:NormedAddCommGroup Fd:ℕinst✝:NeZero df:Space d → Fhae:StronglyMeasurable fhf:Integrable (fun x => f (↑x.2 • ↑x.1)) (volume.toSphere.prod (Measure.volumeIoiPow 0))⊢ HasFiniteIntegral f radialAngularMeasure
  rw [hasFiniteIntegral_iff_norm,F:Typeinst✝¹:NormedAddCommGroup Fd:ℕinst✝:NeZero df:Space d → Fhae:StronglyMeasurable fhf:Integrable (fun x => f (↑x.2 • ↑x.1)) (volume.toSphere.prod (Measure.volumeIoiPow 0))⊢ ∫⁻ (a : Space d), ENNReal.ofReal ‖f a‖ ∂radialAngularMeasure < ⊤F:Typeinst✝¹:NormedAddCommGroup Fd:ℕinst✝:NeZero df:Space d → Fhae:StronglyMeasurable fhf:Integrable (fun x => f (↑x.2 • ↑x.1)) (volume.toSphere.prod (Measure.volumeIoiPow 0))⊢ HasFiniteIntegral (fun x => f (↑x.2 • ↑x.1)) (volume.toSphere.prod (Measure.volumeIoiPow 0)) lintegral_radialMeasure_eq_spherical_mul _ _
    (byF:Typeinst✝¹:NormedAddCommGroup Fd:ℕinst✝:NeZero df:Space d → Fhae:StronglyMeasurable fhf:Integrable (fun x => f (↑x.2 • ↑x.1)) (volume.toSphere.prod (Measure.volumeIoiPow 0))⊢ Measurable fun a => ENNReal.ofReal ‖f a‖F:Typeinst✝¹:NormedAddCommGroup Fd:ℕinst✝:NeZero df:Space d → Fhae:StronglyMeasurable fhf:Integrable (fun x => f (↑x.2 • ↑x.1)) (volume.toSphere.prod (Measure.volumeIoiPow 0))⊢ HasFiniteIntegral (fun x => f (↑x.2 • ↑x.1)) (volume.toSphere.prod (Measure.volumeIoiPow 0)) simpa using StronglyMeasurable.enorm haeAll goals completed! 🐙F:Typeinst✝¹:NormedAddCommGroup Fd:ℕinst✝:NeZero df:Space d → Fhae:StronglyMeasurable fhf:Integrable (fun x => f (↑x.2 • ↑x.1)) (volume.toSphere.prod (Measure.volumeIoiPow 0))⊢ HasFiniteIntegral (fun x => f (↑x.2 • ↑x.1)) (volume.toSphere.prod (Measure.volumeIoiPow 0))), ← hasFiniteIntegral_iff_normF:Typeinst✝¹:NormedAddCommGroup Fd:ℕinst✝:NeZero df:Space d → Fhae:StronglyMeasurable fhf:Integrable (fun x => f (↑x.2 • ↑x.1)) (volume.toSphere.prod (Measure.volumeIoiPow 0))⊢ HasFiniteIntegral (fun x => f (↑x.2 • ↑x.1)) (volume.toSphere.prod (Measure.volumeIoiPow 0))F:Typeinst✝¹:NormedAddCommGroup Fd:ℕinst✝:NeZero df:Space d → Fhae:StronglyMeasurable fhf:Integrable (fun x => f (↑x.2 • ↑x.1)) (volume.toSphere.prod (Measure.volumeIoiPow 0))⊢ HasFiniteIntegral (fun x => f (↑x.2 • ↑x.1)) (volume.toSphere.prod (Measure.volumeIoiPow 0))]F:Typeinst✝¹:NormedAddCommGroup Fd:ℕinst✝:NeZero df:Space d → Fhae:StronglyMeasurable fhf:Integrable (fun x => f (↑x.2 • ↑x.1)) (volume.toSphere.prod (Measure.volumeIoiPow 0))⊢ HasFiniteIntegral (fun x => f (↑x.2 • ↑x.1)) (volume.toSphere.prod (Measure.volumeIoiPow 0))
  exact hf.2All goals completed! 🐙

E. HasTemperateGrowth of measures

E.1. Integrability of powers


private lemma integrable_neg_pow_on_ioi (n : ℕ) :
    IntegrableOn (fun x : ℝ => (|((1 : ℝ) + x) ^ (- (n + 2) : ℝ)|)) (Set.Ioi 0) := byn:ℕ⊢ IntegrableOn (fun x => |(1 + x) ^ (-(↑n + 2))|) (Set.Ioi 0) volume
  have hpre : (fun x : ℝ => (1 : ℝ) + x) ⁻¹' Set.Ioi 1 = Set.Ioi 0 := by
    ext xn:ℕx:ℝ⊢ x ∈ (fun x => 1 + x) ⁻¹' Set.Ioi 1 ↔ x ∈ Set.Ioi 0n:ℕhpre:(fun x => 1 + x) ⁻¹' Set.Ioi 1 = Set.Ioi 0⊢ IntegrableOn (fun x => |(1 + x) ^ (-(↑n + 2))|) (Set.Ioi 0) volume
    simpn:ℕhpre:(fun x => 1 + x) ⁻¹' Set.Ioi 1 = Set.Ioi 0⊢ IntegrableOn (fun x => |(1 + x) ^ (-(↑n + 2))|) (Set.Ioi 0) volumen:ℕhpre:(fun x => 1 + x) ⁻¹' Set.Ioi 1 = Set.Ioi 0⊢ IntegrableOn (fun x => |(1 + x) ^ (-(↑n + 2))|) (Set.Ioi 0) volume
  have integrableOn_rpow_neg :
      IntegrableOn (fun x : ℝ => ((1 : ℝ) + x) ^ (- (n + 2) : ℝ)) (Set.Ioi 0) := by
    rw [← hpren:ℕhpre:(fun x => 1 + x) ⁻¹' Set.Ioi 1 = Set.Ioi 0⊢ IntegrableOn (fun x => (1 + x) ^ (-(↑n + 2))) ((fun x => 1 + x) ⁻¹' Set.Ioi 1) volumen:ℕhpre:(fun x => 1 + x) ⁻¹' Set.Ioi 1 = Set.Ioi 0⊢ IntegrableOn (fun x => (1 + x) ^ (-(↑n + 2))) ((fun x => 1 + x) ⁻¹' Set.Ioi 1) volumen:ℕhpre:(fun x => 1 + x) ⁻¹' Set.Ioi 1 = Set.Ioi 0integrableOn_rpow_neg:IntegrableOn (fun x => (1 + x) ^ (-(↑n + 2))) (Set.Ioi 0) volume⊢ IntegrableOn (fun x => |(1 + x) ^ (-(↑n + 2))|) (Set.Ioi 0) volume]n:ℕhpre:(fun x => 1 + x) ⁻¹' Set.Ioi 1 = Set.Ioi 0⊢ IntegrableOn (fun x => (1 + x) ^ (-(↑n + 2))) ((fun x => 1 + x) ⁻¹' Set.Ioi 1) volumen:ℕhpre:(fun x => 1 + x) ⁻¹' Set.Ioi 1 = Set.Ioi 0integrableOn_rpow_neg:IntegrableOn (fun x => (1 + x) ^ (-(↑n + 2))) (Set.Ioi 0) volume⊢ IntegrableOn (fun x => |(1 + x) ^ (-(↑n + 2))|) (Set.Ioi 0) volume
    exact ((measurePreserving_add_left volume (1 : ℝ)).integrableOn_comp_preimage
      (measurableEmbedding_addLeft 1)
      (f := fun y : ℝ => y ^ (- (n + 2) : ℝ)) (s := Set.Ioi 1)).mpr
      (integrableOn_Ioi_rpow_of_lt (byn:ℕhpre:(fun x => 1 + x) ⁻¹' Set.Ioi 1 = Set.Ioi 0⊢ -(↑n + 2) < -1n:ℕhpre:(fun x => 1 + x) ⁻¹' Set.Ioi 1 = Set.Ioi 0integrableOn_rpow_neg:IntegrableOn (fun x => (1 + x) ^ (-(↑n + 2))) (Set.Ioi 0) volume⊢ IntegrableOn (fun x => |(1 + x) ^ (-(↑n + 2))|) (Set.Ioi 0) volume linarith [Nat.cast_nonneg (α := ℝ) n]All goals completed! 🐙n:ℕhpre:(fun x => 1 + x) ⁻¹' Set.Ioi 1 = Set.Ioi 0integrableOn_rpow_neg:IntegrableOn (fun x => (1 + x) ^ (-(↑n + 2))) (Set.Ioi 0) volume⊢ IntegrableOn (fun x => |(1 + x) ^ (-(↑n + 2))|) (Set.Ioi 0) volume) one_pos)n:ℕhpre:(fun x => 1 + x) ⁻¹' Set.Ioi 1 = Set.Ioi 0integrableOn_rpow_neg:IntegrableOn (fun x => (1 + x) ^ (-(↑n + 2))) (Set.Ioi 0) volume⊢ IntegrableOn (fun x => |(1 + x) ^ (-(↑n + 2))|) (Set.Ioi 0) volume
  refine integrableOn_rpow_neg.congr_fun (fun x hx => ?_) measurableSet_Ioin:ℕhpre:(fun x => 1 + x) ⁻¹' Set.Ioi 1 = Set.Ioi 0integrableOn_rpow_neg:IntegrableOn (fun x => (1 + x) ^ (-(↑n + 2))) (Set.Ioi 0) volumex:ℝhx:x ∈ Set.Ioi 0⊢ (fun x => (1 + x) ^ (-(↑n + 2))) x = |(1 + x) ^ (-(↑n + 2))|
  rw [Set.mem_Ioin:ℕhpre:(fun x => 1 + x) ⁻¹' Set.Ioi 1 = Set.Ioi 0integrableOn_rpow_neg:IntegrableOn (fun x => (1 + x) ^ (-(↑n + 2))) (Set.Ioi 0) volumex:ℝhx:0 < x⊢ (fun x => (1 + x) ^ (-(↑n + 2))) x = |(1 + x) ^ (-(↑n + 2))|n:ℕhpre:(fun x => 1 + x) ⁻¹' Set.Ioi 1 = Set.Ioi 0integrableOn_rpow_neg:IntegrableOn (fun x => (1 + x) ^ (-(↑n + 2))) (Set.Ioi 0) volumex:ℝhx:0 < x⊢ (fun x => (1 + x) ^ (-(↑n + 2))) x = |(1 + x) ^ (-(↑n + 2))|] at hxn:ℕhpre:(fun x => 1 + x) ⁻¹' Set.Ioi 1 = Set.Ioi 0integrableOn_rpow_neg:IntegrableOn (fun x => (1 + x) ^ (-(↑n + 2))) (Set.Ioi 0) volumex:ℝhx:0 < x⊢ (fun x => (1 + x) ^ (-(↑n + 2))) x = |(1 + x) ^ (-(↑n + 2))|
  rw [abs_of_nonneg (Real.rpow_nonneg (byn:ℕhpre:(fun x => 1 + x) ⁻¹' Set.Ioi 1 = Set.Ioi 0integrableOn_rpow_neg:IntegrableOn (fun x => (1 + x) ^ (-(↑n + 2))) (Set.Ioi 0) volumex:ℝhx:0 < x⊢ 0 ≤ 1 + xAll goals completed! 🐙 linarithAll goals completed! 🐙All goals completed! 🐙) _)]All goals completed! 🐙



lemma radialAngularMeasure_integrable_pow_neg_two {d : ℕ} :
    Integrable (fun x : Space d => (1 + ‖x‖) ^ (- (d + 1) : ℝ))
      radialAngularMeasure := byd:ℕ⊢ Integrable (fun x => (1 + ‖x‖) ^ (-(↑d + 1))) radialAngularMeasure
  match d with
  | 0 =>d:ℕ⊢ Integrable (fun x => (1 + ‖x‖) ^ (-(↑0 + 1))) radialAngularMeasure simpAll goals completed! 🐙
  | dm1 + 1 =>d:ℕdm1:ℕ⊢ Integrable (fun x => (1 + ‖x‖) ^ (-(↑(dm1 + 1) + 1))) radialAngularMeasure
  apply integrable_radialAngularMeasure_of_spherical _ (byd:ℕdm1:ℕ⊢ StronglyMeasurable fun x => (1 + ‖x‖) ^ (-(↑(dm1 + 1) + 1)) fun_propAll goals completed! 🐙)
  simp [norm_smul]d:ℕdm1:ℕ⊢ Integrable (fun x => (1 + |↑x.2|) ^ (-1 + (-1 + -↑dm1))) (volume.toSphere.prod (Measure.volumeIoiPow 0))
  rw [MeasureTheory.integrable_prod_iff (AEMeasurable.aestronglyMeasurable (byd:ℕdm1:ℕ⊢ AEMeasurable (fun x => (1 + |↑x.2|) ^ (-1 + (-1 + -↑dm1))) (volume.toSphere.prod (Measure.volumeIoiPow 0))d:ℕdm1:ℕ⊢ (∀ᵐ (x : ↑(Metric.sphere 0 1)) ∂volume.toSphere,
    Integrable (fun y => (1 + |↑(x, y).2|) ^ (-1 + (-1 + -↑dm1))) (Measure.volumeIoiPow 0)) ∧
  Integrable (fun x => ∫ (y : ↑(Set.Ioi 0)), ‖(1 + |↑(x, y).2|) ^ (-1 + (-1 + -↑dm1))‖ ∂Measure.volumeIoiPow 0)
    volume.toSphere fun_propAll goals completed! 🐙d:ℕdm1:ℕ⊢ (∀ᵐ (x : ↑(Metric.sphere 0 1)) ∂volume.toSphere,
    Integrable (fun y => (1 + |↑(x, y).2|) ^ (-1 + (-1 + -↑dm1))) (Measure.volumeIoiPow 0)) ∧
  Integrable (fun x => ∫ (y : ↑(Set.Ioi 0)), ‖(1 + |↑(x, y).2|) ^ (-1 + (-1 + -↑dm1))‖ ∂Measure.volumeIoiPow 0)
    volume.toSphere))]d:ℕdm1:ℕ⊢ (∀ᵐ (x : ↑(Metric.sphere 0 1)) ∂volume.toSphere,
    Integrable (fun y => (1 + |↑(x, y).2|) ^ (-1 + (-1 + -↑dm1))) (Measure.volumeIoiPow 0)) ∧
  Integrable (fun x => ∫ (y : ↑(Set.Ioi 0)), ‖(1 + |↑(x, y).2|) ^ (-1 + (-1 + -↑dm1))‖ ∂Measure.volumeIoiPow 0)
    volume.toSphere
  refine ⟨?_, byd:ℕdm1:ℕ⊢ Integrable (fun x => ∫ (y : ↑(Set.Ioi 0)), ‖(1 + |↑(x, y).2|) ^ (-1 + (-1 + -↑dm1))‖ ∂Measure.volumeIoiPow 0)
  volume.toSphere simpAll goals completed! 🐙⟩
  filter_upwards with xd:ℕdm1:ℕx:↑(Metric.sphere 0 1)⊢ Integrable (fun y => (1 + |↑y|) ^ (-1 + (-1 + -↑dm1))) (Measure.volumeIoiPow 0)
  simp [Measure.volumeIoiPow]d:ℕdm1:ℕx:↑(Metric.sphere 0 1)⊢ Integrable (fun y => (1 + |↑y|) ^ (-1 + (-1 + -↑dm1))) (Measure.comap Subtype.val volume)
  refine ((MeasureTheory.integrableOn_iff_comap_subtypeVal measurableSet_Ioi).mp
    (integrable_neg_pow_on_ioi dm1)).congr ?_d:ℕdm1:ℕx:↑(Metric.sphere 0 1)⊢ (fun x => |(1 + x) ^ (-(↑dm1 + 2))|) ∘ Subtype.val =ᵐ[Measure.comap Subtype.val volume] fun y =>
  (1 + |↑y|) ^ (-1 + (-1 + -↑dm1))
  filter_upwards with yd:ℕdm1:ℕx:↑(Metric.sphere 0 1)y:↑(Set.Ioi 0)⊢ ((fun x => |(1 + x) ^ (-(↑dm1 + 2))|) ∘ Subtype.val) y = (1 + |↑y|) ^ (-1 + (-1 + -↑dm1))
  have hy : (0 : ℝ) < y.1 := y.2d:ℕdm1:ℕx:↑(Metric.sphere 0 1)y:↑(Set.Ioi 0)hy:0 < ↑y⊢ ((fun x => |(1 + x) ^ (-(↑dm1 + 2))|) ∘ Subtype.val) y = (1 + |↑y|) ^ (-1 + (-1 + -↑dm1))
  simp only [Function.comp_apply]d:ℕdm1:ℕx:↑(Metric.sphere 0 1)y:↑(Set.Ioi 0)hy:0 < ↑y⊢ |(1 + ↑y) ^ (-(↑dm1 + 2))| = (1 + |↑y|) ^ (-1 + (-1 + -↑dm1))
  rw [abs_of_pos hy,d:ℕdm1:ℕx:↑(Metric.sphere 0 1)y:↑(Set.Ioi 0)hy:0 < ↑y⊢ |(1 + ↑y) ^ (-(↑dm1 + 2))| = (1 + ↑y) ^ (-1 + (-1 + -↑dm1))d:ℕdm1:ℕx:↑(Metric.sphere 0 1)y:↑(Set.Ioi 0)hy:0 < ↑y⊢ (1 + ↑y) ^ (-(↑dm1 + 2)) = (1 + ↑y) ^ (-1 + (-1 + -↑dm1)) abs_of_nonneg (Real.rpow_nonneg (byd:ℕdm1:ℕx:↑(Metric.sphere 0 1)y:↑(Set.Ioi 0)hy:0 < ↑y⊢ 0 ≤ 1 + ↑yd:ℕdm1:ℕx:↑(Metric.sphere 0 1)y:↑(Set.Ioi 0)hy:0 < ↑y⊢ (1 + ↑y) ^ (-(↑dm1 + 2)) = (1 + ↑y) ^ (-1 + (-1 + -↑dm1)) linarithAll goals completed! 🐙d:ℕdm1:ℕx:↑(Metric.sphere 0 1)y:↑(Set.Ioi 0)hy:0 < ↑y⊢ (1 + ↑y) ^ (-(↑dm1 + 2)) = (1 + ↑y) ^ (-1 + (-1 + -↑dm1))) _)]d:ℕdm1:ℕx:↑(Metric.sphere 0 1)y:↑(Set.Ioi 0)hy:0 < ↑y⊢ (1 + ↑y) ^ (-(↑dm1 + 2)) = (1 + ↑y) ^ (-1 + (-1 + -↑dm1))
  congr 1e_ad:ℕdm1:ℕx:↑(Metric.sphere 0 1)y:↑(Set.Ioi 0)hy:0 < ↑y⊢ -(↑dm1 + 2) = -1 + (-1 + -↑dm1)
  ringAll goals completed! 🐙

E.2. radialAngularMeasure has temperate growth

instance (d : ℕ) : Measure.HasTemperateGrowth (radialAngularMeasure (d := d)) where
  exists_integrable := by𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ Fd:ℕ⊢ ∃ n, Integrable (fun x => (1 + ‖x‖) ^ (-↑n)) radialAngularMeasure
    use d + 1h𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ Fd:ℕ⊢ Integrable (fun x => (1 + ‖x‖) ^ (-↑(d + 1))) radialAngularMeasure
    simpa using radialAngularMeasure_integrable_pow_neg_two (d := d)All goals completed! 🐙