feat: Add surfaces

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

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

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) :

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