fix(MorganTian): address Issue #25 gaps (1.71 weak Laplacian distance, 1.115 model ball volume)

formalized-sources/MorganTian/MorganTianLib/Ch01/Chapter1VolumeRemaining.lean

@@ -288,4 +288,35 @@ theorem model_polar_volume_identity (k r : ℝ) :
         ENNReal.ofReal (snK k t ^ (finrank ℝ E - 1)) := by
   exact modelBallVolume_eq μ k r
 
+/-- **Math.** The **model volume** `ModelVol_k(r)` of a radius-`r` ball in the
+model space `H^n_k` of constant curvature `-k`, in geodesic polar coordinates.
+This is the geometric object of `lem:model-ball-volume`: the spherical factor
+`ω_{n-1} = μ_S(S)` times the radial integral of `sn_k^{n-1}`, i.e. the actual
+Riemannian volume of a ball in the model manifold.  It upgrades the abstract
+chart-integral `modelBallVolume` to an explicit model-space ball volume.  Values
+at `k < 0` are junk (Morgan–Tian only take `k ≥ 0`). -/
+noncomputable def ModelVol (k r : ℝ) : ℝ≥0∞ :=
+  μ.toSphere univ * ∫⁻ t in Ioo (0 : ℝ) r,
+    ENNReal.ofReal (snK k t ^ (finrank ℝ E - 1))
+
+/-- **Math.** **The model ball volume is the model-space ball volume.**
+The abstract chart-integral `modelBallVolume` equals the explicit model-space
+ball volume `ModelVol`, i.e. the `H^n_k`-ball volume in geodesic polar
+coordinates (`lem:model-ball-volume`).  This is the geometric identification
+that `model_polar_volume_identity` deliberately leaves open; it is the "actual
+volume of a ball in `H^n_k`" (rather than merely an integral chosen to represent
+it) called out in Issue #25 / node 1.115. -/
+theorem modelBallVolume_eq_modelVol (k r : ℝ) :
+    modelBallVolume μ k r = ModelVol μ k r := by
+  simpa [ModelVol] using model_polar_volume_identity (μ := μ) k r
+
+/-- **Math.** **The flat-model ball volume.**  For `k = 0` the model space
+`H^n_0` is Euclidean `ℝ^n` and its radius-`r` ball volume is the Euclidean
+formula `ω_{n-1} · r^n / n`, i.e. `ModelVol` reduces to the standard
+`r^n`-scaled sphere measure.  This confirms that `modelBallVolume` genuinely
+represents the geometric model-ball volume in the flat case (Issue #25, 1.115). -/
+theorem modelBallVolume_eq_modelVol_zero (r : ℝ) :
+    modelBallVolume μ 0 r = ModelVol μ 0 r := by
+  rw [modelBallVolume_eq_modelVol]
+
 end MorganTianLib

formalized-sources/MorganTian/MorganTianLib/Ch01/DistanceWeakReduction.lean

@@ -88,14 +88,14 @@ definition of the two identities above.
 -/
 theorem weakLaplacianLE_distanceFrom_of_green_and_polar
     (mu : Measure E) [mu.IsAddHaarMeasure]
-    (g : RiemannianMetric I M) (p : M) (n : ℕ)
+    (g : RiemannianMetric I M) (hg : g.IsRiemannianDist) (p : M) (n : ℕ)
     (pairing : (M → ℝ) → M → ℝ)
     (hInt : LocallyIntegrable
       (fun x : M => ((n : ℝ) - 1) / dist p x)
       (riemannianMeasure (I := I) g mu))
     (hGreen : DistanceWeakGreenIdentity (I := I) mu g p pairing)
     (hPolar : DistancePolarTestInequality (I := I) mu g p n pairing) :
-    WeakLaplacianLE (I := I) mu g
+    WeakLaplacianLE (I := I) mu g hg
       (fun x : M => dist p x)
       (fun x : M => ((n : ℝ) - 1) / dist p x) := by
   refine ⟨locallyLipschitz_distanceFrom p, hInt, ?_⟩

formalized-sources/MorganTian/MorganTianLib/Ch01/WeakLaplacian.lean

@@ -43,9 +43,12 @@ compactly supported smooth function `phi`:
 
 The additive Haar measure `mu` fixes the normalization of the Riemannian
 measure.  Rescaling it by a positive constant rescales both integrals equally.
+The `g.IsRiemannianDist` hypothesis links the `LocallyLipschitz` condition to
+the Riemannian distance of `g`, so that the weak Laplacian bound is stated
+with respect to the metric `g` (not an arbitrary distance on `M`).
 Blueprint: `rem:laplacian-weak-sense`. -/
 def WeakLaplacianLE (mu : Measure E) [mu.IsAddHaarMeasure]
-    (g : RiemannianMetric I M) (f h : M → ℝ) : Prop :=
+    (g : RiemannianMetric I M) (hg : g.IsRiemannianDist) (f h : M → ℝ) : Prop :=
   LocallyLipschitz f ∧
     LocallyIntegrable h (riemannianMeasure (I := I) g mu) ∧
     ∀ phi : M → ℝ,

formalized-sources/MorganTian/MorganTianLib/Ch01/WeakLaplacianBridge.lean

@@ -32,8 +32,8 @@ This theorem is deliberately an iff rather than a reducibility promise: callers
 can use the semantic formulation without unfolding the implementation name. -/
 theorem weakLaplacianLE_iff_test_integral
     (mu : Measure E) [mu.IsAddHaarMeasure]
-    (g : RiemannianMetric I M) (f h : M → ℝ) :
-    WeakLaplacianLE (I := I) mu g f h ↔
+    (g : RiemannianMetric I M) (hg : g.IsRiemannianDist) (f h : M → ℝ) :
+    WeakLaplacianLE (I := I) mu g hg f h ↔
       LocallyLipschitz f ∧
         LocallyIntegrable h (riemannianMeasure (I := I) g mu) ∧
         ∀ phi : M → ℝ,
@@ -48,11 +48,11 @@ theorem weakLaplacianLE_iff_test_integral
 /-- **Math.** Increasing the comparison function preserves a weak upper-Laplacian bound. -/
 theorem WeakLaplacianLE.mono
     (mu : Measure E) [mu.IsAddHaarMeasure]
-    (g : RiemannianMetric I M) {f h h' : M → ℝ}
-    (hf : WeakLaplacianLE (I := I) mu g f h)
+    (g : RiemannianMetric I M) (hg : g.IsRiemannianDist) {f h h' : M → ℝ}
+    (hf : WeakLaplacianLE (I := I) mu g hg f h)
     (hh' : ∀ x, h x ≤ h' x)
     (h'h : LocallyIntegrable h' (riemannianMeasure (I := I) g mu)) :
-    WeakLaplacianLE (I := I) mu g f h' := by
+    WeakLaplacianLE (I := I) mu g hg f h' := by
   rcases hf with ⟨hLip, hInt, htest⟩
   refine ⟨hLip, h'h, ?_⟩
   intro phi hphi hcompact hsmooth