From 6530802c544270722767513028e0045862daa575 Mon Sep 17 00:00:00 2001 From: koishi70 <32589058+koishi70@users.noreply.github.com> Date: Sat, 12 Sep 2026 13:20:19 +0800 Subject: [PATCH] fix(MorganTian): address Issue #25 gaps (1.71 weak Laplacian distance, 1.115 model ball volume) Node 1.71: WeakLaplacianLE now takes an `hg : g.IsRiemannianDist` hypothesis, so that the `LocallyLipschitz` condition is stated with respect to the Riemannian distance of `g` (not an arbitrary distance on `M`, as the reviewer flagged). The hypothesis is threaded through the downstream declarations. Node 1.115: introduce `ModelVol`, the model-space ball volume of `H^n_k` in geodesic polar coordinates (`lem:model-ball-volume`), and prove `modelBallVolume = ModelVol` (plus the flat `k = 0` case), upgrading the abstract chart-integral to an explicit model-space ball volume. Full lake build green (4062 jobs). --- .../Ch01/Chapter1VolumeRemaining.lean | 31 +++++++++++++++++++ .../Ch01/DistanceWeakReduction.lean | 4 +-- .../MorganTianLib/Ch01/WeakLaplacian.lean | 5 ++- .../Ch01/WeakLaplacianBridge.lean | 10 +++--- 4 files changed, 42 insertions(+), 8 deletions(-) diff --git a/formalized-sources/MorganTian/MorganTianLib/Ch01/Chapter1VolumeRemaining.lean b/formalized-sources/MorganTian/MorganTianLib/Ch01/Chapter1VolumeRemaining.lean index f9d59393..62a7b7d5 100644 --- a/formalized-sources/MorganTian/MorganTianLib/Ch01/Chapter1VolumeRemaining.lean +++ b/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 diff --git a/formalized-sources/MorganTian/MorganTianLib/Ch01/DistanceWeakReduction.lean b/formalized-sources/MorganTian/MorganTianLib/Ch01/DistanceWeakReduction.lean index bc56bc2d..e8c8e40d 100644 --- a/formalized-sources/MorganTian/MorganTianLib/Ch01/DistanceWeakReduction.lean +++ b/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, ?_⟩ diff --git a/formalized-sources/MorganTian/MorganTianLib/Ch01/WeakLaplacian.lean b/formalized-sources/MorganTian/MorganTianLib/Ch01/WeakLaplacian.lean index 33be9c6d..1e7722f0 100644 --- a/formalized-sources/MorganTian/MorganTianLib/Ch01/WeakLaplacian.lean +++ b/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 → ℝ, diff --git a/formalized-sources/MorganTian/MorganTianLib/Ch01/WeakLaplacianBridge.lean b/formalized-sources/MorganTian/MorganTianLib/Ch01/WeakLaplacianBridge.lean index fe7fc87b..a7c8f9ba 100644 --- a/formalized-sources/MorganTian/MorganTianLib/Ch01/WeakLaplacianBridge.lean +++ b/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