diff --git a/PhysLean/SpaceAndTime/Space/Basic.lean b/PhysLean/SpaceAndTime/Space/Basic.lean index cd0dc7d9..223176f6 100644 --- a/PhysLean/SpaceAndTime/Space/Basic.lean +++ b/PhysLean/SpaceAndTime/Space/Basic.lean @@ -484,6 +484,10 @@ lemma basis_inner {d} (i : Fin d) (p : Space d) : inner ℝ (basis i) p = p i := by simp [inner_eq_sum, basis_apply] +lemma norm_basis_repr_apply {d} (p : Space d) : + ‖basis.repr p‖ = ‖p‖ := by + simp [basis, norm_eq, PiLp.norm_eq_of_L2] + open InnerProductSpace lemma basis_repr_inner_eq {d} (p : Space d) (v : EuclideanSpace ℝ (Fin d)) : @@ -712,6 +716,10 @@ lemma oneEquiv_measurePreserving : MeasurePreserving oneEquiv volume volume := lemma oneEquiv_symm_measurePreserving : MeasurePreserving oneEquiv.symm volume volume := by exact LinearIsometryEquiv.measurePreserving oneEquiv.symm + +lemma integral_one_dim_eq_integral_real {f : Space 1 → ℝ} : + ∫ x, f x ∂volume = ∫ x, f (oneEquiv.symm x) ∂volume := by rw [integral_comp] + lemma volume_eq_addHaar {d} : (volume (α := Space d)) = Space.basis.toBasis.addHaar := by exact (OrthonormalBasis.addHaar_eq_volume _).symm @@ -791,4 +799,112 @@ lemma volume_metricBall_two_real : simp only [ENNReal.toReal_ofReal_eq_iff] exact Real.pi_nonneg +@[simp] +lemma volume_metricBall_three_real : + (volume.real (Metric.ball (0 : Space 3) 1)) = 4 / 3 * Real.pi := by + trans (volume (Metric.ball (0 : Space 3) 1)).toReal + · rfl + rw [volume_metricBall_three] + simp only [ENNReal.toReal_ofReal_eq_iff] + positivity + +lemma integral_volume_eq_spherical (d : ℕ) (f : Space d.succ → 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 + rw [← MeasureTheory.MeasurePreserving.integral_comp (f := homeomorphUnitSphereProd _) + (MeasureTheory.Measure.measurePreserving_homeomorphUnitSphereProd + (volume (α := Space d.succ))) + (Homeomorph.measurableEmbedding (homeomorphUnitSphereProd (Space d.succ)))] + simp + let f' : (x : (Space d.succ)) → 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 + exact Measure.ae_ne volume 0 + filter_upwards [Measure.ae_ne volume 0] with x hx + congr + simp [smul_smul] + have hx : ‖x‖ ≠ 0 := by + simpa using hx + field_simp + simp + +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 + 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))) + (by fun_prop) + rw [← h0] + simp + let f' : (x : (Space d.succ)) → ENNReal := fun x => f (‖↑x‖ • ‖↑x‖⁻¹ • ↑x) + conv_rhs => + enter [2, x] + change f' x.1 + rw [MeasureTheory.lintegral_subtype_comap] + simp [f'] + refine lintegral_congr_ae ?_ + filter_upwards [Measure.ae_ne volume 0] with x hx + congr + simp [smul_smul] + have hx : ‖x‖ ≠ 0 := by + simpa using hx + field_simp + simp + simp + +instance sfinite : SFinite (@Measure.comap ↑(Set.Ioi 0) ℝ Subtype.instMeasurableSpace + Real.measureSpace.toMeasurableSpace Subtype.val volume) := by + refine { out' := ?_ } + have h1 := SFinite.out' (μ := volume (α := ℝ)) + obtain ⟨m, h⟩ := h1 + use fun n => Measure.comap Subtype.val (m n) + apply And.intro + · intro n + refine (isFiniteMeasure_iff (Measure.comap Subtype.val (m n))).mpr ?_ + rw [MeasurableEmbedding.comap_apply] + simp only [Set.image_univ, Subtype.range_coe_subtype, Set.mem_Ioi] + have hm := h.1 n + exact measure_lt_top (m n) {x | 0 < x} + exact MeasurableEmbedding.subtype_coe measurableSet_Ioi + · ext s hs + rw [MeasurableEmbedding.comap_apply, Measure.sum_apply] + conv_rhs => + enter [1, i] + rw [MeasurableEmbedding.comap_apply (MeasurableEmbedding.subtype_coe measurableSet_Ioi)] + have h2 := h.2 + rw [Measure.ext_iff'] at h2 + rw [← Measure.sum_apply] + exact h2 (Subtype.val '' s) + refine MeasurableSet.subtype_image measurableSet_Ioi hs + exact hs + + apply MeasurableEmbedding.subtype_coe + simp +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 + rw [lintegral_volume_eq_spherical] + rw [Measure.volumeIoiPow, MeasureTheory.prod_withDensity_right, + MeasureTheory.lintegral_withDensity_eq_lintegral_mul ] + rw [Measure.volumeIoiPow, MeasureTheory.prod_withDensity_right, + MeasureTheory.lintegral_withDensity_eq_lintegral_mul ] + · refine lintegral_congr_ae ?_ + simp + filter_upwards with x + simp + ring + all_goals + · fun_prop + + + end Space diff --git a/PhysLean/SpaceAndTime/Space/Derivatives/Grad.lean b/PhysLean/SpaceAndTime/Space/Derivatives/Grad.lean index 6eae8e3a..180d00b0 100644 --- a/PhysLean/SpaceAndTime/Space/Derivatives/Grad.lean +++ b/PhysLean/SpaceAndTime/Space/Derivatives/Grad.lean @@ -498,4 +498,43 @@ lemma distGrad_apply {d} (f : (Space d) →d[ℝ] ℝ) (ε : 𝓢(Space d, ℝ)) change (distGrad f).toFun ε = fun i => distDeriv i f ε rw [distGrad_toFun_eq_distDeriv] +/-! + +### The gradident of a Schwartz map + +-/ + +noncomputable def gradSchwartz {d} (η : 𝓢(Space d, ℝ)) : 𝓢(Space d, EuclideanSpace ℝ (Fin d)) := + let f := SchwartzMap.fderivCLM ℝ (E := _) (F := ℝ) η + let g (i : Fin d) := SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i) f + let B : ℝ →L[ℝ] EuclideanSpace ℝ (Fin d) →L[ℝ] EuclideanSpace ℝ (Fin d) := { + toFun a := { + toFun v := a • v + map_add' v1 v2 := by + simp + map_smul' a v := by rw [smul_comm]; simp + cont := by fun_prop } + map_add' v1 v2 := by + ext1 v + simp [add_smul] + map_smul' a v := by + ext1 v + simp [smul_smul] + cont := by + refine continuous_clm_apply.mpr ?_ + intro y + simp + fun_prop + } + let b (i : Fin d) : Space d → EuclideanSpace ℝ (Fin d) := fun x => EuclideanSpace.single i 1 + have hb_temperate (i : Fin d) : Function.HasTemperateGrowth (b i) := by + exact Function.HasTemperateGrowth.const (EuclideanSpace.single i 1) + let x (i : Fin d):= SchwartzMap.bilinLeftCLM B (hb_temperate i) (g i) + ∑ i, x i + +lemma gradSchwartz_apply_eq_grad {d} (η : 𝓢(Space d, ℝ)) (x : Space d): + gradSchwartz η x = grad η x:= by + simp [gradSchwartz, grad_eq_sum] + rfl + end Space diff --git a/PhysLean/SpaceAndTime/Space/IsDistBounded.lean b/PhysLean/SpaceAndTime/Space/IsDistBounded.lean index 2de86070..3d38f6f4 100644 --- a/PhysLean/SpaceAndTime/Space/IsDistBounded.lean +++ b/PhysLean/SpaceAndTime/Space/IsDistBounded.lean @@ -808,6 +808,38 @@ lemma mono {d : ℕ} {f : Space d → F} intro x exact (hfg x).trans (bound1 x) + +/-! + +### D.8. Constant smul with a predicate + +-/ + +lemma if_norm_gt_one_const_smul {d : ℕ} [NormedSpace ℝ F] {f : Space d → F} + (hf : IsDistBounded f) (c1 : ℝ): + IsDistBounded (fun x => (if 1 < ‖x‖ then c1 else 0) • f x) := by + apply IsDistBounded.mono (f := fun x => (max (abs c1) (abs 0)) • f x) + · apply IsDistBounded.const_smul + exact hf + · apply MeasureTheory.AEStronglyMeasurable.smul + · have h1 := MeasureTheory.AEStronglyMeasurable.indicator (s := Set.Ioi (1 : ℝ)) + (f := fun x => c1) (μ := (Measure.map (fun x => ‖x‖) (volume (α := Space d)))) (by fun_prop) (by exact measurableSet_Ioi) + change AEStronglyMeasurable ((fun r => if 1 < r then c1 else 0) ∘ (fun x => ‖x‖)) volume + apply MeasureTheory.AEStronglyMeasurable.comp_aemeasurable + · exact h1 + · fun_prop + · fun_prop + · intro x + rw [norm_smul, norm_smul] + refine mul_le_mul_of_nonneg ?_ ?_ ?_ ?_ + · simp + split_ifs + · simp + · simp + · simp + · positivity + · positivity + /-! ### D.8. Inner products @@ -943,6 +975,7 @@ lemma norm_add_pos_nat_zpow {d : ℕ} (n : ℤ) (a : ℝ) (ha : 0 < a) : rw [abs_of_nonneg (by positivity), abs_of_nonneg (by positivity)] simp + @[fun_prop] lemma nat_pow_shift {d : ℕ} (n : ℕ) (g : Space d) : diff --git a/PhysLean/SpaceAndTime/Space/RadialAngularMeasure.lean b/PhysLean/SpaceAndTime/Space/RadialAngularMeasure.lean index 0000e19f..45aa191e 100644 --- a/PhysLean/SpaceAndTime/Space/RadialAngularMeasure.lean +++ b/PhysLean/SpaceAndTime/Space/RadialAngularMeasure.lean @@ -56,6 +56,10 @@ open MeasureTheory def radialAngularMeasure {d : ℕ} : Measure (Space d) := volume.withDensity (fun x : Space d => ENNReal.ofReal (1 / ‖x‖ ^ (d - 1))) +instance (d : ℕ) : SFinite (radialAngularMeasure (d := d)):= by + dsimp [radialAngularMeasure] + infer_instance + /-! ### A.1. Basic equalities @@ -83,6 +87,7 @@ lemma integrable_radialAngularMeasure_iff {d : ℕ} {f : Space d → F} : simp only [inv_nonneg, norm_nonneg, pow_nonneg, coe_mk] positivity + /-! ## B. Integrals with respect to radialAngularMeasure @@ -99,6 +104,90 @@ lemma integral_radialAngularMeasure {d : ℕ} (f : Space d → F) : refine Eq.symm (Mathlib.Tactic.LinearCombination.smul_eq_const ?_ (f x)) simp +lemma lintegral_radialMeasure {d : ℕ} (f : Space d → ENNReal) (hf : Measurable f) : + ∫⁻ x, f x ∂radialAngularMeasure = ∫⁻ x, ENNReal.ofReal (1 / ‖x‖ ^ (d - 1)) * f x := by + dsimp [radialAngularMeasure] + rw [lintegral_withDensity_eq_lintegral_mul] + simp + · fun_prop + · fun_prop + +lemma lintegral_radialMeasure_eq_spherical_mul (d : ℕ) (f : Space d.succ → ENNReal) (hf : Measurable f) : + ∫⁻ x, f x ∂radialAngularMeasure = ∫⁻ x, f (x.2.1 • x.1.1) + ∂(volume (α := Space d.succ).toSphere.prod (Measure.volumeIoiPow 0)) := by + rw [lintegral_radialMeasure, lintegral_volume_eq_spherical_mul] + apply lintegral_congr_ae + filter_upwards with x + have hx := x.2.2 + simp [Nat.succ_eq_add_one, -Subtype.coe_prop] at hx + simp [norm_smul] + rw [abs_of_nonneg (le_of_lt x.2.2)] + trans ENNReal.ofReal (↑x.2 ^ d * (x.2.1 ^ d)⁻¹) * f (x.2.1 • ↑x.1.1) + · rw [ENNReal.ofReal_mul] + ring + have h2 := x.2.2 + simp at h2 + positivity + trans ENNReal.ofReal 1 * f (x.2.1 • ↑x.1.1) + · congr + field_simp + simp + fun_prop + fun_prop + +open Real +@[simp] +lemma radialAngularMeasure_closedBall (r : ℝ) : + radialAngularMeasure (Metric.closedBall (0 : Space 3) r) = ENNReal.ofReal (4 * π * r) := by + rw [← setLIntegral_one, ← MeasureTheory.lintegral_indicator, + lintegral_radialMeasure_eq_spherical_mul] + rotate_left + · refine (measurable_indicator_const_iff 1).mpr ?_ + exact measurableSet_closedBall + · exact measurableSet_closedBall + have h1 (x : (Metric.sphere (0 : Space) 1) × ↑(Set.Ioi (0 : ℝ))) : + (Metric.closedBall (0 : Space) r).indicator (fun x => (1 : ENNReal)) (x.2.1 • x.1.1) = + (Set.univ ×ˢ {a | a.1 ≤ r}).indicator (fun x => 1) x := by + refine Set.indicator_const_eq_indicator_const ?_ + simp [norm_smul] + rw [abs_of_nonneg (le_of_lt x.2.2)] + simp [h1] + rw [MeasureTheory.lintegral_indicator, setLIntegral_one] + rotate_left + · refine MeasurableSet.prod ?_ ?_ + · exact MeasurableSet.univ + · simp + fun_prop + rw [MeasureTheory.Measure.prod_prod] + simp [Measure.volumeIoiPow] + rw [MeasureTheory.Measure.comap_apply] + rotate_left + · exact Subtype.val_injective + · intro s hs + refine MeasurableSet.subtype_image ?_ hs + exact measurableSet_Ioi + · simp + fun_prop + trans 3 * ENNReal.ofReal (4 / 3 * π) * volume (α := ℝ) (Set.Ioc 0 r) + · congr + ext x + simp + grind + simp + trans ENNReal.ofReal (3 * ((4 / 3 * π) )) * ENNReal.ofReal r + · simp [ENNReal.ofReal_mul] + field_simp + rw [← ENNReal.ofReal_mul] + simp + positivity + +lemma radialAngularMeasure_real_closedBall (r : ℝ) (hr : 0 < r) : + radialAngularMeasure.real (Metric.closedBall (0 : Space 3) r) = 4 * π * r := by + trans (radialAngularMeasure (Metric.closedBall (0 : Space 3) r)).toReal + · rfl + simp + positivity + /-! ## C. HasTemperateGrowth of measures diff --git a/PhysLean/SpaceAndTime/Space/Slice.lean b/PhysLean/SpaceAndTime/Space/Slice.lean index 885ac77f..6edd22a5 100644 --- a/PhysLean/SpaceAndTime/Space/Slice.lean +++ b/PhysLean/SpaceAndTime/Space/Slice.lean @@ -222,6 +222,12 @@ lemma basis_self_eq_slice {d : ℕ} (i : Fin d.succ) : · simp [slice_symm_apply_self] · simp [basis_apply] +@[simp] +lemma slice_basis_self {d : ℕ} (i : Fin d.succ) : + slice i (basis i) = (1, 0) := by + rw [basis_self_eq_slice] + simp + lemma basis_succAbove_eq_slice {d : ℕ} (i : Fin d.succ) (j : Fin d) : basis (Fin.succAbove i j) = (slice i).symm (0, basis j) := by ext k @@ -229,4 +235,59 @@ lemma basis_succAbove_eq_slice {d : ℕ} (i : Fin d.succ) (j : Fin d) : · simp [basis_apply, slice_symm_apply_self] · simp [basis_apply, slice_symm_apply_succAbove] +@[simp] +lemma slice_basis_succAbove {d : ℕ} (i : Fin d.succ) (j : Fin d) : + slice i (basis (Fin.succAbove i j)) = (0, basis j) := by + rw [basis_succAbove_eq_slice] + simp + +/-! + +### A.6. Measures + +-/ + +lemma volume_map_slice_eq_prod {d : ℕ} (i : Fin d.succ) : + MeasureTheory.Measure.map (slice i) volume = volume.prod volume := by + have h1 : volume (α := ℝ) = (OrthonormalBasis.singleton (Fin 1) ℝ).toBasis.addHaar := + (OrthonormalBasis.addHaar_eq_volume _).symm + rw [volume_eq_addHaar, Module.Basis.map_addHaar, volume_eq_addHaar, h1, + ← Module.Basis.prod_addHaar] + let e : Fin 1 ⊕ Fin d → Fin d.succ := fun x => match x with + | Sum.inl 0 => i + | Sum.inr j => Fin.succAbove i j + have e_injective : Function.Injective e := by + intro x y h + match x, y with + | Sum.inl 0, Sum.inl 0 => rfl + | Sum.inl 0, Sum.inr j => simp [e] at h + | Sum.inr j, Sum.inl 0 =>simp [e] at h + | Sum.inr j1, Sum.inr j2 => simp [e] at h; simp [h] + have e_surjective : Function.Surjective e := by + intro j + rcases Fin.eq_self_or_eq_succAbove i j with h | ⟨k, h⟩ + · use Sum.inl 0 + simp [e, h] + · use Sum.inr k + simp [e, h] + have e_bijective : Function.Bijective e := ⟨e_injective, e_surjective⟩ + let eEquiv : Fin 1 ⊕ Fin d ≃ Fin d.succ := Equiv.ofBijective e e_bijective + let b' : Module.Basis (Fin (d.succ)) ℝ (ℝ × Space d) := + Module.Basis.reindex + ((OrthonormalBasis.singleton (Fin 1) ℝ).toBasis.prod basis.toBasis) eEquiv + trans b'.addHaar + · congr + ext1 j + simp [b'] + obtain ⟨k, rfl⟩ := eEquiv.surjective j + simp [eEquiv] + match k with + | Sum.inl 0 => + simp [e] + | Sum.inr j => + simp [e] + simp [b'] + + + end Space diff --git a/PhysLean/SpaceAndTime/Space/Surfaces/Line.lean b/PhysLean/SpaceAndTime/Space/Surfaces/Line.lean new file mode 100644 index 00000000..9bef5e32 --- /dev/null +++ b/PhysLean/SpaceAndTime/Space/Surfaces/Line.lean @@ -0,0 +1,133 @@ +/- +Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Joseph Tooby-Smith +-/ +import PhysLean.SpaceAndTime.Space.ConstantSliceDist +/-! + + +-/ +open SchwartzMap NNReal +noncomputable section +open Distribution +variable (𝕜 : Type) {E F F' : Type} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] + [NormedAddCommGroup F'] [NormedSpace ℝ E] [NormedSpace ℝ F] + +namespace Space + +open MeasureTheory Real + +/-! + +## A. The definition of the line surface + +-/ + +/-- The linear isometry corresponding the inclusion of the x-axis line into + `Space d.succ`. -/ +def line (d : ℕ) : Space 1 →ₗᵢ[ℝ] Space d.succ where + toFun x := { + val i := + match i with + | 0 => x 0 + | ⟨Nat.succ i, h⟩ => 0} + map_add' := by + intro x y + ext i + simp only [Nat.succ_eq_add_one, Fin.isValue, add_apply] + grind + map_smul' := by + intro c x + ext i + simp only [Nat.succ_eq_add_one, Fin.isValue, smul_apply, RingHom.id_apply] + grind + norm_map' := by + intro x + simp [Space.norm_eq] + congr + rw [Finset.sum_eq_single ⟨0, by simp⟩] + · grind + · grind + +@[simp] +lemma line_apply_zero (d : ℕ) (x : Space 1) : line d x 0 = x 0 := by + rfl + +@[simp] +lemma line_apply_succ (d : ℕ) (x : Space 1) (i : Fin d) : line d x (Fin.succ i) = 0 := by + rfl + +@[simp] +lemma line_apply_succ' (d : ℕ) (x : Space 1) (i : ℕ) (h : i + 1 < d.succ) : line d x ⟨i + 1, h⟩ = 0 := by + rfl + +lemma line_eq_slice_symm (d : ℕ) (x : Space 1) : line d x = (slice 0).symm (x 0, 0) := by + ext i + match i with + | ⟨0, h⟩ => simp + | ⟨Nat.succ i, h⟩ => + simp [slice_symm_apply] + rfl + +lemma line_measurable (d : ℕ) : Measurable (line d) := by + apply Continuous.measurable + exact LinearIsometry.continuous (line d) + +lemma line_injective (d : ℕ) : Function.Injective (line d) := by + intro x y h + ext i + fin_cases i + simp only [Fin.zero_eta, Fin.isValue] + rw [← line_apply_zero, h] + simp + +lemma line_measurableEmbedding (d : ℕ) : MeasurableEmbedding (line d) := by + apply Continuous.measurableEmbedding + · exact LinearIsometry.continuous (line d) + · exact line_injective d + +/-! + +## B. The measure associated with the line + +-/ + +/-- The measure on `Space d.succ` corresponding to integration along the `x`-axis. -/ +def lineMeasure (d : ℕ) : Measure (Space d.succ) := MeasureTheory.Measure.map (line d) (volume) + +instance lineMeasure_hasTemperateGrowth (d : ℕ) : (lineMeasure d).HasTemperateGrowth := by + simp [lineMeasure] + refine { exists_integrable := ?_ } + obtain ⟨n, hn⟩ := MeasureTheory.Measure.HasTemperateGrowth.exists_integrable + (μ := volume (α := Space 1) ) + use n + rw [MeasurableEmbedding.integrable_map_iff (line_measurableEmbedding d)] + change Integrable ((fun x => (1 + ‖⇑(line d) x‖) ^ (- (n : ℝ)))) volume + simpa using hn +/-! + +## C. The distribution associated with the line + +-/ + +/-- The distribution corresponding to integrating over a line. + Physically, this is the distribution associated with, for example, lines of charges, + or infinitely thin wires. -/ +def lineDist (d : ℕ) : (Space d.succ) →d[ℝ] ℝ := + SchwartzMap.integralCLM ℝ (lineMeasure d) + +lemma lineDist_apply (d : ℕ) (f : 𝓢(Space d.succ, ℝ)) : + lineDist d f = ∫ x, f (line d x) ∂(volume (α := Space 1)) := by + simp [lineDist, SchwartzMap.integralCLM, SchwartzMap.mkCLMtoNormedSpace, lineMeasure] + rw [MeasurableEmbedding.integral_map (line_measurableEmbedding d)] + +lemma lineDist_eq_constantSliceDist_diracDelta (d : ℕ) : + lineDist d = constantSliceDist 0 (diracDelta ℝ 0) := by + ext η + simp only [Nat.succ_eq_add_one, lineDist_apply, line_eq_slice_symm, Fin.isValue, + constantSliceDist_apply, diracDelta_apply, sliceSchwartz_apply] + rw [integral_one_dim_eq_integral_real] + rfl + +end Space diff --git a/PhysLean/SpaceAndTime/Space/Surfaces/Ring.lean b/PhysLean/SpaceAndTime/Space/Surfaces/Ring.lean new file mode 100644 index 00000000..97c978a0 --- /dev/null +++ b/PhysLean/SpaceAndTime/Space/Surfaces/Ring.lean @@ -0,0 +1,387 @@ +/- +Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Joseph Tooby-Smith +-/ +import PhysLean.SpaceAndTime.Space.Surfaces.SphericalShell +import PhysLean.SpaceAndTime.Space.Translations +import Mathlib.MeasureTheory.Integral.BoundedContinuousFunction +/-! + +## Ring surface in `Space 3` + +-/ +open SchwartzMap NNReal +noncomputable section +open Distribution +variable (𝕜 : Type) {E F F' : Type} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] + [NormedAddCommGroup F'] [NormedSpace ℝ E] [NormedSpace ℝ F] + +namespace Space + +open MeasureTheory Real + +/-! + +## A. The definition of the ring surface + +-/ + +/-- The map embedding the unit ring in `Space d.succ` into `Space d.succ`. -/ +def ring : Metric.sphere (0 : Space 2) 1 → Space 3 := fun x => + (slice 2).symm (0, sphericalShell 1 x) + +lemma ring_eq : ring = (slice 2).symm ∘ (fun x => (0, sphericalShell 1 x)) := rfl + +lemma ring_injective : Function.Injective ring := by + intro x y h + simp [ring] at h + exact sphericalShell_injective _ h + +@[fun_prop] +lemma ring_continuous : Continuous ring := by + apply Continuous.comp + · fun_prop + · fun_prop + +lemma ring_measurableEmbedding : MeasurableEmbedding ring := + Continuous.measurableEmbedding ring_continuous ring_injective + +@[simp] +lemma volume_range_ring : volume (Set.range ring) = 0 := by + rw [ring_eq, Set.range_comp] + trans (MeasureTheory.Measure.map (slice 2) volume) (Set.range (fun x => ((0 : ℝ), sphericalShell 1 x))) + · rw [MeasureTheory.Measure.map_apply_of_aemeasurable] + congr + rw [@ContinuousLinearEquiv.image_symm_eq_preimage] + · fun_prop + · refine measurableSet_range_of_continuous_injective ?_ ?_ + · fun_prop + · intro x y h + simp at h + exact SetCoe.ext h + rw [volume_map_slice_eq_prod] + trans (volume.prod volume) ({(0 : ℝ)} ×ˢ Set.range (sphericalShell 1)) + · congr + ext a + grind + simp + +/-! + +## B. The measure associated with the ring + +-/ + +/-- The measure on `Space 3` corresponding to integration around a ring. -/ +def ringMeasure : Measure (Space 3) := + MeasureTheory.Measure.map ring (MeasureTheory.Measure.toSphere volume) + +instance ringMeasure_hasTemperateGrowth : + ringMeasure.HasTemperateGrowth := by + rw [ringMeasure] + refine { exists_integrable := ?_ } + use 0 + simp + +instance ringMeasure_prod_volume_hasTemperateGrowth : + (ringMeasure.prod (volume (α := Space))).HasTemperateGrowth := by + exact IsDistBounded.instHasTemperateGrowthProdProdOfOpensMeasurableSpace ringMeasure volume + +instance ringMeasure_sFinite: SFinite ringMeasure := by + rw [ringMeasure] + exact Measure.instSFiniteMap volume.toSphere ring + +instance ringMeasure_finite: IsFiniteMeasure ringMeasure := by + rw [ringMeasure] + exact Measure.isFiniteMeasure_map volume.toSphere ring + +lemma integrable_ringMeasure_of_continuous (f : Space → ℝ) (hf : Continuous (f ∘ ring)) : + Integrable f ringMeasure := by + rw [ringMeasure] + rw [MeasurableEmbedding.integrable_map_iff] + · let f' : BoundedContinuousFunction (Metric.sphere (0 : Space 2) 1) ℝ := + BoundedContinuousFunction.mkOfCompact ⟨f ∘ ring, hf⟩ + exact BoundedContinuousFunction.integrable _ f' + · exact ring_measurableEmbedding + + + +lemma integrable_ringMeasure_of_continuous_euclid (f : Space → EuclideanSpace ℝ (Fin n)) (hf : Continuous (f ∘ ring)) : + Integrable f ringMeasure := by + rw [ringMeasure] + rw [MeasurableEmbedding.integrable_map_iff] + · exact BoundedContinuousFunction.integrable _ + (BoundedContinuousFunction.mkOfCompact ⟨f ∘ ring, hf⟩) + · exact ring_measurableEmbedding + +lemma ringMeasure_prod_volume_map : + (ringMeasure.prod (volume (α := Space))).map (fun x : Space × Space => (x.1, x.2 + x.1)) + = (ringMeasure.prod (volume (α := Space))) := by + refine (MeasureTheory.MeasurePreserving.skew_product (f := id) (g := fun x => fun y => y + x) + ?_ ?_ ?_).map_eq + · exact MeasurePreserving.id ringMeasure + · fun_prop + · filter_upwards with x + exact Measure.IsAddRightInvariant.map_add_right_eq_self (x) + +@[simp] +lemma ringMeasure_univ : ringMeasure Set.univ = ENNReal.ofReal ((2 : ℝ) * π) := by + rw [ringMeasure, Measure.map_apply] + simp + · fun_prop + · exact MeasurableSet.univ + + +/-! + +## C. The distribution associated with the ring + +-/ + + + + +/-- The distribution on `Space 3` corresponding to integration around a ring. -/ +def ringDist : (Space 3) →d[ℝ] ℝ := + SchwartzMap.integralCLM ℝ ringMeasure + +lemma ringDist_apply_eq_integral_ringMeasure (f : 𝓢(Space 3, ℝ)) : + ringDist f = ∫ x, f x ∂ringMeasure := by + rw [ringDist, SchwartzMap.integralCLM_apply] + + +lemma ringDist_eq_integral_delta (f : 𝓢(Space 3, ℝ)) : + ringDist f = ∫ z, diracDelta ℝ z f ∂ringMeasure := by + rw [ringDist_apply_eq_integral_ringMeasure] + simp + +open InnerProductSpace +open Real +lemma ringDist_eq_integral_ring_integral_inner (f : 𝓢(Space 3, ℝ)) : + ringDist f = - ∫ z, (∫ r, ⟪(1/ (4 * π )) • ‖r-z‖ ^ (- 3 : ℤ) • basis.repr (r-z), + Space.grad f r⟫_ℝ) + ∂ringMeasure := by + rw [ringDist_eq_integral_delta] + rw [← MeasureTheory.integral_neg] + apply integral_congr_ae + filter_upwards with a + have h1 := Space.distDiv_inv_pow_eq_dim (d := 2) + trans (1/(3 * volume (α := Space).real (Metric.ball 0 1))) * (distDiv <|distTranslate (basis.repr a) <| + (distOfFunction (fun x => ‖x‖ ^ (-3 : ℤ) • basis.repr x) + (IsDistBounded.zpow_smul_repr_self (- 3 : ℤ) (by omega)))) f + · rw [distDiv_distTranslate,] + erw [h1] + simp [distTranslate_apply] + field_simp + rw [distTranslate_ofFunction, distDiv_ofFunction] + simp [inner_smul_left] + rw [integral_const_mul] + ring + + +set_option synthInstance.maxHeartbeats 0 in +lemma ringDist_eq_integral_integral_ring_inner (f : 𝓢(Space 3, ℝ)) : + ringDist f = - ∫ r, (∫ z, ⟪(1/ (4 * π)) • ‖r-z‖ ^ (- 3 : ℤ) • basis.repr (r-z), Space.grad f r⟫_ℝ + ∂ringMeasure) := by + rw [ringDist_eq_integral_ring_integral_inner, MeasureTheory.integral_integral_swap] + /- Integrability condition -/ + /- Generalizing the grad of the schwartz map. -/ + conv_lhs => + enter [1, x, r] + rw [← gradSchwartz_apply_eq_grad] + generalize (gradSchwartz f) = η + /- Turning the integral into an integral of the norms -/ + apply MeasureTheory.Integrable.mono (g := fun r => + (‖(1/ (4 * π)) • ‖r.2 - r.1‖ ^ (- 3 : ℤ) • basis.repr (r.2 - r.1)‖) * ‖η r.2‖) + rotate_left + · simp + apply MeasureTheory.AEStronglyMeasurable.inner + · apply AEMeasurable.aestronglyMeasurable + fun_prop + · refine AEStronglyMeasurable.comp_snd ?_ + fun_prop + · filter_upwards with r + simp + change ‖⟪_, η r.2⟫_ℝ‖ ≤ _ + exact norm_inner_le_norm ((π⁻¹ * 4⁻¹) • (‖r.2 - r.1‖ ^ 3)⁻¹ • (basis.repr r.2 - basis.repr r.1)) + (η r.2) + /- Removing the `(1/ (4 * π))` from the intergable condition. -/ + generalize (1/ (4 * π)) = C + simp [norm_smul, mul_assoc] + apply Integrable.const_mul + simp [← mul_assoc] + /- Simplifying the norms -/ + apply Integrable.congr (f := fun (x : Space × Space) => (‖x.2 - x.1‖ ^ 2)⁻¹ * ‖η x.2‖) + rotate_left + · filter_upwards with r + simp [← map_sub] + left + by_cases h : ‖r.2 - r.1‖ = 0 + · simp [h] + field_simp + /- Turn the condition into a statement about temperate growth -/ + suffices h : ∃ (n : ℕ), Integrable (fun x : Space × Space => (‖x.2 - x.1‖ ^ 2)⁻¹ * + (1 + ‖x.2‖) ^ (- n : ℝ)) (ringMeasure.prod volume) by + obtain ⟨n, hn⟩ := h + let μ := (ringMeasure.prod (volume (α := Space))) + have h1 {f : Space → EuclideanSpace ℝ (Fin 3)} -- based on integrable_of_le_of_pow_mul_le + {C₁ C₂ : ℝ} {k : ℕ} (hf : ∀ x, ‖f x‖ ≤ C₁) + (h'f : ∀ x, ‖x‖ ^ (k + n) * ‖f x‖ ≤ C₂) (h''f : AEStronglyMeasurable (fun x => f x.2) μ) : + Integrable (fun x : Space × Space ↦ (‖x.2 - x.1‖ ^ 2)⁻¹ * ‖x.2‖ ^ k * ‖f x.2‖) μ := by + apply (hn.const_mul (2 ^ n * (C₁ + C₂))).mono' + · apply AEStronglyMeasurable.mul + · fun_prop + · exact h''f.norm + · filter_upwards with v + simp only [norm_mul, norm_pow, norm_norm, mul_assoc] + trans ‖(‖v.2 - v.1‖ ^ 2)⁻¹‖ * (2 ^ n * (C₁ + C₂) * (1 + ‖v.2‖) ^ (-n : ℝ)) + · apply mul_le_mul + · rfl + · exact pow_mul_le_of_le_of_pow_mul_le (norm_nonneg _) (norm_nonneg _) (hf v.2) (h'f v.2) + · positivity + · positivity + apply le_of_eq + simp + ring + have h2 (f : 𝓢(Space, EuclideanSpace ℝ (Fin 3))) -- based on integrable_pow_mul_iteratedFDeriv + (k : ℕ) : Integrable (fun x : Space × Space ↦ (‖x.2 - x.1‖ ^ 2)⁻¹ * ‖x.2‖ ^ k * ‖f x.2‖) + μ := by + apply h1 (C₁ := (SchwartzMap.seminorm ℝ 0 0) f) + (C₂ := (SchwartzMap.seminorm ℝ (k + n) 0) f) + · fun_prop + · intro x + simpa using norm_iteratedFDeriv_le_seminorm ℝ f 0 x + · intro x + simpa using le_seminorm ℝ (k + n) 0 f x + simpa using h2 η 0 + + obtain ⟨n, hn⟩ := Measure.HasTemperateGrowth.exists_integrable (μ := volume (α := Space)) + use n + + let f : Space × Space → ℝ := (fun x => (‖x.2 - x.1‖ ^ 2)⁻¹ * (1 + ‖x.2‖) ^ (- n : ℝ)) + let S : Set (Space × Space) := {x | ‖x.2 - x.1‖ ≤ 1} + have f_split : f = Set.indicator S f + Set.indicator (Sᶜ) f := by + exact Eq.symm (Set.indicator_self_add_compl S f) + change Integrable f (ringMeasure.prod volume) + rw [f_split] + apply Integrable.add + · rw [MeasureTheory.integrable_indicator_iff] + rotate_left + · simp [S] + fun_prop + apply Integrable.mono (g := fun x => (‖x.2 - x.1‖ ^ 2)⁻¹ ) + rotate_left + · fun_prop + · filter_upwards with x + simp [f] + field_simp + generalize h : ‖x.2 - x.1‖ ^ 2 = a + + by_cases a_zero : a = 0 + · subst a_zero + simp + refine (div_le_div_iff_of_pos_right ?_).mpr ?_ + · subst h + positivity + · refine one_le_pow₀ ?_ + rw [abs_of_nonneg (by positivity)] + simp + + change IntegrableOn (fun x => (‖x.2 - x.1‖ ^ 2)⁻¹) S (ringMeasure.prod volume) + let em : (Space × Space) ≃ᵐ (Space × Space) := + { toFun := fun x => (x.1, x.2 + x.1) + invFun := fun x => (x.1, x.2 - x.1) + left_inv x := by simp + right_inv x := by simp + measurable_toFun := by fun_prop + measurable_invFun := by fun_prop} + rw [← ringMeasure_prod_volume_map] + change IntegrableOn (fun x => (‖x.2 - x.1‖ ^ 2)⁻¹) S (Measure.map em (ringMeasure.prod volume)) + rw [MeasurableEmbedding.integrableOn_map_iff] + rotate_left + · exact MeasurableEquiv.measurableEmbedding em + have hl : (⇑em ⁻¹' S) = Set.univ ×ˢ Metric.closedBall (0 : Space) 1 := by + ext x + simp [em, S] + rw [hl] + have fun_em : ((fun x => (‖x.2 - x.1‖ ^ 2)⁻¹) ∘ ⇑em) = fun x => (‖x.2‖ ^ 2)⁻¹ := by + ext x + simp [em] + rw [fun_em] + suffices h : IntegrableOn (fun x => (1 : ℝ)) (Set.univ ×ˢ Metric.closedBall 0 1) (ringMeasure.prod (radialAngularMeasure (d := 3))) by + rw [radialAngularMeasure] at h + rw [MeasureTheory.prod_withDensity_right] at h + rw [MeasureTheory.IntegrableOn] at h + rw [MeasureTheory.restrict_withDensity] at h + rw [MeasureTheory.integrable_withDensity_iff ] at h + rotate_left + · fun_prop + · simp + · refine MeasurableSet.prod ?_ ?_ + · exact MeasurableSet.univ + · exact measurableSet_closedBall + · fun_prop + simpa using h + simp only [enorm_one, ne_eq, ENNReal.one_ne_top, not_false_eq_true, integrableOn_const_iff, + one_ne_zero, Measure.prod_prod, ringMeasure_univ, radialAngularMeasure_closedBall, mul_one, + false_or] + rw [← ENNReal.ofReal_mul] + simp + positivity + · rw [MeasureTheory.integrable_indicator_iff] + rotate_left + · simp [S] + fun_prop + apply Integrable.mono (g := fun x => (1 + ‖x.2‖) ^ (- n : ℝ)) + rotate_left + · fun_prop + · have hs : MeasurableSet Sᶜ := by + simp [S] + fun_prop + filter_upwards [MeasureTheory.ae_restrict_mem hs] with x hx + simp [S] at hx + simp [f] + trans 1 * (|1 + ‖x.2‖|) ^ (- n : ℝ) + · apply mul_le_mul + · refine inv_le_one_iff₀.mpr ?_ + right + nlinarith + · simp + · positivity + · positivity + simp + apply MeasureTheory.Integrable.integrableOn + simpa using MeasureTheory.Integrable.mul_prod (f := fun (x : Space) => 1) + (by simp) hn + + +lemma ringDist_eq_integral (f : 𝓢(Space 3, ℝ)) : + ringDist f = - ∫ r, (⟪∫ z, (1/ (4 * π)) • ‖r-z‖ ^ (- 3 : ℤ) • basis.repr (r-z) + ∂ringMeasure, Space.grad f r⟫_ℝ) := by + rw [ringDist_eq_integral_integral_ring_inner] + congr 1 + apply integral_congr_ae + have hs : (Set.range ring)ᶜ ∈ ae volume := by + refine compl_mem_ae_iff.mpr ?_ + simp + filter_upwards [hs] with x hx + rw [real_inner_comm, ← integral_inner] + simp [real_inner_comm] + · apply integrable_ringMeasure_of_continuous_euclid + apply Continuous.smul + · fun_prop + apply Continuous.smul + · simp + refine Continuous.inv₀ ?_ ?_ + · refine Continuous.zpow₀ ?_ 3 ?_ + · fun_prop + · simp + · intro z hz + simp [zpow_eq_zero_iff] at hz + have hl : x = ring z := by grind + subst hl + simp at hx + · fun_prop + +end Space diff --git a/PhysLean/SpaceAndTime/Space/Surfaces/SphericalShell.lean b/PhysLean/SpaceAndTime/Space/Surfaces/SphericalShell.lean new file mode 100644 index 00000000..b5f4f3e9 --- /dev/null +++ b/PhysLean/SpaceAndTime/Space/Surfaces/SphericalShell.lean @@ -0,0 +1,254 @@ +/- +Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Joseph Tooby-Smith +-/ +import PhysLean.SpaceAndTime.Space.ConstantSliceDist +import PhysLean.SpaceAndTime.Space.Norm + +import Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic + +/-! + + +-/ +open SchwartzMap NNReal +noncomputable section +open Distribution +variable (𝕜 : Type) {E F F' : Type} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] + [NormedAddCommGroup F'] [NormedSpace ℝ E] [NormedSpace ℝ F] + +namespace Space + +open MeasureTheory Real + +/-! + +## A. The definition of the spherical shell surface + +-/ + +/-- The map embedding the unit sphere in `Space d.succ` into `Space d.succ`. -/ +def sphericalShell (d : ℕ) : Metric.sphere (0 : Space d.succ) 1 → Space d.succ := fun x => x.1 + +lemma sphericalShell_injective (d : ℕ) : Function.Injective (sphericalShell d) := by + intro x y h + simp [sphericalShell] at h + grind + +lemma sphericalShell_continuous (d : ℕ) : Continuous (sphericalShell d) := continuous_subtype_val + +lemma sphericalShell_measurableEmbedding (d : ℕ) : MeasurableEmbedding (sphericalShell d) := by + apply Continuous.measurableEmbedding + · exact sphericalShell_continuous d + · exact sphericalShell_injective d + +@[simp] +lemma norm_sphericalShell (d : ℕ) (x : Metric.sphere (0 : Space d.succ) 1) : + ‖sphericalShell d x‖ = 1 := by + simp [sphericalShell, Metric.sphere] + +/-! + +## B. The measure associated with the spherical shell + +-/ + +/-- The measure on `Space d.succ` corresponding to integration around a spherical shell. -/ +def sphericalShellMeasure (d : ℕ) : Measure (Space d.succ) := + MeasureTheory.Measure.map (sphericalShell d) (MeasureTheory.Measure.toSphere volume) + +instance sphericalShellMeasure_hasTemperateGrowth (d : ℕ) : + (sphericalShellMeasure d).HasTemperateGrowth := by + rw [sphericalShellMeasure] + refine { exists_integrable := ?_ } + use 0 + simp + +/-! + +## C. The distribution associated with the spherical shell + +-/ + +/-- The distribution associated with a spherical shell. + One can roughly think of this distribution as the distribution which + takes test functions `f (r)` to `∫ d³r f(r) ρ(r)` where `ρ(r)` is the + mass, charge or current etc. distribution. -/ +def sphericalShellDist (d : ℕ) : (Space d.succ) →d[ℝ] ℝ := + SchwartzMap.integralCLM ℝ (sphericalShellMeasure d) + + +lemma sphericalShellDist_apply_eq_integral_sphericalShellMeasure (d : ℕ) (f : 𝓢(Space d.succ, ℝ)) : + sphericalShellDist d f = ∫ x, f x ∂sphericalShellMeasure d := by + rw [sphericalShellDist, SchwartzMap.integralCLM_apply] + +lemma sphericalShellDist_apply_eq_integral_sphere_volume (d : ℕ) (f : 𝓢(Space d.succ, ℝ)) : + sphericalShellDist d f = + ∫ x, f (sphericalShell d x) ∂(MeasureTheory.Measure.toSphere volume) := by + rw [sphericalShellDist_apply_eq_integral_sphericalShellMeasure, sphericalShellMeasure, + MeasurableEmbedding.integral_map (sphericalShell_measurableEmbedding d)] + +lemma sphericalShellDist_apply_eq_integral_radius_ioi_one (d : ℕ) (f : 𝓢(Space d.succ, ℝ)) : + sphericalShellDist d f = + ∫ n, (-∫ (r : ℝ) in Set.Ioi 1, _root_.deriv (fun r => f (r • n.1)) r) ∂(volume.toSphere) := by + rw [sphericalShellDist_apply_eq_integral_sphere_volume] + congr + funext x + let η' : 𝓢(ℝ, ℝ) := compCLM (g := fun a => a • (sphericalShell d x) ) ℝ (by + apply And.intro + · fun_prop + · intro n' + match n' with + | 0 => + use 1, 1 + simp [norm_smul] + | 1 => + use 0, 1 + intro x + simp [fderiv_smul_const, iteratedFDeriv_succ_eq_comp_right] + | n' + 1 + 1 => + use 0, 0 + intro x + simp only [Real.norm_eq_abs, pow_zero, mul_one, norm_le_zero_iff] + rw [iteratedFDeriv_succ_eq_comp_right] + conv_lhs => + enter [2, 3, y] + simp [fderiv_smul_const] + rw [iteratedFDeriv_succ_const] + rfl) (by use 1, 1; simp [norm_smul]) f + rw [MeasureTheory.integral_Ioi_of_hasDerivAt_of_tendsto + (f := fun r => f (r • sphericalShell d x)) (m := 0)] + · simp + · fun_prop + · intro x hx + refine DifferentiableAt.hasDerivAt ?_ + have := f.differentiable + fun_prop + · exact (integrable ((derivCLM ℝ ℝ) η')).integrableOn + · exact Filter.Tendsto.mono_left η'.toZeroAtInfty.zero_at_infty' atTop_le_cocompact + +lemma sphericalShellDist_apply_eq_integral_radius_ioi_if (d : ℕ) (f : 𝓢(Space d.succ, ℝ)) : + sphericalShellDist d f = + ∫ n, (-∫ (r : ℝ) in Set.Ioi 0, (if 1 < r then 1 else 0) * + _root_.deriv (fun r => f (r • n.1)) r) ∂(volume.toSphere) := by + rw [sphericalShellDist_apply_eq_integral_radius_ioi_one] + congr + funext n + simp only [Nat.succ_eq_add_one, ite_mul, one_mul, zero_mul, neg_inj] + rw [← MeasureTheory.integral_indicator measurableSet_Ioi] + rw [← MeasureTheory.integral_indicator measurableSet_Ioi] + congr + funext x + simp [Set.indicator] + intro h1 h2 + linarith + +lemma sphericalShellDist_apply_eq_volumeIoiPow (d : ℕ) (f : 𝓢(Space d.succ, ℝ)) : + sphericalShellDist d f = + ∫ n, (-∫ r, ‖r.1‖⁻¹ ^ d * (if 1 < r.1 then 1 else 0) * + _root_.deriv (fun r => f (r • n.1)) r.1 + ∂((Measure.volumeIoiPow (Module.finrank ℝ (Space d.succ) - 1)))) ∂(volume.toSphere) := by + rw [sphericalShellDist_apply_eq_integral_radius_ioi_if] + congr + funext n + simp [Measure.volumeIoiPow] + erw [integral_withDensity_eq_integral_smul (by fun_prop)] + rw [← Measure.Subtype.volume_def] + rw [← MeasureTheory.integral_subtype] + congr + funext r + split_ifs + any_goals simp + rename_i h + generalize _root_.deriv (fun r => f (r • ↑n)) r.1 = a + symm + trans ((r.1 ^ d).toNNReal : ℝ) • ((|r.1| ^ d)⁻¹ * a) + · rfl + simp + rw [max_eq_left (by positivity)] + field_simp + rw [abs_of_nonneg] + positivity + +lemma sphericalShellDist_apply_eq_volumeIoiPow_prod (d : ℕ) (f : 𝓢(Space d.succ, ℝ)) : + sphericalShellDist d f = - + ∫ r, ‖r.2.1‖⁻¹ ^ d * (if 1 < r.2.1 then 1 else 0) * + _root_.deriv (fun a => f (a • r.1)) r.2.1 + ∂(volume (α := Space d.succ).toSphere.prod + (Measure.volumeIoiPow (Module.finrank ℝ (Space d.succ) - 1))) := by + rw [MeasureTheory.integral_prod, sphericalShellDist_apply_eq_volumeIoiPow, + MeasureTheory.integral_neg] + /- Integrability condition -/ + convert integrable_isDistBounded_inner_grad_schwartzMap_spherical + ((IsDistBounded.inv_pow_smul_repr_self (d.succ) (by omega)).if_norm_gt_one_const_smul 1) f + rename_i r + simp [norm_smul] + rw [abs_of_nonneg (le_of_lt r.2.2)] + split_ifs + swap + · simp + rename_i hrl + let x : Space d.succ := r.2.1 • r.1.1 + have hr := r.2.2 + simp [-Subtype.coe_prop] at hr + have hr2 : r.2.1 ≠ 0 := by exact Ne.symm (ne_of_lt hr) + trans (r.2.1 ^ d)⁻¹ * _root_.deriv (fun a => f (a • ‖↑x‖⁻¹ • ↑x)) ‖x‖ + · simp [x, norm_smul] + left + congr + funext a + congr + simp [smul_smul] + rw [abs_of_nonneg (le_of_lt hr)] + field_simp + simp only [one_smul] + rw [abs_of_nonneg (le_of_lt hr)] + rw [← grad_inner_space_unit_vector] + rw [real_inner_comm] + simp [inner_smul_left, x, norm_smul, abs_of_nonneg (le_of_lt hr)] + field_simp + ring + exact SchwartzMap.differentiable f + +lemma sphericalShellDist_apply_eq_volume_deriv_radius (d : ℕ) (f : 𝓢(Space d.succ, ℝ)) : + sphericalShellDist d f = - + ∫ (r : Space d.succ), ‖r‖⁻¹ ^ d * (if 1 < ‖r‖ then 1 else 0) * + _root_.deriv (fun a => f (a • ‖r‖⁻¹ • r)) ‖r‖ := by + rw [sphericalShellDist_apply_eq_volumeIoiPow_prod] + rw [← MeasureTheory.MeasurePreserving.integral_comp (f := homeomorphUnitSphereProd _) + (MeasureTheory.Measure.measurePreserving_homeomorphUnitSphereProd + (volume (α := Space d.succ))) + (Homeomorph.measurableEmbedding (homeomorphUnitSphereProd (Space d.succ)))] + congr 1 + simp only [Nat.succ_eq_add_one, homeomorphUnitSphereProd_apply_snd_coe, norm_norm, inv_pow, + mul_ite, mul_one, mul_zero, homeomorphUnitSphereProd_apply_fst_coe, ite_mul, zero_mul] + let f (x : Space d.succ) : ℝ := + if 1 < ‖↑x‖ then (‖↑x‖ ^ d)⁻¹ * _root_.deriv (fun a => f (a • ‖↑x‖⁻¹ • ↑x)) ‖↑x‖ + else 0 + conv_lhs => + enter [2, x] + change f x.1 + rw [MeasureTheory.integral_subtype_comap (by simp), ← setIntegral_univ] + simp + rfl + +open InnerProductSpace + +lemma sphericalShellDist_apply_eq_integral_grad (d : ℕ) (f : 𝓢(Space d.succ, ℝ)) : + sphericalShellDist d f = + - ∫ x, ⟪(if 1 < ‖x‖ then 1 else 0) • ‖x‖⁻¹ ^ d.succ • basis.repr x, Space.grad f x⟫_ℝ := by + rw [sphericalShellDist_apply_eq_volume_deriv_radius] + congr + funext r + split_ifs + swap + · simp + simp + symm + trans ‖r‖⁻¹ ^ d * ⟪‖r‖⁻¹ • basis.repr r, Space.grad f r⟫_ℝ + · simp only [Nat.succ_eq_add_one, inv_pow, inner_smul_left, map_inv₀, conj_trivial] + ring_nf + simp [real_inner_comm, ← grad_inner_space_unit_vector _ _ (SchwartzMap.differentiable f)] + +end Space