Skip to content

refactor: replace d.succ with d (1 of 2) #1183

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
zhikaip merged 1 commit into from
Jun 15, 2026
+107 −147
Merged

refactor: replace d.succ with d (1 of 2) #1183

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions Physlib/ClassicalMechanics/RigidBody/SolidSphere.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -51,8 +51,8 @@ lemma solidSphere_mass {d : ℕ} (m R : ℝ≥0) (hr : R ≠ 0) : (solidSphere d
have h1 : (@volume (Space d.succ) measureSpaceOfInnerProductSpace).real
(Metric.closedBall 0 R) ≠ 0 := by
refine (measureReal_ne_zero_iff ?_).mpr ?_
· apply Space.volume_closedBall_ne_top
· apply Space.volume_closedBall_ne_zero
· apply measure_closedBall_lt_top.ne
· apply (Metric.measure_closedBall_pos volume _ _).ne'
have hr' := R.2
have hx : R.1 ≠ 0 := by simpa using hr
apply lt_of_le_of_ne hr' (Ne.symm hx)
Expand Down
4 changes: 2 additions & 2 deletions Physlib/Electromagnetism/Current/InfiniteWire.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -117,7 +117,7 @@ noncomputable def infiniteWire (𝓕 : FreeSpace) (I : ℝ) :
constantSliceDist 0
((- I * 𝓕.μ₀ / (2 * Real.pi)) • distOfFunction (fun (x : Space 2) =>
Real.log ‖x‖ • Lorentz.Vector.basis (Sum.inr 0))
(IsDistBounded.log_norm.smul_const _))
((IsDistBounded.log_norm (by norm_num)).smul_const _))

/-!

Expand Down Expand Up @@ -155,7 +155,7 @@ lemma infiniteWire_vectorPotential (𝓕 : FreeSpace) (I : ℝ) :
constantSliceDist 0
((- I * 𝓕.μ₀ / (2 * Real.pi)) • distOfFunction (fun (x : Space 2) =>
Real.log ‖x‖ • EuclideanSpace.single 0 (1 : ℝ))
(by apply IsDistBounded.log_norm.smul_const))) := by
(by apply (IsDistBounded.log_norm (by norm_num)).smul_const))) := by
ext η i
simp [vectorPotential, infiniteWire, constantTime_apply,
constantSliceDist_apply, Lorentz.Vector.spatialCLM, distOfFunction_vector_eval,
Expand Down
5 changes: 2 additions & 3 deletions Physlib/Electromagnetism/PointParticle/ThreeDimension.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -157,7 +157,7 @@ lemma threeDimPointParticle_eq_distTranslate (𝓕 : FreeSpace) (q : ℝ) (r₀
distTranslate (basis.repr r₀) <|
distOfFunction (fun x => (((q * 𝓕.μ₀ * 𝓕.c)/ (4 * π))* ‖x‖⁻¹) •
Lorentz.Vector.basis (Sum.inl 0))
((IsDistBounded.inv.const_mul_fun _).smul_const _)) := by
(((IsDistBounded.inv (by norm_num)).const_mul_fun _).smul_const _)) := by
rw [threeDimPointParticle]
congr
ext η
Expand Down Expand Up @@ -187,8 +187,7 @@ lemma threeDimPointParticle_scalarPotential (𝓕 : FreeSpace) (q : ℝ) (r₀ :
Lorentz.Vector.basis_apply, ↓reduceIte, mul_one, smul_eq_mul]
rw [distOfFunction_mul_fun _ (IsDistBounded.inv_shift _),
distOfFunction_mul_fun _ (IsDistBounded.inv_shift _)]
simp only [Nat.succ_eq_add_one, Nat.reduceAdd, ContinuousLinearMap.coe_smul', Pi.smul_apply,
smul_eq_mul]
simp only [ContinuousLinearMap.coe_smul', Pi.smul_apply, smul_eq_mul]
ring_nf
simp only [𝓕.c_sq, one_div, mul_inv_rev, mul_eq_mul_right_iff, inv_eq_zero, OfNat.ofNat_ne_zero,
or_false]
Expand Down
14 changes: 6 additions & 8 deletions Physlib/QuantumMechanics/DDimensions/Operators/Position.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -220,7 +220,7 @@ lemma radiusPowLM_apply_memHS {d : ℕ} (s : ℝ) (ψ : 𝓢(Space d, ℂ)) (a :
MemHS (𝐫 s ψ) := by
rcases Nat.eq_zero_or_pos d with (rfl | hd)
· simp only [MemHS, MemLp.of_discrete]
· have : Nontrivial (Space d) := Nat.succ_pred_eq_of_pos hd ▸ Space.instNontrivialSucc
· have : NeZero d := ⟨hd.ne'⟩
refine (memLp_two_iff_integrable_sq_norm (by fun_prop)).mpr ⟨by fun_prop, ?_⟩
suffices ∫⁻ (x : Space d), ‖‖ψ x‖ ^ 2 * ‖x‖ ^ (2 * s)‖ₑ < ⊤ by
have hInt (x : Space d) : ‖𝐫 s ψ x‖ ^ 2 = ‖ψ x‖ ^ 2 * ‖x‖ ^ (2 * s) := by
Expand All @@ -237,7 +237,7 @@ lemma radiusPowLM_apply_memHS {d : ℕ} (s : ℝ) (ψ : 𝓢(Space d, ℂ)) (a :
_ = ‖C ^ 2‖ₑ * ∫⁻ (x : Space d) in (Metric.ball 0 1), ‖‖x‖ ^ (2 * (a + s))‖ₑ :=
lintegral_const_mul _ (by fun_prop)
apply ENNReal.mul_lt_top enorm_lt_top
exact ((integrableOn_norm_rpow_ball_iff hd Real.zero_lt_one _).mpr h).hasFiniteIntegral
exact ((integrableOn_norm_rpow_ball_iff Real.zero_lt_one _).mpr h).hasFiniteIntegral
apply ae_iff.mpr
refine measure_mono_null ?_ (measure_singleton 0)
intro x hx
Expand Down Expand Up @@ -265,7 +265,7 @@ lemma radiusPowLM_apply_memHS {d : ℕ} (s : ℝ) (ψ : 𝓢(Space d, ℂ)) (a :
lintegral_const_mul _ (by fun_prop)
apply ENNReal.mul_lt_top enorm_lt_top
have hd' : (d + -2 * d : ℝ) < 0 := by simp [hd]
exact ((integrableOn_norm_rpow_ball_compl_iff hd zero_lt_one _).mpr hd').hasFiniteIntegral
exact ((integrableOn_norm_rpow_ball_compl_iff zero_lt_one _).mpr hd').hasFiniteIntegral
intro x hx
simp only [Set.mem_compl_iff, Metric.mem_ball, dist_zero_right, not_lt] at hx
simp_rw [← enorm_mul, enorm_le_iff_norm_le, norm_mul, norm_pow, Real.norm_eq_abs, sq_abs,
Expand Down Expand Up @@ -336,26 +336,24 @@ lemma radiusRegPow_tendsto_radiusPow' {d : ℕ} (s : ℝ) (ψ : 𝓢(Space d,
· exact radiusRegPow_tendsto_radiusPow s ψ hx.ne

/-- a.e. version of `radiusRegPow_tendsto_radiusPow` -/
lemma radiusRegPow_ae_tendsto_radiusPow {d : ℕ} (hd : 0 < d) (s : ℝ) (ψ : 𝓢(Space d, ℂ)) :
lemma radiusRegPow_ae_tendsto_radiusPow {d : ℕ} [NeZero d] (s : ℝ) (ψ : 𝓢(Space d, ℂ)) :
∀ᵐ x, Tendsto (fun ε ↦ 𝐫₀ ε s ψ x) nhdsZeroUnits (nhds (𝐫 s ψ x)) := by
apply ae_iff.mpr
suffices h : {x | ¬Tendsto (fun ε ↦ 𝐫₀ ε s ψ x) nhdsZeroUnits (nhds (𝐫 s ψ x))} ⊆ {0} by
rcases Set.subset_singleton_iff_eq.mp h with (h' | h')
· exact h' ▸ measure_empty
· have : Nontrivial (Space d) := Nat.succ_pred_eq_of_pos hd ▸ Space.instNontrivialSucc
exact h' ▸ measure_singleton 0
· exact h' ▸ measure_singleton 0
intro x hx
by_contra hx'
exact hx <| radiusRegPow_tendsto_radiusPow s ψ hx'

lemma radiusRegPow_ae_tendsto_iff {d : ℕ} (hd : 0 < d) {s : ℝ} {ψ : 𝓢(Space d, ℂ)}
lemma radiusRegPow_ae_tendsto_iff {d : ℕ} [NeZero d] {s : ℝ} {ψ : 𝓢(Space d, ℂ)}
{φ : Space d → ℂ} : (∀ᵐ x, Tendsto (fun ε ↦ 𝐫₀ ε s ψ x) nhdsZeroUnits (nhds (φ x)))
↔ φ =ᵐ[volume] 𝐫 s ψ := by
let t₁ := {x | ¬Tendsto (fun ε ↦ 𝐫₀ ε s ψ x) nhdsZeroUnits (nhds (φ x))}
let t₂ := {x | φ x ≠ 𝐫 s ψ x}
show volume t₁ = 0 ↔ volume t₂ = 0
suffices heq : t₁ ∪ {0} = t₂ ∪ {0} by
have : Nontrivial (Space d) := Nat.succ_pred_eq_of_pos hd ▸ Space.instNontrivialSucc
have hUnion : ∀ t : Set (Space d), volume t = 0 ↔ volume (t ∪ {0}) = 0 :=
fun _ ↦ by simp only [measure_union_null_iff, measure_singleton, and_true]
rw [hUnion t₁, hUnion t₂, heq]
Expand Down
2 changes: 1 addition & 1 deletion Physlib/QuantumMechanics/DDimensions/SpaceDHilbertSpace/PolyBddSchwartzSubmodule.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -255,7 +255,7 @@ lemma dense_top (d : ℕ) : Dense (polyBddSchwartzSubmodule d ⊤ : Set (SpaceDH
have hξ := L2.eLpNorm_rpow_two_norm_lt_top ξ
simp_rw [eLpNorm_one_eq_lintegral_enorm, Real.rpow_ofNat, enorm_pow, enorm_norm] at hξ
exact hξ
· have : Nontrivial (Space d) := Nat.succ_pred_eq_of_pos hd ▸ Space.instNontrivialSucc
· have : NeZero d := ⟨hd.ne'⟩
let C : ℝ := (ENNReal.ofReal (√Real.pi ^ d / Real.Gamma (d / 2 + 1))).toReal
have hvolB : ⇑volume ∘ B = fun n ↦ ENNReal.ofReal (C * (b n).rOut ^ d) := by
ext n
Expand Down
6 changes: 3 additions & 3 deletions Physlib/SpaceAndTime/Space/Basic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -240,12 +240,12 @@ noncomputable instance {d} : MetricSpace (Space d) where

-/

instance {d : ℕ} : Nontrivial (Space d.succ) where
instance instNontrivial {d : ℕ} [NeZero d] : Nontrivial (Space d) where
exists_pair_ne := by
obtain k := Classical.choice Space.instNonempty
obtain ⟨v1, hv⟩ := exists_ne (0 : EuclideanSpace ℝ (Fin d.succ))
obtain ⟨v1, hv⟩ := exists_ne (0 : EuclideanSpace ℝ (Fin d))
use k, v1 +ᵥ k
simpa only [ne_eq, eq_vadd_iff_vsub_eq, vsub_self] using hv.symm
simpa [ne_eq, eq_vadd_iff_vsub_eq, vsub_self] using hv.symm

/-!

Expand Down
127 changes: 46 additions & 81 deletions Physlib/SpaceAndTime/Space/Integrals/Basic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -21,10 +21,10 @@ We focus here on the volume measure, which is the usual measure on `Space d`, i.

- `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.succ` with
- `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.succ`
- `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.

Expand All @@ -45,40 +45,6 @@ open InnerProductSpace MeasureTheory
lemma volume_eq_addHaar {d} : (volume (α := Space d)) = Space.basis.toBasis.addHaar := by
exact (OrthonormalBasis.addHaar_eq_volume _).symm

lemma volume_closedBall_ne_zero {d : ℕ} (x : Space d.succ) {r : ℝ} (hr : 0 < r) :

@morrison-daniel morrison-daniel Jun 14, 2026

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why is this and the next one removed? Are they redundant now?

@zhikaip zhikaip Jun 14, 2026 •
edited
Loading

Copy link
Copy Markdown
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

oops I probably should've split this off as they are unrelated to this refactor, but (nevermind I remembered I was checking because they were also stated with d.succ)

basically I found out that they are one-liners with what's already in Mathlib and I don't feel they're necessary, i.e.

lemma volume_closedBall_ne_zero {d : ℕ} (x : Space d.succ) {r : ℝ} (hr : 0 < r) :
    volume (Metric.closedBall x r) ≠ 0 := by
  apply (Metric.measure_closedBall_pos volume _ hr).ne'

lemma volume_closedBall_ne_top {d : ℕ} (x : Space d.succ) (r : ℝ) :
    volume (Metric.closedBall x r) ≠ ⊤ := by
  apply measure_closedBall_lt_top.ne

These only affect the changes in Physlib/ClassicalMechanics/RigidBody/SolidSphere.lean (at the very beginning of the diff page).

@zhikaip zhikaip Jun 14, 2026

Copy link
Copy Markdown
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Updated PR summary to document this change as well

@morrison-daniel morrison-daniel Jun 15, 2026

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ah makes sense!

volume (Metric.closedBall x r) ≠ 0 := by
obtain ⟨k,hk⟩ := Nat.even_or_odd' d.succ
rcases hk with hk | hk
· rw [InnerProductSpace.volume_closedBall_of_dim_even (k := k)]
simp only [Nat.succ_eq_add_one, finrank_eq_dim, ne_eq, mul_eq_zero, Nat.add_eq_zero_iff,
one_ne_zero, and_false, not_false_eq_true, pow_eq_zero_iff, ENNReal.ofReal_eq_zero, not_or,
not_le]
apply And.intro
· simp_all
· positivity
· simpa using hk
· rw [InnerProductSpace.volume_closedBall_of_dim_odd (k := k)]
simp only [Nat.succ_eq_add_one, finrank_eq_dim, ne_eq, mul_eq_zero, Nat.add_eq_zero_iff,
one_ne_zero, and_false, not_false_eq_true, pow_eq_zero_iff, ENNReal.ofReal_eq_zero, not_or,
not_le]
apply And.intro
· simp_all
· positivity
· simpa using hk

lemma volume_closedBall_ne_top {d : ℕ} (x : Space d.succ) (r : ℝ) :
volume (Metric.closedBall x r) ≠ ⊤ := by
obtain ⟨k,hk⟩ := Nat.even_or_odd' d.succ
rcases hk with hk | hk
· rw [InnerProductSpace.volume_closedBall_of_dim_even (by simpa using hk)]
simp only [Nat.succ_eq_add_one, finrank_eq_dim, ne_eq]
apply not_eq_of_beq_eq_false
rfl
· rw [InnerProductSpace.volume_closedBall_of_dim_odd (by simpa using hk)]
simp only [Nat.succ_eq_add_one, finrank_eq_dim, ne_eq]
apply not_eq_of_beq_eq_false
rfl

@[simp]
lemma volume_metricBall_three :
volume (Metric.ball (0 : Space 3) 1) = ENNReal.ofReal (4 / 3 * Real.pi) := by
Expand Down Expand Up @@ -128,24 +94,23 @@ lemma integral_one_dim_eq_integral_real {f : Space 1 → ℝ} :

-/

lemma integral_volume_eq_spherical (d : ℕ) (f : Space d.succ → F)
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.succ).toSphere.prod
(Measure.volumeIoiPow (Module.finrank ℝ (Space d.succ) - 1))) := by
∫ x, f x ∂volume = ∫ x, f (x.2.1 • x.1.1) ∂(volume (α := Space d).toSphere.prod
(Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1))) := by
rw [← MeasureTheory.MeasurePreserving.integral_comp (f := homeomorphUnitSphereProd _)
(MeasureTheory.Measure.measurePreserving_homeomorphUnitSphereProd
(volume (α := Space d.succ)))
(Homeomorph.measurableEmbedding (homeomorphUnitSphereProd (Space d.succ)))]
simp only [Nat.succ_eq_add_one, homeomorphUnitSphereProd_apply_snd_coe,
homeomorphUnitSphereProd_apply_fst_coe]
let f' : (x : (Space d.succ)) → F := fun x => f (‖↑x‖ • ‖↑x‖⁻¹ • ↑x)
(volume (α := Space d)))
(Homeomorph.measurableEmbedding (homeomorphUnitSphereProd (Space d)))]
simp only [homeomorphUnitSphereProd_apply_snd_coe, homeomorphUnitSphereProd_apply_fst_coe]
let f' : (x : (Space d)) → F := fun x => f (‖↑x‖ • ‖↑x‖⁻¹ • ↑x)
conv_rhs =>
enter [2, x]
change f' x.1
rw [MeasureTheory.integral_subtype_comap (by simp), ← setIntegral_univ]
simp [f']
refine integral_congr_ae ?_
have h1 : ∀ᵐ x ∂(volume (α := Space d.succ)), x ≠ 0 := by
have h1 : ∀ᵐ x ∂(volume (α := Space d)), x ≠ 0 := by
exact Measure.ae_ne volume 0
filter_upwards [Measure.ae_ne volume 0] with x hx
congr
Expand All @@ -156,14 +121,14 @@ lemma integral_volume_eq_spherical (d : ℕ) (f : Space d.succ → F)
simp

lemma integrable_spherical_of_integrable {d : ℕ} {F : Type*}
[NormedAddCommGroup F] [NormedSpace ℝ F] {f : Space d.succ → F}
[NormedAddCommGroup F] [NormedSpace ℝ F] {f : Space d → F}
(hf : Integrable f volume) :
Integrable
(fun x : ↑(Metric.sphere (0 : Space d.succ) 1) × Set.Ioi (0 : ℝ) =>
(fun x : ↑(Metric.sphere (0 : Space d) 1) × Set.Ioi (0 : ℝ) =>
f (x.2.1 • x.1.1))
(volume (α := Space d.succ).toSphere.prod
(Measure.volumeIoiPow (Module.finrank ℝ (Space d.succ) - 1))) := by
let s : Set (Space d.succ) := {0}ᶜ
(volume (α := Space d).toSphere.prod
(Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1))) := by
let s : Set (Space d) := {0}ᶜ
have h1 : Integrable (fun x : s => f x.1)
(.comap (Subtype.val (p := fun x => x ∈ s)) volume) := by
change Integrable (f ∘ Subtype.val)
Expand All @@ -172,26 +137,26 @@ lemma integrable_spherical_of_integrable {d : ℕ} {F : Type*}
· exact hf.integrableOn
· simp [s]
have he := MeasureTheory.Measure.measurePreserving_homeomorphUnitSphereProd
(volume (α := Space d.succ))
(volume (α := Space d))
have hcomp :
Integrable
((fun x : s => f x.1) ∘ (homeomorphUnitSphereProd (Space d.succ)).symm)
(volume (α := Space d.succ).toSphere.prod
(Measure.volumeIoiPow (Module.finrank ℝ (Space d.succ) - 1))) := by
((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_emb]
· convert h1
simp only [Nat.succ_eq_add_one, Function.comp_apply, Homeomorph.symm_apply_apply]
· exact Homeomorph.measurableEmbedding (homeomorphUnitSphereProd (Space d.succ))
simp only [Function.comp_apply, Homeomorph.symm_apply_apply]
· exact Homeomorph.measurableEmbedding (homeomorphUnitSphereProd (Space d))
convert hcomp using 1

lemma integral_volume_eq_spherical_iterated {d : ℕ} {F : Type*}
[NormedAddCommGroup F] [NormedSpace ℝ F] (f : Space d.succ → F)
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.succ, f x =
∫ n : ↑(Metric.sphere (0 : Space d.succ) 1),
∫ 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.succ) - 1))
∂(volume (α := Space d.succ).toSphere) := by
∂(Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1))
∂(volume (α := Space d).toSphere) := by
rw [integral_volume_eq_spherical]
rw [MeasureTheory.integral_prod]
exact integrable_spherical_of_integrable hf
Expand Down Expand Up @@ -226,14 +191,14 @@ instance : SFinite (@Measure.comap ↑(Set.Ioi 0) ℝ Subtype.instMeasurableSpac
apply MeasurableEmbedding.subtype_coe
simp

lemma integral_volume_eq_spherical_integral {d : ℕ} {F : Type*}
[NormedAddCommGroup F] [NormedSpace ℝ F] (f : Space d.succ → F)
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.succ, f x =
∫ n : ↑(Metric.sphere (0 : Space d.succ) 1),
∫ r : Set.Ioi (0 : ℝ), (r.1 ^ d) • f (r.1 • n.1)
∫ 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.succ).toSphere) := by
∂(volume (α := Space d).toSphere) := by
rw [integral_volume_eq_spherical_iterated f hf]
congr
funext n
Expand All @@ -242,26 +207,26 @@ lemma integral_volume_eq_spherical_integral {d : ℕ} {F : Type*}
congr
funext r
have hr : 0 ≤ (r : ℝ) := le_of_lt r.2
rw [NNReal.smul_def, Real.coe_toNNReal _ (pow_nonneg hr d)]
rw [NNReal.smul_def, Real.coe_toNNReal _ (pow_nonneg hr (d - 1))]

/-!

## D. Lower Lebesgue integral over volume to spherical

-/

lemma lintegral_volume_eq_spherical (d : ℕ) (f : Space d.succ → ENNReal) (hf : Measurable f) :
∫⁻ x, f x ∂volume = ∫⁻ x, f (x.2.1 • x.1.1) ∂(volume (α := Space d.succ).toSphere.prod
(Measure.volumeIoiPow (Module.finrank ℝ (Space d.succ) - 1))) := by
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))) := by
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.succ)))
(volume (α := Space d)))
(by fun_prop)
rw [← h0]
simp only [Nat.succ_eq_add_one, homeomorphUnitSphereProd_apply_snd_coe,
homeomorphUnitSphereProd_apply_fst_coe]
let f' : (x : (Space d.succ)) → ENNReal := fun x => f (‖↑x‖ • ‖↑x‖⁻¹ • ↑x)
simp only [homeomorphUnitSphereProd_apply_snd_coe, homeomorphUnitSphereProd_apply_fst_coe]
let f' : (x : (Space d)) → ENNReal := fun x => f (‖↑x‖ • ‖↑x‖⁻¹ • ↑x)
conv_rhs =>
enter [2, x]
change f' x.1
Expand All @@ -276,17 +241,17 @@ lemma lintegral_volume_eq_spherical (d : ℕ) (f : Space d.succ → ENNReal) (hf
field_simp
rw [one_smul]

lemma lintegral_volume_eq_spherical_mul (d : ℕ) (f : Space d.succ → ENNReal) (hf : Measurable f) :
∫⁻ x, f x ∂volume = ∫⁻ x, f (x.2.1 • x.1.1) * .ofReal (x.2.1 ^ d)
∂(volume (α := Space d.succ).toSphere.prod (Measure.volumeIoiPow 0)) := by
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)) := by
rw [lintegral_volume_eq_spherical, Measure.volumeIoiPow,
MeasureTheory.prod_withDensity_right,
MeasureTheory.lintegral_withDensity_eq_lintegral_mul,
Measure.volumeIoiPow, MeasureTheory.prod_withDensity_right,
MeasureTheory.lintegral_withDensity_eq_lintegral_mul]
· refine lintegral_congr_ae ?_
simp only [Nat.succ_eq_add_one, finrank_eq_dim, add_tsub_cancel_right, pow_zero,
ENNReal.ofReal_one]
simp only [finrank_eq_dim, pow_zero, ENNReal.ofReal_one]
filter_upwards with x
simp only [Pi.mul_apply, one_mul]
ring
Expand Down
Loading
Loading