Physlib.SpaceAndTime.Space.Integrals.Basic

Imports

/-
Copyright (c) 2026 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.Module
public import Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls

Integrals in Space

i. Overview

In this module we give general properties of integrals over Space d. We focus here on the volume measure, which is the usual measure on Space d, i.e. dx dy dz.

ii. Key results

volume_eq_addHaar : The volume measure on Space d is the same as the Haar measure associated with the basis of Space d.

integral_volume_eq_spherical : The integral of a function over Space d with respect to the volume measure can be expressed as an integral over the unit sphere and the positive reals.

lintegral_volume_eq_spherical : The lower Lebesgue integral of a function over Space d with respect to the volume measure can be expressed as a lower Lebesgue integral over the unit sphere and the positive reals.

@[expose] public section

A. Properties of the volume measure

              lemma volume_eq_addHaar {d} : (volume (α := Space d)) = Space.basis.toBasis.addHaar := byd:ℕ⊢ volume = basis.toBasis.addHaar
  exact (OrthonormalBasis.addHaar_eq_volume _).symmAll goals completed! 🐙

@[simp]
lemma volume_metricBall_three :
    volume (Metric.ball (0 : Space 3) 1) = ENNReal.ofReal (4 / 3 * Real.pi) := by⊢ volume (Metric.ball 0 1) = ENNReal.ofReal (4 / 3 * Real.pi)
  rw [InnerProductSpace.volume_ball_of_dim_odd (k := 1)⊢ ENNReal.ofReal 1 ^ Module.finrank ℝ Space *
    ENNReal.ofReal (Real.pi ^ 1 * 2 ^ (1 + 1) / ↑(Module.finrank ℝ Space).doubleFactorial) =
  ENNReal.ofReal (4 / 3 * Real.pi)hk⊢ Module.finrank ℝ Space = 2 * 1 + 1⊢ ENNReal.ofReal 1 ^ Module.finrank ℝ Space *
    ENNReal.ofReal (Real.pi ^ 1 * 2 ^ (1 + 1) / ↑(Module.finrank ℝ Space).doubleFactorial) =
  ENNReal.ofReal (4 / 3 * Real.pi)hk⊢ Module.finrank ℝ Space = 2 * 1 + 1]⊢ ENNReal.ofReal 1 ^ Module.finrank ℝ Space *
    ENNReal.ofReal (Real.pi ^ 1 * 2 ^ (1 + 1) / ↑(Module.finrank ℝ Space).doubleFactorial) =
  ENNReal.ofReal (4 / 3 * Real.pi)hk⊢ Module.finrank ℝ Space = 2 * 1 + 1
  simp only [ENNReal.ofReal_one, finrank_eq_dim, one_pow, pow_one, Nat.reduceAdd,
    Nat.doubleFactorial.eq_3, Nat.doubleFactorial, mul_one, Nat.cast_ofNat, one_mul]⊢ ENNReal.ofReal (Real.pi * 2 ^ 2 / 3) = ENNReal.ofReal (4 / 3 * Real.pi)hk⊢ Module.finrank ℝ Space = 2 * 1 + 1
  ring_nfhk⊢ Module.finrank ℝ Space = 2 * 1 + 1
  simpAll goals completed! 🐙

@[simp]
lemma volume_metricBall_two :
    volume (Metric.ball (0 : Space 2) 1) = ENNReal.ofReal Real.pi := by⊢ volume (Metric.ball 0 1) = ENNReal.ofReal Real.pi
  rw [InnerProductSpace.volume_ball_of_dim_even (k := 1)⊢ ENNReal.ofReal 1 ^ Module.finrank ℝ (Space 2) * ENNReal.ofReal (Real.pi ^ 1 / ↑(Nat.factorial 1)) =
  ENNReal.ofReal Real.pihk⊢ Module.finrank ℝ (Space 2) = 2 * 1⊢ ENNReal.ofReal 1 ^ Module.finrank ℝ (Space 2) * ENNReal.ofReal (Real.pi ^ 1 / ↑(Nat.factorial 1)) =
  ENNReal.ofReal Real.pihk⊢ Module.finrank ℝ (Space 2) = 2 * 1]⊢ ENNReal.ofReal 1 ^ Module.finrank ℝ (Space 2) * ENNReal.ofReal (Real.pi ^ 1 / ↑(Nat.factorial 1)) =
  ENNReal.ofReal Real.pihk⊢ Module.finrank ℝ (Space 2) = 2 * 1
  simp [finrank_eq_dim]hk⊢ Module.finrank ℝ (Space 2) = 2 * 1
  simp [finrank_eq_dim]All goals completed! 🐙

@[simp]
lemma volume_metricBall_two_real :
    (volume.real (Metric.ball (0 : Space 2) 1)) = Real.pi := by⊢ volume.real (Metric.ball 0 1) = Real.pi
  trans (volume (Metric.ball (0 : Space 2) 1)).toReal⊢ volume.real (Metric.ball 0 1) = (volume (Metric.ball 0 1)).toReal⊢ (volume (Metric.ball 0 1)).toReal = Real.pi
  ·⊢ volume.real (Metric.ball 0 1) = (volume (Metric.ball 0 1)).toReal rflAll goals completed! 🐙
  rw [volume_metricBall_two⊢ (ENNReal.ofReal Real.pi).toReal = Real.pi⊢ (ENNReal.ofReal Real.pi).toReal = Real.pi]⊢ (ENNReal.ofReal Real.pi).toReal = Real.pi
  simp only [ENNReal.toReal_ofReal_eq_iff]⊢ 0 ≤ Real.pi
  exact Real.pi_nonnegAll goals completed! 🐙

@[simp]
lemma volume_metricBall_three_real :
    (volume.real (Metric.ball (0 : Space 3) 1)) = 4 / 3 * Real.pi := by⊢ volume.real (Metric.ball 0 1) = 4 / 3 * Real.pi
  trans (volume (Metric.ball (0 : Space 3) 1)).toReal⊢ volume.real (Metric.ball 0 1) = (volume (Metric.ball 0 1)).toReal⊢ (volume (Metric.ball 0 1)).toReal = 4 / 3 * Real.pi
  ·⊢ volume.real (Metric.ball 0 1) = (volume (Metric.ball 0 1)).toReal rflAll goals completed! 🐙
  rw [volume_metricBall_three⊢ (ENNReal.ofReal (4 / 3 * Real.pi)).toReal = 4 / 3 * Real.pi⊢ (ENNReal.ofReal (4 / 3 * Real.pi)).toReal = 4 / 3 * Real.pi]⊢ (ENNReal.ofReal (4 / 3 * Real.pi)).toReal = 4 / 3 * Real.pi
  simp only [ENNReal.toReal_ofReal_eq_iff]⊢ 0 ≤ 4 / 3 * Real.pi
  positivityAll goals completed! 🐙

B. Integrals over one-dimensional space



lemma integral_one_dim_eq_integral_real {f : Space 1 → ℝ} :
    ∫ x, f x ∂volume = ∫ x, f (oneEquiv.symm x) ∂volume := byf:Space 1 → ℝ⊢ ∫ (x : Space 1), f x = ∫ (x : ℝ), f (oneEquiv.symm x) rw [integral_compf:Space 1 → ℝ⊢ ∫ (x : Space 1), f x = ∫ (y : Space 1), f yAll goals completed! 🐙]All goals completed! 🐙

C. Integrals over volume to spherical

              

lemma integral_volume_eq_spherical (d : ℕ) [NeZero d] (f : Space d → F)
    [NormedAddCommGroup F] [NormedSpace ℝ F] :
    ∫ x, f x ∂volume = ∫ x, f (x.2.1 • x.1.1) ∂(volume (α := Space d).toSphere.prod
        (Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1))) := byF:Type u_1d:ℕinst✝²:NeZero df:Space d → Finst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ F⊢ ∫ (x : Space d), f x =
  ∫ (x : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)),
    f (↑x.2 • ↑x.1) ∂volume.toSphere.prod (Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1))
  rw [← MeasureTheory.MeasurePreserving.integral_comp (f := homeomorphUnitSphereProd _)
    (MeasureTheory.Measure.measurePreserving_homeomorphUnitSphereProd
    (volume (α := Space d)))
    (Homeomorph.measurableEmbedding (homeomorphUnitSphereProd (Space d)))F:Type u_1d:ℕinst✝²:NeZero df:Space d → Finst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ F⊢ ∫ (x : Space d), f x =
  ∫ (x : ↑{0}ᶜ),
    f
      (↑((homeomorphUnitSphereProd (Space d)) x).2 •
        ↑((homeomorphUnitSphereProd (Space d)) x).1) ∂Measure.comap Subtype.val volumeF:Type u_1d:ℕinst✝²:NeZero df:Space d → Finst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ F⊢ ∫ (x : Space d), f x =
  ∫ (x : ↑{0}ᶜ),
    f
      (↑((homeomorphUnitSphereProd (Space d)) x).2 •
        ↑((homeomorphUnitSphereProd (Space d)) x).1) ∂Measure.comap Subtype.val volume]F:Type u_1d:ℕinst✝²:NeZero df:Space d → Finst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ F⊢ ∫ (x : Space d), f x =
  ∫ (x : ↑{0}ᶜ),
    f
      (↑((homeomorphUnitSphereProd (Space d)) x).2 •
        ↑((homeomorphUnitSphereProd (Space d)) x).1) ∂Measure.comap Subtype.val volume
  simp only [homeomorphUnitSphereProd_apply_snd_coe, homeomorphUnitSphereProd_apply_fst_coe]F:Type u_1d:ℕinst✝²:NeZero df:Space d → Finst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ F⊢ ∫ (x : Space d), f x = ∫ (x : ↑{0}ᶜ), f (‖↑x‖ • ‖↑x‖⁻¹ • ↑x) ∂Measure.comap Subtype.val volume
  let f' : (x : (Space d)) → F := fun x => f (‖↑x‖ • ‖↑x‖⁻¹ • ↑x)F:Type u_1d:ℕinst✝²:NeZero df:Space d → Finst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Ff':Space d → F := fun x => f (‖x‖ • ‖x‖⁻¹ • x)⊢ ∫ (x : Space d), f x = ∫ (x : ↑{0}ᶜ), f (‖↑x‖ • ‖↑x‖⁻¹ • ↑x) ∂Measure.comap Subtype.val volume
  conv_rhs =>
    enter [2, x]F:Type u_1d:ℕinst✝²:NeZero df:Space d → Finst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Ff':Space d → F := fun x => f (‖x‖ • ‖x‖⁻¹ • x)x:↑{0}ᶜ| f (‖↑x‖ • ‖↑x‖⁻¹ • ↑x)
    change f' x.1F:Type u_1d:ℕinst✝²:NeZero df:Space d → Finst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Ff':Space d → F := fun x => f (‖x‖ • ‖x‖⁻¹ • x)x:↑{0}ᶜ| f' ↑x
  rw [MeasureTheory.integral_subtype_comap (byF:Type u_1d:ℕinst✝²:NeZero df:Space d → Finst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Ff':Space d → F := fun x => f (‖x‖ • ‖x‖⁻¹ • x)⊢ MeasurableSet {0}ᶜF:Type u_1d:ℕinst✝²:NeZero df:Space d → Finst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Ff':Space d → F := fun x => f (‖x‖ • ‖x‖⁻¹ • x)⊢ ∫ (x : Space d) in Set.univ, f x = ∫ (x : Space d) in {0}ᶜ, f' x simpAll goals completed! 🐙F:Type u_1d:ℕinst✝²:NeZero df:Space d → Finst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Ff':Space d → F := fun x => f (‖x‖ • ‖x‖⁻¹ • x)⊢ ∫ (x : Space d) in Set.univ, f x = ∫ (x : Space d) in {0}ᶜ, f' x), ← setIntegral_univF:Type u_1d:ℕinst✝²:NeZero df:Space d → Finst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Ff':Space d → F := fun x => f (‖x‖ • ‖x‖⁻¹ • x)⊢ ∫ (x : Space d) in Set.univ, f x = ∫ (x : Space d) in {0}ᶜ, f' xF:Type u_1d:ℕinst✝²:NeZero df:Space d → Finst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Ff':Space d → F := fun x => f (‖x‖ • ‖x‖⁻¹ • x)⊢ ∫ (x : Space d) in Set.univ, f x = ∫ (x : Space d) in {0}ᶜ, f' x]F:Type u_1d:ℕinst✝²:NeZero df:Space d → Finst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Ff':Space d → F := fun x => f (‖x‖ • ‖x‖⁻¹ • x)⊢ ∫ (x : Space d) in Set.univ, f x = ∫ (x : Space d) in {0}ᶜ, f' x
  simp [f']F:Type u_1d:ℕinst✝²:NeZero df:Space d → Finst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Ff':Space d → F := fun x => f (‖x‖ • ‖x‖⁻¹ • x)⊢ ∫ (x : Space d), f x = ∫ (x : Space d), f (‖x‖ • ‖x‖⁻¹ • x)
  refine integral_congr_ae ?_F:Type u_1d:ℕinst✝²:NeZero df:Space d → Finst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Ff':Space d → F := fun x => f (‖x‖ • ‖x‖⁻¹ • x)⊢ f =ᵐ[volume] fun x => f (‖x‖ • ‖x‖⁻¹ • x)
  have h1 : ∀ᵐ x ∂(volume (α := Space d)), x ≠ 0 := byF:Type u_1d:ℕinst✝²:NeZero df:Space d → Finst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ F⊢ ∫ (x : Space d), f x =
  ∫ (x : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)),
    f (↑x.2 • ↑x.1) ∂volume.toSphere.prod (Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1))F:Type u_1d:ℕinst✝²:NeZero df:Space d → Finst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Ff':Space d → F := fun x => f (‖x‖ • ‖x‖⁻¹ • x)h1:∀ᵐ (x : Space d), x ≠ 0⊢ f =ᵐ[volume] fun x => f (‖x‖ • ‖x‖⁻¹ • x)
    exact Measure.ae_ne volume 0F:Type u_1d:ℕinst✝²:NeZero df:Space d → Finst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Ff':Space d → F := fun x => f (‖x‖ • ‖x‖⁻¹ • x)h1:∀ᵐ (x : Space d), x ≠ 0⊢ f =ᵐ[volume] fun x => f (‖x‖ • ‖x‖⁻¹ • x)F:Type u_1d:ℕinst✝²:NeZero df:Space d → Finst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Ff':Space d → F := fun x => f (‖x‖ • ‖x‖⁻¹ • x)h1:∀ᵐ (x : Space d), x ≠ 0⊢ f =ᵐ[volume] fun x => f (‖x‖ • ‖x‖⁻¹ • x)
  filter_upwards [Measure.ae_ne volume 0] with x hxF:Type u_1d:ℕinst✝²:NeZero df:Space d → Finst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Ff':Space d → F := fun x => f (‖x‖ • ‖x‖⁻¹ • x)h1:∀ᵐ (x : Space d), x ≠ 0x:Space dhx:x ≠ 0⊢ f x = f (‖x‖ • ‖x‖⁻¹ • x)
  congrF:Type u_1d:ℕinst✝²:NeZero df:Space d → Finst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Ff':Space d → F := fun x => f (‖x‖ • ‖x‖⁻¹ • x)h1:∀ᵐ (x : Space d), x ≠ 0x:Space dhx:x ≠ 0⊢ x = ‖x‖ • ‖x‖⁻¹ • x
  simp [smul_smul]F:Type u_1d:ℕinst✝²:NeZero df:Space d → Finst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Ff':Space d → F := fun x => f (‖x‖ • ‖x‖⁻¹ • x)h1:∀ᵐ (x : Space d), x ≠ 0x:Space dhx:x ≠ 0⊢ x = (‖x‖ * ‖x‖⁻¹) • x
  have hx : ‖x‖ ≠ 0 := byF:Type u_1d:ℕinst✝²:NeZero df:Space d → Finst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ F⊢ ∫ (x : Space d), f x =
  ∫ (x : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)),
    f (↑x.2 • ↑x.1) ∂volume.toSphere.prod (Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1))F:Type u_1d:ℕinst✝²:NeZero df:Space d → Finst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Ff':Space d → F := fun x => f (‖x‖ • ‖x‖⁻¹ • x)h1:∀ᵐ (x : Space d), x ≠ 0x:Space dhx✝:x ≠ 0hx:‖x‖ ≠ 0⊢ x = (‖x‖ * ‖x‖⁻¹) • x
    simpa using hxF:Type u_1d:ℕinst✝²:NeZero df:Space d → Finst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Ff':Space d → F := fun x => f (‖x‖ • ‖x‖⁻¹ • x)h1:∀ᵐ (x : Space d), x ≠ 0x:Space dhx✝:x ≠ 0hx:‖x‖ ≠ 0⊢ x = (‖x‖ * ‖x‖⁻¹) • xF:Type u_1d:ℕinst✝²:NeZero df:Space d → Finst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Ff':Space d → F := fun x => f (‖x‖ • ‖x‖⁻¹ • x)h1:∀ᵐ (x : Space d), x ≠ 0x:Space dhx✝:x ≠ 0hx:‖x‖ ≠ 0⊢ x = (‖x‖ * ‖x‖⁻¹) • x
  field_simpF:Type u_1d:ℕinst✝²:NeZero df:Space d → Finst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Ff':Space d → F := fun x => f (‖x‖ • ‖x‖⁻¹ • x)h1:∀ᵐ (x : Space d), x ≠ 0x:Space dhx✝:x ≠ 0hx:‖x‖ ≠ 0⊢ x = 1 • x
  simpAll goals completed! 🐙

-- `unusedArguments` (newly flagged under v4.32.0): `NormedSpace ℝ F` is required
-- to state the goal but is not referenced in the proof term.
@[nolint unusedArguments]
lemma integrable_spherical_of_integrable {d : ℕ} {F : Type*}
    [NormedAddCommGroup F] [NormedSpace ℝ F] {f : Space d → F}
    (hf : Integrable f volume) :
    Integrable
      (fun x : ↑(Metric.sphere (0 : Space d) 1) × Set.Ioi (0 : ℝ) =>
        f (x.2.1 • x.1.1))
      (volume (α := Space d).toSphere.prod
        (Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1))) := byd:ℕF:Type u_1inst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Ff:Space d → Fhf:Integrable f volume⊢ Integrable (fun x => f (↑x.2 • ↑x.1)) (volume.toSphere.prod (Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1)))
  let s : Set (Space d) := {0}ᶜd:ℕF:Type u_1inst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Ff:Space d → Fhf:Integrable f volumes:Set (Space d) := {0}ᶜ⊢ Integrable (fun x => f (↑x.2 • ↑x.1)) (volume.toSphere.prod (Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1)))
  have h1 : Integrable (fun x : s => f x.1)
      (.comap (Subtype.val (p := fun x => x ∈ s)) volume) := by
    change Integrable (f ∘ Subtype.val)
      (.comap (Subtype.val (p := fun x => x ∈ s)) volume)d:ℕF:Type u_1inst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Ff:Space d → Fhf:Integrable f volumes:Set (Space d) := {0}ᶜ⊢ Integrable (f ∘ Subtype.val) (Measure.comap Subtype.val volume)d:ℕF:Type u_1inst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Ff:Space d → Fhf:Integrable f volumes:Set (Space d) := {0}ᶜh1:Integrable (fun x => f ↑x) (Measure.comap Subtype.val volume)⊢ Integrable (fun x => f (↑x.2 • ↑x.1)) (volume.toSphere.prod (Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1)))
    rw [← MeasureTheory.integrableOn_iff_comap_subtypeVald:ℕF:Type u_1inst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Ff:Space d → Fhf:Integrable f volumes:Set (Space d) := {0}ᶜ⊢ IntegrableOn f s volumed:ℕF:Type u_1inst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Ff:Space d → Fhf:Integrable f volumes:Set (Space d) := {0}ᶜ⊢ MeasurableSet sd:ℕF:Type u_1inst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Ff:Space d → Fhf:Integrable f volumes:Set (Space d) := {0}ᶜ⊢ IntegrableOn f s volumed:ℕF:Type u_1inst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Ff:Space d → Fhf:Integrable f volumes:Set (Space d) := {0}ᶜ⊢ MeasurableSet sd:ℕF:Type u_1inst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Ff:Space d → Fhf:Integrable f volumes:Set (Space d) := {0}ᶜh1:Integrable (fun x => f ↑x) (Measure.comap Subtype.val volume)⊢ Integrable (fun x => f (↑x.2 • ↑x.1)) (volume.toSphere.prod (Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1)))]d:ℕF:Type u_1inst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Ff:Space d → Fhf:Integrable f volumes:Set (Space d) := {0}ᶜ⊢ IntegrableOn f s volumed:ℕF:Type u_1inst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Ff:Space d → Fhf:Integrable f volumes:Set (Space d) := {0}ᶜ⊢ MeasurableSet sd:ℕF:Type u_1inst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Ff:Space d → Fhf:Integrable f volumes:Set (Space d) := {0}ᶜh1:Integrable (fun x => f ↑x) (Measure.comap Subtype.val volume)⊢ Integrable (fun x => f (↑x.2 • ↑x.1)) (volume.toSphere.prod (Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1)))
    ·d:ℕF:Type u_1inst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Ff:Space d → Fhf:Integrable f volumes:Set (Space d) := {0}ᶜ⊢ IntegrableOn f s volumed:ℕF:Type u_1inst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Ff:Space d → Fhf:Integrable f volumes:Set (Space d) := {0}ᶜh1:Integrable (fun x => f ↑x) (Measure.comap Subtype.val volume)⊢ Integrable (fun x => f (↑x.2 • ↑x.1)) (volume.toSphere.prod (Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1))) exact hf.integrableOnAll goals completed! 🐙d:ℕF:Type u_1inst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Ff:Space d → Fhf:Integrable f volumes:Set (Space d) := {0}ᶜh1:Integrable (fun x => f ↑x) (Measure.comap Subtype.val volume)⊢ Integrable (fun x => f (↑x.2 • ↑x.1)) (volume.toSphere.prod (Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1)))
    ·d:ℕF:Type u_1inst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Ff:Space d → Fhf:Integrable f volumes:Set (Space d) := {0}ᶜ⊢ MeasurableSet sd:ℕF:Type u_1inst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Ff:Space d → Fhf:Integrable f volumes:Set (Space d) := {0}ᶜh1:Integrable (fun x => f ↑x) (Measure.comap Subtype.val volume)⊢ Integrable (fun x => f (↑x.2 • ↑x.1)) (volume.toSphere.prod (Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1))) simp [s]d:ℕF:Type u_1inst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Ff:Space d → Fhf:Integrable f volumes:Set (Space d) := {0}ᶜh1:Integrable (fun x => f ↑x) (Measure.comap Subtype.val volume)⊢ Integrable (fun x => f (↑x.2 • ↑x.1)) (volume.toSphere.prod (Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1)))d:ℕF:Type u_1inst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Ff:Space d → Fhf:Integrable f volumes:Set (Space d) := {0}ᶜh1:Integrable (fun x => f ↑x) (Measure.comap Subtype.val volume)⊢ Integrable (fun x => f (↑x.2 • ↑x.1)) (volume.toSphere.prod (Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1)))
  have he := MeasureTheory.Measure.measurePreserving_homeomorphUnitSphereProd
    (volume (α := Space d))d:ℕF:Type u_1inst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Ff:Space d → Fhf:Integrable f volumes:Set (Space d) := {0}ᶜh1:Integrable (fun x => f ↑x) (Measure.comap Subtype.val volume)he:MeasurePreserving (⇑(homeomorphUnitSphereProd (Space d))) (Measure.comap Subtype.val volume)
  (volume.toSphere.prod (Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1)))⊢ Integrable (fun x => f (↑x.2 • ↑x.1)) (volume.toSphere.prod (Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1)))
  have hcomp :
      Integrable
        ((fun x : s => f x.1) ∘ (homeomorphUnitSphereProd (Space d)).symm)
        (volume (α := Space d).toSphere.prod
          (Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1))) := by
    rw [← he.integrable_comp_embd:ℕF:Type u_1inst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Ff:Space d → Fhf:Integrable f volumes:Set (Space d) := {0}ᶜh1:Integrable (fun x => f ↑x) (Measure.comap Subtype.val volume)he:MeasurePreserving (⇑(homeomorphUnitSphereProd (Space d))) (Measure.comap Subtype.val volume)
  (volume.toSphere.prod (Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1)))⊢ Integrable (((fun x => f ↑x) ∘ ⇑(homeomorphUnitSphereProd (Space d)).symm) ∘ ⇑(homeomorphUnitSphereProd (Space d)))
  (Measure.comap Subtype.val volume)h₂d:ℕF:Type u_1inst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Ff:Space d → Fhf:Integrable f volumes:Set (Space d) := {0}ᶜh1:Integrable (fun x => f ↑x) (Measure.comap Subtype.val volume)he:MeasurePreserving (⇑(homeomorphUnitSphereProd (Space d))) (Measure.comap Subtype.val volume)
  (volume.toSphere.prod (Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1)))⊢ MeasurableEmbedding ⇑(homeomorphUnitSphereProd (Space d))d:ℕF:Type u_1inst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Ff:Space d → Fhf:Integrable f volumes:Set (Space d) := {0}ᶜh1:Integrable (fun x => f ↑x) (Measure.comap Subtype.val volume)he:MeasurePreserving (⇑(homeomorphUnitSphereProd (Space d))) (Measure.comap Subtype.val volume)
  (volume.toSphere.prod (Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1)))⊢ Integrable (((fun x => f ↑x) ∘ ⇑(homeomorphUnitSphereProd (Space d)).symm) ∘ ⇑(homeomorphUnitSphereProd (Space d)))
  (Measure.comap Subtype.val volume)h₂d:ℕF:Type u_1inst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Ff:Space d → Fhf:Integrable f volumes:Set (Space d) := {0}ᶜh1:Integrable (fun x => f ↑x) (Measure.comap Subtype.val volume)he:MeasurePreserving (⇑(homeomorphUnitSphereProd (Space d))) (Measure.comap Subtype.val volume)
  (volume.toSphere.prod (Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1)))⊢ MeasurableEmbedding ⇑(homeomorphUnitSphereProd (Space d))d:ℕF:Type u_1inst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Ff:Space d → Fhf:Integrable f volumes:Set (Space d) := {0}ᶜh1:Integrable (fun x => f ↑x) (Measure.comap Subtype.val volume)he:MeasurePreserving (⇑(homeomorphUnitSphereProd (Space d))) (Measure.comap Subtype.val volume)
  (volume.toSphere.prod (Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1)))hcomp:Integrable ((fun x => f ↑x) ∘ ⇑(homeomorphUnitSphereProd (Space d)).symm)
  (volume.toSphere.prod (Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1)))⊢ Integrable (fun x => f (↑x.2 • ↑x.1)) (volume.toSphere.prod (Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1)))]d:ℕF:Type u_1inst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Ff:Space d → Fhf:Integrable f volumes:Set (Space d) := {0}ᶜh1:Integrable (fun x => f ↑x) (Measure.comap Subtype.val volume)he:MeasurePreserving (⇑(homeomorphUnitSphereProd (Space d))) (Measure.comap Subtype.val volume)
  (volume.toSphere.prod (Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1)))⊢ Integrable (((fun x => f ↑x) ∘ ⇑(homeomorphUnitSphereProd (Space d)).symm) ∘ ⇑(homeomorphUnitSphereProd (Space d)))
  (Measure.comap Subtype.val volume)h₂d:ℕF:Type u_1inst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Ff:Space d → Fhf:Integrable f volumes:Set (Space d) := {0}ᶜh1:Integrable (fun x => f ↑x) (Measure.comap Subtype.val volume)he:MeasurePreserving (⇑(homeomorphUnitSphereProd (Space d))) (Measure.comap Subtype.val volume)
  (volume.toSphere.prod (Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1)))⊢ MeasurableEmbedding ⇑(homeomorphUnitSphereProd (Space d))d:ℕF:Type u_1inst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Ff:Space d → Fhf:Integrable f volumes:Set (Space d) := {0}ᶜh1:Integrable (fun x => f ↑x) (Measure.comap Subtype.val volume)he:MeasurePreserving (⇑(homeomorphUnitSphereProd (Space d))) (Measure.comap Subtype.val volume)
  (volume.toSphere.prod (Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1)))hcomp:Integrable ((fun x => f ↑x) ∘ ⇑(homeomorphUnitSphereProd (Space d)).symm)
  (volume.toSphere.prod (Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1)))⊢ Integrable (fun x => f (↑x.2 • ↑x.1)) (volume.toSphere.prod (Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1)))
    ·d:ℕF:Type u_1inst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Ff:Space d → Fhf:Integrable f volumes:Set (Space d) := {0}ᶜh1:Integrable (fun x => f ↑x) (Measure.comap Subtype.val volume)he:MeasurePreserving (⇑(homeomorphUnitSphereProd (Space d))) (Measure.comap Subtype.val volume)
  (volume.toSphere.prod (Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1)))⊢ Integrable (((fun x => f ↑x) ∘ ⇑(homeomorphUnitSphereProd (Space d)).symm) ∘ ⇑(homeomorphUnitSphereProd (Space d)))
  (Measure.comap Subtype.val volume)d:ℕF:Type u_1inst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Ff:Space d → Fhf:Integrable f volumes:Set (Space d) := {0}ᶜh1:Integrable (fun x => f ↑x) (Measure.comap Subtype.val volume)he:MeasurePreserving (⇑(homeomorphUnitSphereProd (Space d))) (Measure.comap Subtype.val volume)
  (volume.toSphere.prod (Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1)))hcomp:Integrable ((fun x => f ↑x) ∘ ⇑(homeomorphUnitSphereProd (Space d)).symm)
  (volume.toSphere.prod (Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1)))⊢ Integrable (fun x => f (↑x.2 • ↑x.1)) (volume.toSphere.prod (Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1))) convert h1d:ℕF:Type u_1inst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Ff:Space d → Fhf:Integrable f volumes:Set (Space d) := {0}ᶜh1:Integrable (fun x => f ↑x) (Measure.comap Subtype.val volume)he:MeasurePreserving (⇑(homeomorphUnitSphereProd (Space d))) (Measure.comap Subtype.val volume)
  (volume.toSphere.prod (Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1)))x✝:↑{0}ᶜ⊢ (((fun x => f ↑x) ∘ ⇑(homeomorphUnitSphereProd (Space d)).symm) ∘ ⇑(homeomorphUnitSphereProd (Space d))) x✝ = f ↑x✝d:ℕF:Type u_1inst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Ff:Space d → Fhf:Integrable f volumes:Set (Space d) := {0}ᶜh1:Integrable (fun x => f ↑x) (Measure.comap Subtype.val volume)he:MeasurePreserving (⇑(homeomorphUnitSphereProd (Space d))) (Measure.comap Subtype.val volume)
  (volume.toSphere.prod (Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1)))hcomp:Integrable ((fun x => f ↑x) ∘ ⇑(homeomorphUnitSphereProd (Space d)).symm)
  (volume.toSphere.prod (Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1)))⊢ Integrable (fun x => f (↑x.2 • ↑x.1)) (volume.toSphere.prod (Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1)))
      simp only [Function.comp_apply, Homeomorph.symm_apply_apply]All goals completed! 🐙d:ℕF:Type u_1inst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Ff:Space d → Fhf:Integrable f volumes:Set (Space d) := {0}ᶜh1:Integrable (fun x => f ↑x) (Measure.comap Subtype.val volume)he:MeasurePreserving (⇑(homeomorphUnitSphereProd (Space d))) (Measure.comap Subtype.val volume)
  (volume.toSphere.prod (Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1)))hcomp:Integrable ((fun x => f ↑x) ∘ ⇑(homeomorphUnitSphereProd (Space d)).symm)
  (volume.toSphere.prod (Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1)))⊢ Integrable (fun x => f (↑x.2 • ↑x.1)) (volume.toSphere.prod (Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1)))
    ·h₂d:ℕF:Type u_1inst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Ff:Space d → Fhf:Integrable f volumes:Set (Space d) := {0}ᶜh1:Integrable (fun x => f ↑x) (Measure.comap Subtype.val volume)he:MeasurePreserving (⇑(homeomorphUnitSphereProd (Space d))) (Measure.comap Subtype.val volume)
  (volume.toSphere.prod (Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1)))⊢ MeasurableEmbedding ⇑(homeomorphUnitSphereProd (Space d))d:ℕF:Type u_1inst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Ff:Space d → Fhf:Integrable f volumes:Set (Space d) := {0}ᶜh1:Integrable (fun x => f ↑x) (Measure.comap Subtype.val volume)he:MeasurePreserving (⇑(homeomorphUnitSphereProd (Space d))) (Measure.comap Subtype.val volume)
  (volume.toSphere.prod (Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1)))hcomp:Integrable ((fun x => f ↑x) ∘ ⇑(homeomorphUnitSphereProd (Space d)).symm)
  (volume.toSphere.prod (Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1)))⊢ Integrable (fun x => f (↑x.2 • ↑x.1)) (volume.toSphere.prod (Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1))) exact Homeomorph.measurableEmbedding (homeomorphUnitSphereProd (Space d))d:ℕF:Type u_1inst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Ff:Space d → Fhf:Integrable f volumes:Set (Space d) := {0}ᶜh1:Integrable (fun x => f ↑x) (Measure.comap Subtype.val volume)he:MeasurePreserving (⇑(homeomorphUnitSphereProd (Space d))) (Measure.comap Subtype.val volume)
  (volume.toSphere.prod (Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1)))hcomp:Integrable ((fun x => f ↑x) ∘ ⇑(homeomorphUnitSphereProd (Space d)).symm)
  (volume.toSphere.prod (Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1)))⊢ Integrable (fun x => f (↑x.2 • ↑x.1)) (volume.toSphere.prod (Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1)))d:ℕF:Type u_1inst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Ff:Space d → Fhf:Integrable f volumes:Set (Space d) := {0}ᶜh1:Integrable (fun x => f ↑x) (Measure.comap Subtype.val volume)he:MeasurePreserving (⇑(homeomorphUnitSphereProd (Space d))) (Measure.comap Subtype.val volume)
  (volume.toSphere.prod (Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1)))hcomp:Integrable ((fun x => f ↑x) ∘ ⇑(homeomorphUnitSphereProd (Space d)).symm)
  (volume.toSphere.prod (Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1)))⊢ Integrable (fun x => f (↑x.2 • ↑x.1)) (volume.toSphere.prod (Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1)))
  exact hcompAll goals completed! 🐙

lemma integral_volume_eq_spherical_iterated {d : ℕ} [NeZero d] {F : Type*}
    [NormedAddCommGroup F] [NormedSpace ℝ F] (f : Space d → F)
    (hf : Integrable f volume) :
    ∫ x : Space d, f x =
      ∫ n : ↑(Metric.sphere (0 : Space d) 1),
        ∫ r : Set.Ioi (0 : ℝ), f (r.1 • n.1)
          ∂(Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1))
        ∂(volume (α := Space d).toSphere) := byd:ℕinst✝²:NeZero dF:Type u_1inst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Ff:Space d → Fhf:Integrable f volume⊢ ∫ (x : Space d), f x =
  ∫ (n : ↑(Metric.sphere 0 1)),
    ∫ (r : ↑(Set.Ioi 0)), f (↑r • ↑n) ∂Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1) ∂volume.toSphere
  rw [integral_volume_eq_sphericald:ℕinst✝²:NeZero dF:Type u_1inst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Ff:Space d → Fhf:Integrable f volume⊢ ∫ (x : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)),
    f (↑x.2 • ↑x.1) ∂volume.toSphere.prod (Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1)) =
  ∫ (n : ↑(Metric.sphere 0 1)),
    ∫ (r : ↑(Set.Ioi 0)), f (↑r • ↑n) ∂Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1) ∂volume.toSphered:ℕinst✝²:NeZero dF:Type u_1inst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Ff:Space d → Fhf:Integrable f volume⊢ ∫ (x : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)),
    f (↑x.2 • ↑x.1) ∂volume.toSphere.prod (Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1)) =
  ∫ (n : ↑(Metric.sphere 0 1)),
    ∫ (r : ↑(Set.Ioi 0)), f (↑r • ↑n) ∂Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1) ∂volume.toSphere]d:ℕinst✝²:NeZero dF:Type u_1inst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Ff:Space d → Fhf:Integrable f volume⊢ ∫ (x : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)),
    f (↑x.2 • ↑x.1) ∂volume.toSphere.prod (Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1)) =
  ∫ (n : ↑(Metric.sphere 0 1)),
    ∫ (r : ↑(Set.Ioi 0)), f (↑r • ↑n) ∂Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1) ∂volume.toSphere
  rw [MeasureTheory.integral_prodd:ℕinst✝²:NeZero dF:Type u_1inst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Ff:Space d → Fhf:Integrable f volume⊢ ∫ (x : ↑(Metric.sphere 0 1)),
    ∫ (y : ↑(Set.Ioi 0)),
      f (↑(x, y).2 • ↑(x, y).1) ∂Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1) ∂volume.toSphere =
  ∫ (n : ↑(Metric.sphere 0 1)),
    ∫ (r : ↑(Set.Ioi 0)), f (↑r • ↑n) ∂Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1) ∂volume.toSpherehfd:ℕinst✝²:NeZero dF:Type u_1inst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Ff:Space d → Fhf:Integrable f volume⊢ Integrable (fun x => f (↑x.2 • ↑x.1)) (volume.toSphere.prod (Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1)))hfd:ℕinst✝²:NeZero dF:Type u_1inst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Ff:Space d → Fhf:Integrable f volume⊢ Integrable (fun x => f (↑x.2 • ↑x.1)) (volume.toSphere.prod (Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1)))]hfd:ℕinst✝²:NeZero dF:Type u_1inst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Ff:Space d → Fhf:Integrable f volume⊢ Integrable (fun x => f (↑x.2 • ↑x.1)) (volume.toSphere.prod (Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1)))
  exact integrable_spherical_of_integrable hfAll goals completed! 🐙

/- An instance of `sfinite` on the spherical integral measure on `Space d`.
  This is needed in many of the calculations related to spherical integrals,
  but cannot be inferred by Lean without this. -/
instance : SFinite (@Measure.comap ↑(Set.Ioi 0) ℝ Subtype.instMeasurableSpace
        Real.measureSpace.toMeasurableSpace Subtype.val volume) := by⊢ SFinite (Measure.comap Subtype.val volume)
      refine { out' := ?_ }⊢ ∃ m, (∀ (n : ℕ), IsFiniteMeasure (m n)) ∧ Measure.comap Subtype.val volume = Measure.sum m
      have h1 := SFinite.out' (μ := volume (α := ℝ))h1:∃ m, (∀ (n : ℕ), IsFiniteMeasure (m n)) ∧ volume = Measure.sum m⊢ ∃ m, (∀ (n : ℕ), IsFiniteMeasure (m n)) ∧ Measure.comap Subtype.val volume = Measure.sum m
      obtain ⟨m, h⟩ := h1m:ℕ → Measure ℝh:(∀ (n : ℕ), IsFiniteMeasure (m n)) ∧ volume = Measure.sum m⊢ ∃ m, (∀ (n : ℕ), IsFiniteMeasure (m n)) ∧ Measure.comap Subtype.val volume = Measure.sum m
      use fun n => Measure.comap Subtype.val (m n)hm:ℕ → Measure ℝh:(∀ (n : ℕ), IsFiniteMeasure (m n)) ∧ volume = Measure.sum m⊢ (∀ (n : ℕ), IsFiniteMeasure ((fun n => Measure.comap Subtype.val (m n)) n)) ∧
  Measure.comap Subtype.val volume = Measure.sum fun n => Measure.comap Subtype.val (m n)
      apply And.introh.leftm:ℕ → Measure ℝh:(∀ (n : ℕ), IsFiniteMeasure (m n)) ∧ volume = Measure.sum m⊢ ∀ (n : ℕ), IsFiniteMeasure (Measure.comap Subtype.val (m n))h.rightm:ℕ → Measure ℝh:(∀ (n : ℕ), IsFiniteMeasure (m n)) ∧ volume = Measure.sum m⊢ Measure.comap Subtype.val volume = Measure.sum fun n => Measure.comap Subtype.val (m n)
      ·h.leftm:ℕ → Measure ℝh:(∀ (n : ℕ), IsFiniteMeasure (m n)) ∧ volume = Measure.sum m⊢ ∀ (n : ℕ), IsFiniteMeasure (Measure.comap Subtype.val (m n)) intro nh.leftm:ℕ → Measure ℝh:(∀ (n : ℕ), IsFiniteMeasure (m n)) ∧ volume = Measure.sum mn:ℕ⊢ IsFiniteMeasure (Measure.comap Subtype.val (m n))
        refine (isFiniteMeasure_iff (Measure.comap Subtype.val (m n))).mpr ?_h.leftm:ℕ → Measure ℝh:(∀ (n : ℕ), IsFiniteMeasure (m n)) ∧ volume = Measure.sum mn:ℕ⊢ (Measure.comap Subtype.val (m n)) Set.univ < ⊤
        rw [MeasurableEmbedding.comap_apply (MeasurableEmbedding.subtype_coe measurableSet_Ioi)h.leftm:ℕ → Measure ℝh:(∀ (n : ℕ), IsFiniteMeasure (m n)) ∧ volume = Measure.sum mn:ℕ⊢ (m n) (Subtype.val '' Set.univ) < ⊤h.leftm:ℕ → Measure ℝh:(∀ (n : ℕ), IsFiniteMeasure (m n)) ∧ volume = Measure.sum mn:ℕ⊢ (m n) (Subtype.val '' Set.univ) < ⊤]h.leftm:ℕ → Measure ℝh:(∀ (n : ℕ), IsFiniteMeasure (m n)) ∧ volume = Measure.sum mn:ℕ⊢ (m n) (Subtype.val '' Set.univ) < ⊤
        simp only [Set.image_univ, Subtype.range_coe_subtype, Set.mem_Ioi]h.leftm:ℕ → Measure ℝh:(∀ (n : ℕ), IsFiniteMeasure (m n)) ∧ volume = Measure.sum mn:ℕ⊢ (m n) {x | 0 < x} < ⊤
        have hm := h.1 nh.leftm:ℕ → Measure ℝh:(∀ (n : ℕ), IsFiniteMeasure (m n)) ∧ volume = Measure.sum mn:ℕhm:IsFiniteMeasure (m n)⊢ (m n) {x | 0 < x} < ⊤
        exact measure_lt_top (m n) {x | 0 < x}All goals completed! 🐙
      ·h.rightm:ℕ → Measure ℝh:(∀ (n : ℕ), IsFiniteMeasure (m n)) ∧ volume = Measure.sum m⊢ Measure.comap Subtype.val volume = Measure.sum fun n => Measure.comap Subtype.val (m n) ext s hsh.rightm:ℕ → Measure ℝh:(∀ (n : ℕ), IsFiniteMeasure (m n)) ∧ volume = Measure.sum ms:Set ↑(Set.Ioi 0)hs:MeasurableSet s⊢ (Measure.comap Subtype.val volume) s = (Measure.sum fun n => Measure.comap Subtype.val (m n)) s
        rw [MeasurableEmbedding.comap_apply,h.rightm:ℕ → Measure ℝh:(∀ (n : ℕ), IsFiniteMeasure (m n)) ∧ volume = Measure.sum ms:Set ↑(Set.Ioi 0)hs:MeasurableSet s⊢ volume (Subtype.val '' s) = (Measure.sum fun n => Measure.comap Subtype.val (m n)) sh.right.hfm:ℕ → Measure ℝh:(∀ (n : ℕ), IsFiniteMeasure (m n)) ∧ volume = Measure.sum ms:Set ↑(Set.Ioi 0)hs:MeasurableSet s⊢ MeasurableEmbedding Subtype.valh.rightm:ℕ → Measure ℝh:(∀ (n : ℕ), IsFiniteMeasure (m n)) ∧ volume = Measure.sum ms:Set ↑(Set.Ioi 0)hs:MeasurableSet s⊢ volume (Subtype.val '' s) = ∑' (i : ℕ), (Measure.comap Subtype.val (m i)) sh.right.hsm:ℕ → Measure ℝh:(∀ (n : ℕ), IsFiniteMeasure (m n)) ∧ volume = Measure.sum ms:Set ↑(Set.Ioi 0)hs:MeasurableSet s⊢ MeasurableSet sh.right.hfm:ℕ → Measure ℝh:(∀ (n : ℕ), IsFiniteMeasure (m n)) ∧ volume = Measure.sum ms:Set ↑(Set.Ioi 0)hs:MeasurableSet s⊢ MeasurableEmbedding Subtype.val Measure.sum_applyh.rightm:ℕ → Measure ℝh:(∀ (n : ℕ), IsFiniteMeasure (m n)) ∧ volume = Measure.sum ms:Set ↑(Set.Ioi 0)hs:MeasurableSet s⊢ volume (Subtype.val '' s) = ∑' (i : ℕ), (Measure.comap Subtype.val (m i)) sh.right.hsm:ℕ → Measure ℝh:(∀ (n : ℕ), IsFiniteMeasure (m n)) ∧ volume = Measure.sum ms:Set ↑(Set.Ioi 0)hs:MeasurableSet s⊢ MeasurableSet sh.right.hfm:ℕ → Measure ℝh:(∀ (n : ℕ), IsFiniteMeasure (m n)) ∧ volume = Measure.sum ms:Set ↑(Set.Ioi 0)hs:MeasurableSet s⊢ MeasurableEmbedding Subtype.valh.rightm:ℕ → Measure ℝh:(∀ (n : ℕ), IsFiniteMeasure (m n)) ∧ volume = Measure.sum ms:Set ↑(Set.Ioi 0)hs:MeasurableSet s⊢ volume (Subtype.val '' s) = ∑' (i : ℕ), (Measure.comap Subtype.val (m i)) sh.right.hsm:ℕ → Measure ℝh:(∀ (n : ℕ), IsFiniteMeasure (m n)) ∧ volume = Measure.sum ms:Set ↑(Set.Ioi 0)hs:MeasurableSet s⊢ MeasurableSet sh.right.hfm:ℕ → Measure ℝh:(∀ (n : ℕ), IsFiniteMeasure (m n)) ∧ volume = Measure.sum ms:Set ↑(Set.Ioi 0)hs:MeasurableSet s⊢ MeasurableEmbedding Subtype.val]h.rightm:ℕ → Measure ℝh:(∀ (n : ℕ), IsFiniteMeasure (m n)) ∧ volume = Measure.sum ms:Set ↑(Set.Ioi 0)hs:MeasurableSet s⊢ volume (Subtype.val '' s) = ∑' (i : ℕ), (Measure.comap Subtype.val (m i)) sh.right.hsm:ℕ → Measure ℝh:(∀ (n : ℕ), IsFiniteMeasure (m n)) ∧ volume = Measure.sum ms:Set ↑(Set.Ioi 0)hs:MeasurableSet s⊢ MeasurableSet sh.right.hfm:ℕ → Measure ℝh:(∀ (n : ℕ), IsFiniteMeasure (m n)) ∧ volume = Measure.sum ms:Set ↑(Set.Ioi 0)hs:MeasurableSet s⊢ MeasurableEmbedding Subtype.val
        conv_rhs =>
          enter [1, i]m:ℕ → Measure ℝh:(∀ (n : ℕ), IsFiniteMeasure (m n)) ∧ volume = Measure.sum ms:Set ↑(Set.Ioi 0)hs:MeasurableSet si:ℕ| (Measure.comap Subtype.val (m i)) s
          rw [MeasurableEmbedding.comap_apply (MeasurableEmbedding.subtype_coe measurableSet_Ioi)]m:ℕ → Measure ℝh:(∀ (n : ℕ), IsFiniteMeasure (m n)) ∧ volume = Measure.sum ms:Set ↑(Set.Ioi 0)hs:MeasurableSet si:ℕ| (m i) (Subtype.val '' s)
        have h2 := h.2h.rightm:ℕ → Measure ℝh:(∀ (n : ℕ), IsFiniteMeasure (m n)) ∧ volume = Measure.sum ms:Set ↑(Set.Ioi 0)hs:MeasurableSet sh2:volume = Measure.sum m⊢ volume (Subtype.val '' s) = ∑' (i : ℕ), (m i) (Subtype.val '' s)h.right.hsm:ℕ → Measure ℝh:(∀ (n : ℕ), IsFiniteMeasure (m n)) ∧ volume = Measure.sum ms:Set ↑(Set.Ioi 0)hs:MeasurableSet s⊢ MeasurableSet sh.right.hfm:ℕ → Measure ℝh:(∀ (n : ℕ), IsFiniteMeasure (m n)) ∧ volume = Measure.sum ms:Set ↑(Set.Ioi 0)hs:MeasurableSet s⊢ MeasurableEmbedding Subtype.val
        rw [Measure.ext_iff'h.rightm:ℕ → Measure ℝh:(∀ (n : ℕ), IsFiniteMeasure (m n)) ∧ volume = Measure.sum ms:Set ↑(Set.Ioi 0)hs:MeasurableSet sh2:∀ (s : Set ℝ), volume s = (Measure.sum m) s⊢ volume (Subtype.val '' s) = ∑' (i : ℕ), (m i) (Subtype.val '' s)h.right.hsm:ℕ → Measure ℝh:(∀ (n : ℕ), IsFiniteMeasure (m n)) ∧ volume = Measure.sum ms:Set ↑(Set.Ioi 0)hs:MeasurableSet s⊢ MeasurableSet sh.right.hfm:ℕ → Measure ℝh:(∀ (n : ℕ), IsFiniteMeasure (m n)) ∧ volume = Measure.sum ms:Set ↑(Set.Ioi 0)hs:MeasurableSet s⊢ MeasurableEmbedding Subtype.valh.rightm:ℕ → Measure ℝh:(∀ (n : ℕ), IsFiniteMeasure (m n)) ∧ volume = Measure.sum ms:Set ↑(Set.Ioi 0)hs:MeasurableSet sh2:∀ (s : Set ℝ), volume s = (Measure.sum m) s⊢ volume (Subtype.val '' s) = ∑' (i : ℕ), (m i) (Subtype.val '' s)h.right.hsm:ℕ → Measure ℝh:(∀ (n : ℕ), IsFiniteMeasure (m n)) ∧ volume = Measure.sum ms:Set ↑(Set.Ioi 0)hs:MeasurableSet s⊢ MeasurableSet sh.right.hfm:ℕ → Measure ℝh:(∀ (n : ℕ), IsFiniteMeasure (m n)) ∧ volume = Measure.sum ms:Set ↑(Set.Ioi 0)hs:MeasurableSet s⊢ MeasurableEmbedding Subtype.val] at h2h.rightm:ℕ → Measure ℝh:(∀ (n : ℕ), IsFiniteMeasure (m n)) ∧ volume = Measure.sum ms:Set ↑(Set.Ioi 0)hs:MeasurableSet sh2:∀ (s : Set ℝ), volume s = (Measure.sum m) s⊢ volume (Subtype.val '' s) = ∑' (i : ℕ), (m i) (Subtype.val '' s)h.right.hsm:ℕ → Measure ℝh:(∀ (n : ℕ), IsFiniteMeasure (m n)) ∧ volume = Measure.sum ms:Set ↑(Set.Ioi 0)hs:MeasurableSet s⊢ MeasurableSet sh.right.hfm:ℕ → Measure ℝh:(∀ (n : ℕ), IsFiniteMeasure (m n)) ∧ volume = Measure.sum ms:Set ↑(Set.Ioi 0)hs:MeasurableSet s⊢ MeasurableEmbedding Subtype.val
        rw [← Measure.sum_applyh.rightm:ℕ → Measure ℝh:(∀ (n : ℕ), IsFiniteMeasure (m n)) ∧ volume = Measure.sum ms:Set ↑(Set.Ioi 0)hs:MeasurableSet sh2:∀ (s : Set ℝ), volume s = (Measure.sum m) s⊢ volume (Subtype.val '' s) = (Measure.sum m) (Subtype.val '' s)h.right.hsm:ℕ → Measure ℝh:(∀ (n : ℕ), IsFiniteMeasure (m n)) ∧ volume = Measure.sum ms:Set ↑(Set.Ioi 0)hs:MeasurableSet sh2:∀ (s : Set ℝ), volume s = (Measure.sum m) s⊢ MeasurableSet (Subtype.val '' s)h.right.hsm:ℕ → Measure ℝh:(∀ (n : ℕ), IsFiniteMeasure (m n)) ∧ volume = Measure.sum ms:Set ↑(Set.Ioi 0)hs:MeasurableSet s⊢ MeasurableSet sh.right.hfm:ℕ → Measure ℝh:(∀ (n : ℕ), IsFiniteMeasure (m n)) ∧ volume = Measure.sum ms:Set ↑(Set.Ioi 0)hs:MeasurableSet s⊢ MeasurableEmbedding Subtype.valh.rightm:ℕ → Measure ℝh:(∀ (n : ℕ), IsFiniteMeasure (m n)) ∧ volume = Measure.sum ms:Set ↑(Set.Ioi 0)hs:MeasurableSet sh2:∀ (s : Set ℝ), volume s = (Measure.sum m) s⊢ volume (Subtype.val '' s) = (Measure.sum m) (Subtype.val '' s)h.right.hsm:ℕ → Measure ℝh:(∀ (n : ℕ), IsFiniteMeasure (m n)) ∧ volume = Measure.sum ms:Set ↑(Set.Ioi 0)hs:MeasurableSet sh2:∀ (s : Set ℝ), volume s = (Measure.sum m) s⊢ MeasurableSet (Subtype.val '' s)h.right.hsm:ℕ → Measure ℝh:(∀ (n : ℕ), IsFiniteMeasure (m n)) ∧ volume = Measure.sum ms:Set ↑(Set.Ioi 0)hs:MeasurableSet s⊢ MeasurableSet sh.right.hfm:ℕ → Measure ℝh:(∀ (n : ℕ), IsFiniteMeasure (m n)) ∧ volume = Measure.sum ms:Set ↑(Set.Ioi 0)hs:MeasurableSet s⊢ MeasurableEmbedding Subtype.val]h.rightm:ℕ → Measure ℝh:(∀ (n : ℕ), IsFiniteMeasure (m n)) ∧ volume = Measure.sum ms:Set ↑(Set.Ioi 0)hs:MeasurableSet sh2:∀ (s : Set ℝ), volume s = (Measure.sum m) s⊢ volume (Subtype.val '' s) = (Measure.sum m) (Subtype.val '' s)h.right.hsm:ℕ → Measure ℝh:(∀ (n : ℕ), IsFiniteMeasure (m n)) ∧ volume = Measure.sum ms:Set ↑(Set.Ioi 0)hs:MeasurableSet sh2:∀ (s : Set ℝ), volume s = (Measure.sum m) s⊢ MeasurableSet (Subtype.val '' s)h.right.hsm:ℕ → Measure ℝh:(∀ (n : ℕ), IsFiniteMeasure (m n)) ∧ volume = Measure.sum ms:Set ↑(Set.Ioi 0)hs:MeasurableSet s⊢ MeasurableSet sh.right.hfm:ℕ → Measure ℝh:(∀ (n : ℕ), IsFiniteMeasure (m n)) ∧ volume = Measure.sum ms:Set ↑(Set.Ioi 0)hs:MeasurableSet s⊢ MeasurableEmbedding Subtype.val
        exact h2 (Subtype.val '' s)h.right.hsm:ℕ → Measure ℝh:(∀ (n : ℕ), IsFiniteMeasure (m n)) ∧ volume = Measure.sum ms:Set ↑(Set.Ioi 0)hs:MeasurableSet sh2:∀ (s : Set ℝ), volume s = (Measure.sum m) s⊢ MeasurableSet (Subtype.val '' s)h.right.hsm:ℕ → Measure ℝh:(∀ (n : ℕ), IsFiniteMeasure (m n)) ∧ volume = Measure.sum ms:Set ↑(Set.Ioi 0)hs:MeasurableSet s⊢ MeasurableSet sh.right.hfm:ℕ → Measure ℝh:(∀ (n : ℕ), IsFiniteMeasure (m n)) ∧ volume = Measure.sum ms:Set ↑(Set.Ioi 0)hs:MeasurableSet s⊢ MeasurableEmbedding Subtype.val
        refine MeasurableSet.subtype_image measurableSet_Ioi hsh.right.hsm:ℕ → Measure ℝh:(∀ (n : ℕ), IsFiniteMeasure (m n)) ∧ volume = Measure.sum ms:Set ↑(Set.Ioi 0)hs:MeasurableSet s⊢ MeasurableSet sh.right.hfm:ℕ → Measure ℝh:(∀ (n : ℕ), IsFiniteMeasure (m n)) ∧ volume = Measure.sum ms:Set ↑(Set.Ioi 0)hs:MeasurableSet s⊢ MeasurableEmbedding Subtype.val
        exact hsh.right.hfm:ℕ → Measure ℝh:(∀ (n : ℕ), IsFiniteMeasure (m n)) ∧ volume = Measure.sum ms:Set ↑(Set.Ioi 0)hs:MeasurableSet s⊢ MeasurableEmbedding Subtype.val
        apply MeasurableEmbedding.subtype_coeh.right.hfm:ℕ → Measure ℝh:(∀ (n : ℕ), IsFiniteMeasure (m n)) ∧ volume = Measure.sum ms:Set ↑(Set.Ioi 0)hs:MeasurableSet s⊢ MeasurableSet (Set.Ioi 0)
        simpAll goals completed! 🐙

lemma integral_volume_eq_spherical_integral {d : ℕ} [NeZero d] {F : Type*}
    [NormedAddCommGroup F] [NormedSpace ℝ F] (f : Space d → F)
    (hf : Integrable f volume) :
    ∫ x : Space d, f x =
      ∫ n : ↑(Metric.sphere (0 : Space d) 1),
        ∫ r : Set.Ioi (0 : ℝ), (r.1 ^ (d - 1)) • f (r.1 • n.1)
          ∂(.comap Subtype.val volume)
        ∂(volume (α := Space d).toSphere) := byd:ℕinst✝²:NeZero dF:Type u_1inst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Ff:Space d → Fhf:Integrable f volume⊢ ∫ (x : Space d), f x =
  ∫ (n : ↑(Metric.sphere 0 1)),
    ∫ (r : ↑(Set.Ioi 0)), ↑r ^ (d - 1) • f (↑r • ↑n) ∂Measure.comap Subtype.val volume ∂volume.toSphere
  rw [integral_volume_eq_spherical_iterated f hfd:ℕinst✝²:NeZero dF:Type u_1inst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Ff:Space d → Fhf:Integrable f volume⊢ ∫ (n : ↑(Metric.sphere 0 1)),
    ∫ (r : ↑(Set.Ioi 0)), f (↑r • ↑n) ∂Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1) ∂volume.toSphere =
  ∫ (n : ↑(Metric.sphere 0 1)),
    ∫ (r : ↑(Set.Ioi 0)), ↑r ^ (d - 1) • f (↑r • ↑n) ∂Measure.comap Subtype.val volume ∂volume.toSphered:ℕinst✝²:NeZero dF:Type u_1inst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Ff:Space d → Fhf:Integrable f volume⊢ ∫ (n : ↑(Metric.sphere 0 1)),
    ∫ (r : ↑(Set.Ioi 0)), f (↑r • ↑n) ∂Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1) ∂volume.toSphere =
  ∫ (n : ↑(Metric.sphere 0 1)),
    ∫ (r : ↑(Set.Ioi 0)), ↑r ^ (d - 1) • f (↑r • ↑n) ∂Measure.comap Subtype.val volume ∂volume.toSphere]d:ℕinst✝²:NeZero dF:Type u_1inst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Ff:Space d → Fhf:Integrable f volume⊢ ∫ (n : ↑(Metric.sphere 0 1)),
    ∫ (r : ↑(Set.Ioi 0)), f (↑r • ↑n) ∂Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1) ∂volume.toSphere =
  ∫ (n : ↑(Metric.sphere 0 1)),
    ∫ (r : ↑(Set.Ioi 0)), ↑r ^ (d - 1) • f (↑r • ↑n) ∂Measure.comap Subtype.val volume ∂volume.toSphere
  congre_fd:ℕinst✝²:NeZero dF:Type u_1inst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Ff:Space d → Fhf:Integrable f volume⊢ (fun n => ∫ (r : ↑(Set.Ioi 0)), f (↑r • ↑n) ∂Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1)) = fun n =>
  ∫ (r : ↑(Set.Ioi 0)), ↑r ^ (d - 1) • f (↑r • ↑n) ∂Measure.comap Subtype.val volume
  funext ne_fd:ℕinst✝²:NeZero dF:Type u_1inst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Ff:Space d → Fhf:Integrable f volumen:↑(Metric.sphere 0 1)⊢ ∫ (r : ↑(Set.Ioi 0)), f (↑r • ↑n) ∂Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1) =
  ∫ (r : ↑(Set.Ioi 0)), ↑r ^ (d - 1) • f (↑r • ↑n) ∂Measure.comap Subtype.val volume
  simp [Measure.volumeIoiPow]e_fd:ℕinst✝²:NeZero dF:Type u_1inst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Ff:Space d → Fhf:Integrable f volumen:↑(Metric.sphere 0 1)⊢ (∫ (r : ↑(Set.Ioi 0)),
    f (↑r • ↑n) ∂(Measure.comap Subtype.val volume).withDensity fun r => ENNReal.ofReal (↑r ^ (d - 1))) =
  ∫ (r : ↑(Set.Ioi 0)), ↑r ^ (d - 1) • f (↑r • ↑n) ∂Measure.comap Subtype.val volume
  erw [integral_withDensity_eq_integral_smul (byd:ℕinst✝²:NeZero dF:Type u_1inst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Ff:Space d → Fhf:Integrable f volumen:↑(Metric.sphere 0 1)⊢ Measurable fun r => (↑r ^ (d - 1)).toNNReal fun_propAll goals completed! 🐙)]e_fd:ℕinst✝²:NeZero dF:Type u_1inst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Ff:Space d → Fhf:Integrable f volumen:↑(Metric.sphere 0 1)⊢ ∫ (x : ↑(Set.Ioi 0)), (↑x ^ (d - 1)).toNNReal • f (↑x • ↑n) ∂Measure.comap Subtype.val volume =
  ∫ (r : ↑(Set.Ioi 0)), ↑r ^ (d - 1) • f (↑r • ↑n) ∂Measure.comap Subtype.val volume
  congre_f.e_fd:ℕinst✝²:NeZero dF:Type u_1inst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Ff:Space d → Fhf:Integrable f volumen:↑(Metric.sphere 0 1)⊢ (fun x => (↑x ^ (d - 1)).toNNReal • f (↑x • ↑n)) = fun r => ↑r ^ (d - 1) • f (↑r • ↑n)
  funext re_f.e_fd:ℕinst✝²:NeZero dF:Type u_1inst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Ff:Space d → Fhf:Integrable f volumen:↑(Metric.sphere 0 1)r:↑(Set.Ioi 0)⊢ (↑r ^ (d - 1)).toNNReal • f (↑r • ↑n) = ↑r ^ (d - 1) • f (↑r • ↑n)
  have hr : 0 ≤ (r : ℝ) := le_of_lt r.2e_f.e_fd:ℕinst✝²:NeZero dF:Type u_1inst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Ff:Space d → Fhf:Integrable f volumen:↑(Metric.sphere 0 1)r:↑(Set.Ioi 0)hr:0 ≤ ↑r⊢ (↑r ^ (d - 1)).toNNReal • f (↑r • ↑n) = ↑r ^ (d - 1) • f (↑r • ↑n)
  rw [NNReal.smul_def,e_f.e_fd:ℕinst✝²:NeZero dF:Type u_1inst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Ff:Space d → Fhf:Integrable f volumen:↑(Metric.sphere 0 1)r:↑(Set.Ioi 0)hr:0 ≤ ↑r⊢ ↑(↑r ^ (d - 1)).toNNReal • f (↑r • ↑n) = ↑r ^ (d - 1) • f (↑r • ↑n)All goals completed! 🐙 Real.coe_toNNReal _ (pow_nonneg hr (d - 1))e_f.e_fd:ℕinst✝²:NeZero dF:Type u_1inst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Ff:Space d → Fhf:Integrable f volumen:↑(Metric.sphere 0 1)r:↑(Set.Ioi 0)hr:0 ≤ ↑r⊢ ↑r ^ (d - 1) • f (↑r • ↑n) = ↑r ^ (d - 1) • f (↑r • ↑n)All goals completed! 🐙]All goals completed! 🐙

D. Lower Lebesgue integral over volume to spherical



lemma lintegral_volume_eq_spherical (d : ℕ) [NeZero d]
    (f : Space d → ENNReal) (hf : Measurable f) :
    ∫⁻ x, f x ∂volume = ∫⁻ x, f (x.2.1 • x.1.1) ∂(volume (α := Space d).toSphere.prod
        (Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1))) := byd:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ ∫⁻ (x : Space d), f x =
  ∫⁻ (x : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)),
    f (↑x.2 • ↑x.1) ∂volume.toSphere.prod (Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1))
  have h0 := MeasureTheory.MeasurePreserving.lintegral_comp
    (f := fun x => f (x.2.1 • x.1.1)) (g := homeomorphUnitSphereProd _)
    (MeasureTheory.Measure.measurePreserving_homeomorphUnitSphereProd
    (volume (α := Space d)))
    (byd:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable fun x => f (↑x.2 • ↑x.1)d:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable fh0:∫⁻ (a : ↑{0}ᶜ),
    f
      (↑((homeomorphUnitSphereProd (Space d)) a).2 •
        ↑((homeomorphUnitSphereProd (Space d)) a).1) ∂Measure.comap Subtype.val volume =
  ∫⁻ (b : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)),
    f (↑b.2 • ↑b.1) ∂volume.toSphere.prod (Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1))⊢ ∫⁻ (x : Space d), f x =
  ∫⁻ (x : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)),
    f (↑x.2 • ↑x.1) ∂volume.toSphere.prod (Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1)) fun_propAll goals completed! 🐙d:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable fh0:∫⁻ (a : ↑{0}ᶜ),
    f
      (↑((homeomorphUnitSphereProd (Space d)) a).2 •
        ↑((homeomorphUnitSphereProd (Space d)) a).1) ∂Measure.comap Subtype.val volume =
  ∫⁻ (b : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)),
    f (↑b.2 • ↑b.1) ∂volume.toSphere.prod (Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1))⊢ ∫⁻ (x : Space d), f x =
  ∫⁻ (x : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)),
    f (↑x.2 • ↑x.1) ∂volume.toSphere.prod (Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1)))d:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable fh0:∫⁻ (a : ↑{0}ᶜ),
    f
      (↑((homeomorphUnitSphereProd (Space d)) a).2 •
        ↑((homeomorphUnitSphereProd (Space d)) a).1) ∂Measure.comap Subtype.val volume =
  ∫⁻ (b : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)),
    f (↑b.2 • ↑b.1) ∂volume.toSphere.prod (Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1))⊢ ∫⁻ (x : Space d), f x =
  ∫⁻ (x : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)),
    f (↑x.2 • ↑x.1) ∂volume.toSphere.prod (Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1))
  rw [← h0d:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable fh0:∫⁻ (a : ↑{0}ᶜ),
    f
      (↑((homeomorphUnitSphereProd (Space d)) a).2 •
        ↑((homeomorphUnitSphereProd (Space d)) a).1) ∂Measure.comap Subtype.val volume =
  ∫⁻ (b : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)),
    f (↑b.2 • ↑b.1) ∂volume.toSphere.prod (Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1))⊢ ∫⁻ (x : Space d), f x =
  ∫⁻ (a : ↑{0}ᶜ),
    f
      (↑((homeomorphUnitSphereProd (Space d)) a).2 •
        ↑((homeomorphUnitSphereProd (Space d)) a).1) ∂Measure.comap Subtype.val volumed:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable fh0:∫⁻ (a : ↑{0}ᶜ),
    f
      (↑((homeomorphUnitSphereProd (Space d)) a).2 •
        ↑((homeomorphUnitSphereProd (Space d)) a).1) ∂Measure.comap Subtype.val volume =
  ∫⁻ (b : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)),
    f (↑b.2 • ↑b.1) ∂volume.toSphere.prod (Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1))⊢ ∫⁻ (x : Space d), f x =
  ∫⁻ (a : ↑{0}ᶜ),
    f
      (↑((homeomorphUnitSphereProd (Space d)) a).2 •
        ↑((homeomorphUnitSphereProd (Space d)) a).1) ∂Measure.comap Subtype.val volume]d:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable fh0:∫⁻ (a : ↑{0}ᶜ),
    f
      (↑((homeomorphUnitSphereProd (Space d)) a).2 •
        ↑((homeomorphUnitSphereProd (Space d)) a).1) ∂Measure.comap Subtype.val volume =
  ∫⁻ (b : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)),
    f (↑b.2 • ↑b.1) ∂volume.toSphere.prod (Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1))⊢ ∫⁻ (x : Space d), f x =
  ∫⁻ (a : ↑{0}ᶜ),
    f
      (↑((homeomorphUnitSphereProd (Space d)) a).2 •
        ↑((homeomorphUnitSphereProd (Space d)) a).1) ∂Measure.comap Subtype.val volume
  simp only [homeomorphUnitSphereProd_apply_snd_coe, homeomorphUnitSphereProd_apply_fst_coe]d:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable fh0:∫⁻ (a : ↑{0}ᶜ),
    f
      (↑((homeomorphUnitSphereProd (Space d)) a).2 •
        ↑((homeomorphUnitSphereProd (Space d)) a).1) ∂Measure.comap Subtype.val volume =
  ∫⁻ (b : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)),
    f (↑b.2 • ↑b.1) ∂volume.toSphere.prod (Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1))⊢ ∫⁻ (x : Space d), f x = ∫⁻ (a : ↑{0}ᶜ), f (‖↑a‖ • ‖↑a‖⁻¹ • ↑a) ∂Measure.comap Subtype.val volume
  let f' : (x : (Space d)) → ENNReal := fun x => f (‖↑x‖ • ‖↑x‖⁻¹ • ↑x)d:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable fh0:∫⁻ (a : ↑{0}ᶜ),
    f
      (↑((homeomorphUnitSphereProd (Space d)) a).2 •
        ↑((homeomorphUnitSphereProd (Space d)) a).1) ∂Measure.comap Subtype.val volume =
  ∫⁻ (b : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)),
    f (↑b.2 • ↑b.1) ∂volume.toSphere.prod (Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1))f':Space d → ENNReal := fun x => f (‖x‖ • ‖x‖⁻¹ • x)⊢ ∫⁻ (x : Space d), f x = ∫⁻ (a : ↑{0}ᶜ), f (‖↑a‖ • ‖↑a‖⁻¹ • ↑a) ∂Measure.comap Subtype.val volume
  conv_rhs =>
    enter [2, x]d:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable fh0:∫⁻ (a : ↑{0}ᶜ),
    f
      (↑((homeomorphUnitSphereProd (Space d)) a).2 •
        ↑((homeomorphUnitSphereProd (Space d)) a).1) ∂Measure.comap Subtype.val volume =
  ∫⁻ (b : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)),
    f (↑b.2 • ↑b.1) ∂volume.toSphere.prod (Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1))f':Space d → ENNReal := fun x => f (‖x‖ • ‖x‖⁻¹ • x)x:↑{0}ᶜ| f (‖↑x‖ • ‖↑x‖⁻¹ • ↑x)
    change f' x.1d:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable fh0:∫⁻ (a : ↑{0}ᶜ),
    f
      (↑((homeomorphUnitSphereProd (Space d)) a).2 •
        ↑((homeomorphUnitSphereProd (Space d)) a).1) ∂Measure.comap Subtype.val volume =
  ∫⁻ (b : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)),
    f (↑b.2 • ↑b.1) ∂volume.toSphere.prod (Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1))f':Space d → ENNReal := fun x => f (‖x‖ • ‖x‖⁻¹ • x)x:↑{0}ᶜ| f' ↑x
  rw [MeasureTheory.lintegral_subtype_comap (byd:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable fh0:∫⁻ (a : ↑{0}ᶜ),
    f
      (↑((homeomorphUnitSphereProd (Space d)) a).2 •
        ↑((homeomorphUnitSphereProd (Space d)) a).1) ∂Measure.comap Subtype.val volume =
  ∫⁻ (b : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)),
    f (↑b.2 • ↑b.1) ∂volume.toSphere.prod (Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1))f':Space d → ENNReal := fun x => f (‖x‖ • ‖x‖⁻¹ • x)⊢ MeasurableSet {0}ᶜd:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable fh0:∫⁻ (a : ↑{0}ᶜ),
    f
      (↑((homeomorphUnitSphereProd (Space d)) a).2 •
        ↑((homeomorphUnitSphereProd (Space d)) a).1) ∂Measure.comap Subtype.val volume =
  ∫⁻ (b : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)),
    f (↑b.2 • ↑b.1) ∂volume.toSphere.prod (Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1))f':Space d → ENNReal := fun x => f (‖x‖ • ‖x‖⁻¹ • x)⊢ ∫⁻ (x : Space d), f x = ∫⁻ (x : Space d) in {0}ᶜ, f' x simpAll goals completed! 🐙d:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable fh0:∫⁻ (a : ↑{0}ᶜ),
    f
      (↑((homeomorphUnitSphereProd (Space d)) a).2 •
        ↑((homeomorphUnitSphereProd (Space d)) a).1) ∂Measure.comap Subtype.val volume =
  ∫⁻ (b : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)),
    f (↑b.2 • ↑b.1) ∂volume.toSphere.prod (Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1))f':Space d → ENNReal := fun x => f (‖x‖ • ‖x‖⁻¹ • x)⊢ ∫⁻ (x : Space d), f x = ∫⁻ (x : Space d) in {0}ᶜ, f' x)]d:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable fh0:∫⁻ (a : ↑{0}ᶜ),
    f
      (↑((homeomorphUnitSphereProd (Space d)) a).2 •
        ↑((homeomorphUnitSphereProd (Space d)) a).1) ∂Measure.comap Subtype.val volume =
  ∫⁻ (b : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)),
    f (↑b.2 • ↑b.1) ∂volume.toSphere.prod (Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1))f':Space d → ENNReal := fun x => f (‖x‖ • ‖x‖⁻¹ • x)⊢ ∫⁻ (x : Space d), f x = ∫⁻ (x : Space d) in {0}ᶜ, f' x
  simp [f']d:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable fh0:∫⁻ (a : ↑{0}ᶜ),
    f
      (↑((homeomorphUnitSphereProd (Space d)) a).2 •
        ↑((homeomorphUnitSphereProd (Space d)) a).1) ∂Measure.comap Subtype.val volume =
  ∫⁻ (b : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)),
    f (↑b.2 • ↑b.1) ∂volume.toSphere.prod (Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1))f':Space d → ENNReal := fun x => f (‖x‖ • ‖x‖⁻¹ • x)⊢ ∫⁻ (x : Space d), f x = ∫⁻ (x : Space d), f (‖x‖ • ‖x‖⁻¹ • x)
  refine lintegral_congr_ae ?_d:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable fh0:∫⁻ (a : ↑{0}ᶜ),
    f
      (↑((homeomorphUnitSphereProd (Space d)) a).2 •
        ↑((homeomorphUnitSphereProd (Space d)) a).1) ∂Measure.comap Subtype.val volume =
  ∫⁻ (b : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)),
    f (↑b.2 • ↑b.1) ∂volume.toSphere.prod (Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1))f':Space d → ENNReal := fun x => f (‖x‖ • ‖x‖⁻¹ • x)⊢ f =ᵐ[volume] fun x => f (‖x‖ • ‖x‖⁻¹ • x)
  filter_upwards [Measure.ae_ne volume 0] with x hxd:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable fh0:∫⁻ (a : ↑{0}ᶜ),
    f
      (↑((homeomorphUnitSphereProd (Space d)) a).2 •
        ↑((homeomorphUnitSphereProd (Space d)) a).1) ∂Measure.comap Subtype.val volume =
  ∫⁻ (b : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)),
    f (↑b.2 • ↑b.1) ∂volume.toSphere.prod (Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1))f':Space d → ENNReal := fun x => f (‖x‖ • ‖x‖⁻¹ • x)x:Space dhx:x ≠ 0⊢ f x = f (‖x‖ • ‖x‖⁻¹ • x)
  congrd:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable fh0:∫⁻ (a : ↑{0}ᶜ),
    f
      (↑((homeomorphUnitSphereProd (Space d)) a).2 •
        ↑((homeomorphUnitSphereProd (Space d)) a).1) ∂Measure.comap Subtype.val volume =
  ∫⁻ (b : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)),
    f (↑b.2 • ↑b.1) ∂volume.toSphere.prod (Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1))f':Space d → ENNReal := fun x => f (‖x‖ • ‖x‖⁻¹ • x)x:Space dhx:x ≠ 0⊢ x = ‖x‖ • ‖x‖⁻¹ • x
  simp [smul_smul]d:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable fh0:∫⁻ (a : ↑{0}ᶜ),
    f
      (↑((homeomorphUnitSphereProd (Space d)) a).2 •
        ↑((homeomorphUnitSphereProd (Space d)) a).1) ∂Measure.comap Subtype.val volume =
  ∫⁻ (b : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)),
    f (↑b.2 • ↑b.1) ∂volume.toSphere.prod (Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1))f':Space d → ENNReal := fun x => f (‖x‖ • ‖x‖⁻¹ • x)x:Space dhx:x ≠ 0⊢ x = (‖x‖ * ‖x‖⁻¹) • x
  have hx : ‖x‖ ≠ 0 := byd:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ ∫⁻ (x : Space d), f x =
  ∫⁻ (x : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)),
    f (↑x.2 • ↑x.1) ∂volume.toSphere.prod (Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1))d:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable fh0:∫⁻ (a : ↑{0}ᶜ),
    f
      (↑((homeomorphUnitSphereProd (Space d)) a).2 •
        ↑((homeomorphUnitSphereProd (Space d)) a).1) ∂Measure.comap Subtype.val volume =
  ∫⁻ (b : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)),
    f (↑b.2 • ↑b.1) ∂volume.toSphere.prod (Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1))f':Space d → ENNReal := fun x => f (‖x‖ • ‖x‖⁻¹ • x)x:Space dhx✝:x ≠ 0hx:‖x‖ ≠ 0⊢ x = (‖x‖ * ‖x‖⁻¹) • x
    simpa using hxd:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable fh0:∫⁻ (a : ↑{0}ᶜ),
    f
      (↑((homeomorphUnitSphereProd (Space d)) a).2 •
        ↑((homeomorphUnitSphereProd (Space d)) a).1) ∂Measure.comap Subtype.val volume =
  ∫⁻ (b : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)),
    f (↑b.2 • ↑b.1) ∂volume.toSphere.prod (Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1))f':Space d → ENNReal := fun x => f (‖x‖ • ‖x‖⁻¹ • x)x:Space dhx✝:x ≠ 0hx:‖x‖ ≠ 0⊢ x = (‖x‖ * ‖x‖⁻¹) • xd:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable fh0:∫⁻ (a : ↑{0}ᶜ),
    f
      (↑((homeomorphUnitSphereProd (Space d)) a).2 •
        ↑((homeomorphUnitSphereProd (Space d)) a).1) ∂Measure.comap Subtype.val volume =
  ∫⁻ (b : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)),
    f (↑b.2 • ↑b.1) ∂volume.toSphere.prod (Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1))f':Space d → ENNReal := fun x => f (‖x‖ • ‖x‖⁻¹ • x)x:Space dhx✝:x ≠ 0hx:‖x‖ ≠ 0⊢ x = (‖x‖ * ‖x‖⁻¹) • x
  field_simpd:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable fh0:∫⁻ (a : ↑{0}ᶜ),
    f
      (↑((homeomorphUnitSphereProd (Space d)) a).2 •
        ↑((homeomorphUnitSphereProd (Space d)) a).1) ∂Measure.comap Subtype.val volume =
  ∫⁻ (b : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)),
    f (↑b.2 • ↑b.1) ∂volume.toSphere.prod (Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1))f':Space d → ENNReal := fun x => f (‖x‖ • ‖x‖⁻¹ • x)x:Space dhx✝:x ≠ 0hx:‖x‖ ≠ 0⊢ x = 1 • x
  rw [one_smuld:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable fh0:∫⁻ (a : ↑{0}ᶜ),
    f
      (↑((homeomorphUnitSphereProd (Space d)) a).2 •
        ↑((homeomorphUnitSphereProd (Space d)) a).1) ∂Measure.comap Subtype.val volume =
  ∫⁻ (b : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)),
    f (↑b.2 • ↑b.1) ∂volume.toSphere.prod (Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1))f':Space d → ENNReal := fun x => f (‖x‖ • ‖x‖⁻¹ • x)x:Space dhx✝:x ≠ 0hx:‖x‖ ≠ 0⊢ x = xAll goals completed! 🐙]All goals completed! 🐙



lemma lintegral_volume_eq_spherical_mul (d : ℕ) [NeZero d]
    (f : Space d → ENNReal) (hf : Measurable f) :
    ∫⁻ x, f x ∂volume = ∫⁻ x, f (x.2.1 • x.1.1) * .ofReal (x.2.1 ^ (d - 1))
      ∂(volume (α := Space d).toSphere.prod (Measure.volumeIoiPow 0)) := byd:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ ∫⁻ (x : Space d), f x =
  ∫⁻ (x : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)),
    f (↑x.2 • ↑x.1) * ENNReal.ofReal (↑x.2 ^ (d - 1)) ∂volume.toSphere.prod (Measure.volumeIoiPow 0)
  rw [lintegral_volume_eq_spherical,d:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ ∫⁻ (x : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)),
    f (↑x.2 • ↑x.1) ∂volume.toSphere.prod (Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1)) =
  ∫⁻ (x : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)),
    f (↑x.2 • ↑x.1) * ENNReal.ofReal (↑x.2 ^ (d - 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⊢ ∫⁻ (a : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)),
    ((fun z => ENNReal.ofReal (↑z.2 ^ (Module.finrank ℝ (Space d) - 1))) * fun x => f (↑x.2 • ↑x.1))
      a ∂volume.toSphere.prod (Measure.comap Subtype.val volume) =
  ∫⁻ (a : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)),
    ((fun z => ENNReal.ofReal (↑z.2 ^ 0)) * fun x => f (↑x.2 • ↑x.1) * ENNReal.ofReal (↑x.2 ^ (d - 1)))
      a ∂volume.toSphere.prod (Measure.comap Subtype.val volume)h_mfd:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable fun z => ENNReal.ofReal (↑z.2 ^ 0)ad:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable fun x => f (↑x.2 • ↑x.1) * ENNReal.ofReal (↑x.2 ^ (d - 1))d:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable fun r => ENNReal.ofReal (↑r ^ 0)h_mfd:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable fun z => ENNReal.ofReal (↑z.2 ^ (Module.finrank ℝ (Space d) - 1))ad:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable fun x => f (↑x.2 • ↑x.1)d:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable fun r => ENNReal.ofReal (↑r ^ (Module.finrank ℝ (Space d) - 1))hfd:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable f Measure.volumeIoiPow,d:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ ∫⁻ (x : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)),
    f
      (↑x.2 •
        ↑x.1) ∂volume.toSphere.prod
      ((Measure.comap Subtype.val volume).withDensity fun r => ENNReal.ofReal (↑r ^ (Module.finrank ℝ (Space d) - 1))) =
  ∫⁻ (x : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)),
    f (↑x.2 • ↑x.1) * ENNReal.ofReal (↑x.2 ^ (d - 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⊢ ∫⁻ (a : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)),
    ((fun z => ENNReal.ofReal (↑z.2 ^ (Module.finrank ℝ (Space d) - 1))) * fun x => f (↑x.2 • ↑x.1))
      a ∂volume.toSphere.prod (Measure.comap Subtype.val volume) =
  ∫⁻ (a : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)),
    ((fun z => ENNReal.ofReal (↑z.2 ^ 0)) * fun x => f (↑x.2 • ↑x.1) * ENNReal.ofReal (↑x.2 ^ (d - 1)))
      a ∂volume.toSphere.prod (Measure.comap Subtype.val volume)h_mfd:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable fun z => ENNReal.ofReal (↑z.2 ^ 0)ad:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable fun x => f (↑x.2 • ↑x.1) * ENNReal.ofReal (↑x.2 ^ (d - 1))d:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable fun r => ENNReal.ofReal (↑r ^ 0)h_mfd:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable fun z => ENNReal.ofReal (↑z.2 ^ (Module.finrank ℝ (Space d) - 1))ad:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable fun x => f (↑x.2 • ↑x.1)d:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable fun r => ENNReal.ofReal (↑r ^ (Module.finrank ℝ (Space d) - 1))hfd:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable f
    MeasureTheory.prod_withDensity_right,d:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ (∫⁻ (x : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)),
    f
      (↑x.2 •
        ↑x.1) ∂(volume.toSphere.prod (Measure.comap Subtype.val volume)).withDensity fun z =>
      ENNReal.ofReal (↑z.2 ^ (Module.finrank ℝ (Space d) - 1))) =
  ∫⁻ (x : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)),
    f (↑x.2 • ↑x.1) * ENNReal.ofReal (↑x.2 ^ (d - 1)) ∂volume.toSphere.prod (Measure.volumeIoiPow 0)d:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable fun r => ENNReal.ofReal (↑r ^ (Module.finrank ℝ (Space d) - 1))hfd:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable fd:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ ∫⁻ (a : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)),
    ((fun z => ENNReal.ofReal (↑z.2 ^ (Module.finrank ℝ (Space d) - 1))) * fun x => f (↑x.2 • ↑x.1))
      a ∂volume.toSphere.prod (Measure.comap Subtype.val volume) =
  ∫⁻ (a : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)),
    ((fun z => ENNReal.ofReal (↑z.2 ^ 0)) * fun x => f (↑x.2 • ↑x.1) * ENNReal.ofReal (↑x.2 ^ (d - 1)))
      a ∂volume.toSphere.prod (Measure.comap Subtype.val volume)h_mfd:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable fun z => ENNReal.ofReal (↑z.2 ^ 0)ad:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable fun x => f (↑x.2 • ↑x.1) * ENNReal.ofReal (↑x.2 ^ (d - 1))d:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable fun r => ENNReal.ofReal (↑r ^ 0)h_mfd:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable fun z => ENNReal.ofReal (↑z.2 ^ (Module.finrank ℝ (Space d) - 1))ad:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable fun x => f (↑x.2 • ↑x.1)d:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable fun r => ENNReal.ofReal (↑r ^ (Module.finrank ℝ (Space d) - 1))hfd:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable f
    MeasureTheory.lintegral_withDensity_eq_lintegral_mul,d:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ ∫⁻ (a : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)),
    ((fun z => ENNReal.ofReal (↑z.2 ^ (Module.finrank ℝ (Space d) - 1))) * fun x => f (↑x.2 • ↑x.1))
      a ∂volume.toSphere.prod (Measure.comap Subtype.val volume) =
  ∫⁻ (x : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)),
    f (↑x.2 • ↑x.1) * ENNReal.ofReal (↑x.2 ^ (d - 1)) ∂volume.toSphere.prod (Measure.volumeIoiPow 0)h_mfd:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable fun z => ENNReal.ofReal (↑z.2 ^ (Module.finrank ℝ (Space d) - 1))ad:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable fun x => f (↑x.2 • ↑x.1)d:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable fun r => ENNReal.ofReal (↑r ^ (Module.finrank ℝ (Space d) - 1))hfd:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable fd:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ ∫⁻ (a : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)),
    ((fun z => ENNReal.ofReal (↑z.2 ^ (Module.finrank ℝ (Space d) - 1))) * fun x => f (↑x.2 • ↑x.1))
      a ∂volume.toSphere.prod (Measure.comap Subtype.val volume) =
  ∫⁻ (a : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)),
    ((fun z => ENNReal.ofReal (↑z.2 ^ 0)) * fun x => f (↑x.2 • ↑x.1) * ENNReal.ofReal (↑x.2 ^ (d - 1)))
      a ∂volume.toSphere.prod (Measure.comap Subtype.val volume)h_mfd:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable fun z => ENNReal.ofReal (↑z.2 ^ 0)ad:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable fun x => f (↑x.2 • ↑x.1) * ENNReal.ofReal (↑x.2 ^ (d - 1))d:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable fun r => ENNReal.ofReal (↑r ^ 0)h_mfd:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable fun z => ENNReal.ofReal (↑z.2 ^ (Module.finrank ℝ (Space d) - 1))ad:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable fun x => f (↑x.2 • ↑x.1)d:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable fun r => ENNReal.ofReal (↑r ^ (Module.finrank ℝ (Space d) - 1))hfd:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable f
    Measure.volumeIoiPow,d:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ ∫⁻ (a : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)),
    ((fun z => ENNReal.ofReal (↑z.2 ^ (Module.finrank ℝ (Space d) - 1))) * fun x => f (↑x.2 • ↑x.1))
      a ∂volume.toSphere.prod (Measure.comap Subtype.val volume) =
  ∫⁻ (x : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)),
    f (↑x.2 • ↑x.1) *
      ENNReal.ofReal
        (↑x.2 ^
          (d -
            1)) ∂volume.toSphere.prod ((Measure.comap Subtype.val volume).withDensity fun r => ENNReal.ofReal (↑r ^ 0))h_mfd:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable fun z => ENNReal.ofReal (↑z.2 ^ (Module.finrank ℝ (Space d) - 1))ad:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable fun x => f (↑x.2 • ↑x.1)d:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable fun r => ENNReal.ofReal (↑r ^ (Module.finrank ℝ (Space d) - 1))hfd:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable fd:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ ∫⁻ (a : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)),
    ((fun z => ENNReal.ofReal (↑z.2 ^ (Module.finrank ℝ (Space d) - 1))) * fun x => f (↑x.2 • ↑x.1))
      a ∂volume.toSphere.prod (Measure.comap Subtype.val volume) =
  ∫⁻ (a : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)),
    ((fun z => ENNReal.ofReal (↑z.2 ^ 0)) * fun x => f (↑x.2 • ↑x.1) * ENNReal.ofReal (↑x.2 ^ (d - 1)))
      a ∂volume.toSphere.prod (Measure.comap Subtype.val volume)h_mfd:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable fun z => ENNReal.ofReal (↑z.2 ^ 0)ad:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable fun x => f (↑x.2 • ↑x.1) * ENNReal.ofReal (↑x.2 ^ (d - 1))d:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable fun r => ENNReal.ofReal (↑r ^ 0)h_mfd:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable fun z => ENNReal.ofReal (↑z.2 ^ (Module.finrank ℝ (Space d) - 1))ad:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable fun x => f (↑x.2 • ↑x.1)d:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable fun r => ENNReal.ofReal (↑r ^ (Module.finrank ℝ (Space d) - 1))hfd:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable f MeasureTheory.prod_withDensity_right,d:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ ∫⁻ (a : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)),
    ((fun z => ENNReal.ofReal (↑z.2 ^ (Module.finrank ℝ (Space d) - 1))) * fun x => f (↑x.2 • ↑x.1))
      a ∂volume.toSphere.prod (Measure.comap Subtype.val volume) =
  ∫⁻ (x : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)),
    f (↑x.2 • ↑x.1) *
      ENNReal.ofReal
        (↑x.2 ^
          (d -
            1)) ∂(volume.toSphere.prod (Measure.comap Subtype.val volume)).withDensity fun z =>
      ENNReal.ofReal (↑z.2 ^ 0)d:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable fun r => ENNReal.ofReal (↑r ^ 0)h_mfd:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable fun z => ENNReal.ofReal (↑z.2 ^ (Module.finrank ℝ (Space d) - 1))ad:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable fun x => f (↑x.2 • ↑x.1)d:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable fun r => ENNReal.ofReal (↑r ^ (Module.finrank ℝ (Space d) - 1))hfd:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable fd:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ ∫⁻ (a : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)),
    ((fun z => ENNReal.ofReal (↑z.2 ^ (Module.finrank ℝ (Space d) - 1))) * fun x => f (↑x.2 • ↑x.1))
      a ∂volume.toSphere.prod (Measure.comap Subtype.val volume) =
  ∫⁻ (a : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)),
    ((fun z => ENNReal.ofReal (↑z.2 ^ 0)) * fun x => f (↑x.2 • ↑x.1) * ENNReal.ofReal (↑x.2 ^ (d - 1)))
      a ∂volume.toSphere.prod (Measure.comap Subtype.val volume)h_mfd:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable fun z => ENNReal.ofReal (↑z.2 ^ 0)ad:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable fun x => f (↑x.2 • ↑x.1) * ENNReal.ofReal (↑x.2 ^ (d - 1))d:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable fun r => ENNReal.ofReal (↑r ^ 0)h_mfd:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable fun z => ENNReal.ofReal (↑z.2 ^ (Module.finrank ℝ (Space d) - 1))ad:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable fun x => f (↑x.2 • ↑x.1)d:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable fun r => ENNReal.ofReal (↑r ^ (Module.finrank ℝ (Space d) - 1))hfd:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable f
    MeasureTheory.lintegral_withDensity_eq_lintegral_muld:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ ∫⁻ (a : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)),
    ((fun z => ENNReal.ofReal (↑z.2 ^ (Module.finrank ℝ (Space d) - 1))) * fun x => f (↑x.2 • ↑x.1))
      a ∂volume.toSphere.prod (Measure.comap Subtype.val volume) =
  ∫⁻ (a : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)),
    ((fun z => ENNReal.ofReal (↑z.2 ^ 0)) * fun x => f (↑x.2 • ↑x.1) * ENNReal.ofReal (↑x.2 ^ (d - 1)))
      a ∂volume.toSphere.prod (Measure.comap Subtype.val volume)h_mfd:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable fun z => ENNReal.ofReal (↑z.2 ^ 0)ad:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable fun x => f (↑x.2 • ↑x.1) * ENNReal.ofReal (↑x.2 ^ (d - 1))d:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable fun r => ENNReal.ofReal (↑r ^ 0)h_mfd:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable fun z => ENNReal.ofReal (↑z.2 ^ (Module.finrank ℝ (Space d) - 1))ad:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable fun x => f (↑x.2 • ↑x.1)d:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable fun r => ENNReal.ofReal (↑r ^ (Module.finrank ℝ (Space d) - 1))hfd:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable fd:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ ∫⁻ (a : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)),
    ((fun z => ENNReal.ofReal (↑z.2 ^ (Module.finrank ℝ (Space d) - 1))) * fun x => f (↑x.2 • ↑x.1))
      a ∂volume.toSphere.prod (Measure.comap Subtype.val volume) =
  ∫⁻ (a : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)),
    ((fun z => ENNReal.ofReal (↑z.2 ^ 0)) * fun x => f (↑x.2 • ↑x.1) * ENNReal.ofReal (↑x.2 ^ (d - 1)))
      a ∂volume.toSphere.prod (Measure.comap Subtype.val volume)h_mfd:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable fun z => ENNReal.ofReal (↑z.2 ^ 0)ad:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable fun x => f (↑x.2 • ↑x.1) * ENNReal.ofReal (↑x.2 ^ (d - 1))d:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable fun r => ENNReal.ofReal (↑r ^ 0)h_mfd:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable fun z => ENNReal.ofReal (↑z.2 ^ (Module.finrank ℝ (Space d) - 1))ad:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable fun x => f (↑x.2 • ↑x.1)d:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable fun r => ENNReal.ofReal (↑r ^ (Module.finrank ℝ (Space d) - 1))hfd:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable f]d:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ ∫⁻ (a : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)),
    ((fun z => ENNReal.ofReal (↑z.2 ^ (Module.finrank ℝ (Space d) - 1))) * fun x => f (↑x.2 • ↑x.1))
      a ∂volume.toSphere.prod (Measure.comap Subtype.val volume) =
  ∫⁻ (a : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)),
    ((fun z => ENNReal.ofReal (↑z.2 ^ 0)) * fun x => f (↑x.2 • ↑x.1) * ENNReal.ofReal (↑x.2 ^ (d - 1)))
      a ∂volume.toSphere.prod (Measure.comap Subtype.val volume)h_mfd:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable fun z => ENNReal.ofReal (↑z.2 ^ 0)ad:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable fun x => f (↑x.2 • ↑x.1) * ENNReal.ofReal (↑x.2 ^ (d - 1))d:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable fun r => ENNReal.ofReal (↑r ^ 0)h_mfd:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable fun z => ENNReal.ofReal (↑z.2 ^ (Module.finrank ℝ (Space d) - 1))ad:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable fun x => f (↑x.2 • ↑x.1)d:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable fun r => ENNReal.ofReal (↑r ^ (Module.finrank ℝ (Space d) - 1))hfd:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ Measurable f
  ·d:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ ∫⁻ (a : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)),
    ((fun z => ENNReal.ofReal (↑z.2 ^ (Module.finrank ℝ (Space d) - 1))) * fun x => f (↑x.2 • ↑x.1))
      a ∂volume.toSphere.prod (Measure.comap Subtype.val volume) =
  ∫⁻ (a : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)),
    ((fun z => ENNReal.ofReal (↑z.2 ^ 0)) * fun x => f (↑x.2 • ↑x.1) * ENNReal.ofReal (↑x.2 ^ (d - 1)))
      a ∂volume.toSphere.prod (Measure.comap Subtype.val volume) refine lintegral_congr_ae ?_d:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ ((fun z => ENNReal.ofReal (↑z.2 ^ (Module.finrank ℝ (Space d) - 1))) * fun x =>
    f (↑x.2 • ↑x.1)) =ᵐ[volume.toSphere.prod (Measure.comap Subtype.val volume)]
  (fun z => ENNReal.ofReal (↑z.2 ^ 0)) * fun x => f (↑x.2 • ↑x.1) * ENNReal.ofReal (↑x.2 ^ (d - 1))
    simp only [finrank_eq_dim, pow_zero, ENNReal.ofReal_one]d:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable f⊢ ((fun z => ENNReal.ofReal (↑z.2 ^ (d - 1))) * fun x =>
    f (↑x.2 • ↑x.1)) =ᵐ[volume.toSphere.prod (Measure.comap Subtype.val volume)]
  (fun z => 1) * fun x => f (↑x.2 • ↑x.1) * ENNReal.ofReal (↑x.2 ^ (d - 1))
    filter_upwards with xd:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable fx:↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)⊢ ((fun z => ENNReal.ofReal (↑z.2 ^ (d - 1))) * fun x => f (↑x.2 • ↑x.1)) x =
  ((fun z => 1) * fun x => f (↑x.2 • ↑x.1) * ENNReal.ofReal (↑x.2 ^ (d - 1))) x
    simp only [Pi.mul_apply, one_mul]d:ℕinst✝:NeZero df:Space d → ENNRealhf:Measurable fx:↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)⊢ ENNReal.ofReal (↑x.2 ^ (d - 1)) * f (↑x.2 • ↑x.1) = f (↑x.2 • ↑x.1) * ENNReal.ofReal (↑x.2 ^ (d - 1))
    ringAll goals completed! 🐙
  all_goals fun_propAll goals completed! 🐙