9k: eliminate _g wrappers — Bochner stack fully explicit-g

OpenGALib/GeometricMeasureTheory/Isoperimetric/ReducedBoundary.lean

@@ -143,9 +143,10 @@ infrastructure.
 
 **Ground truth**: Maggi 2012 Theorem 15.5. -/
 theorem tangentHyperplane_at_reducedBoundary_orthogonal
+    (g : Riemannian.RiemannianMetric I M)
     (Ω : FinitePerimeter M) (x : M)
     (_hx : x ∈ FinitePerimeter.reducedBoundary Ω) (v : TangentSpace I x) :
-    Riemannian.HasMetric.metric.metricInner x v (Varifold.bvGradientDirection I Ω x) = 0 ↔
+    g.metricInner x v (Varifold.bvGradientDirection I Ω x) = 0 ↔
       v ∈ (Submodule.span ℝ {Varifold.bvGradientDirection I Ω x})ᗮ := by
   sorry
 

OpenGALib/Riemannian/Operators/Bochner.lean

@@ -55,12 +55,15 @@ Combines `hessian_gradientNormSq_apply_chartFrame` summed over
 `OrthonormalBasis.sum_sq_inner_left` for Frobenius². -/
 theorem bochner_leibniz_trace_reduction
     [IsManifold I 2 M]
+    (g : RiemannianMetric I M) (hg : g = hm.metric)
     (f : M → ℝ) (hf : ContMDiff I 𝓘(ℝ, ℝ) ∞ f) (x : M) :
-    (1 / 2 : ℝ) * (Operators.scalarLaplacian (I := I) HasMetric.metric ((fun y => HasMetric.metric.metricInner y (manifoldGradient (I := I) HasMetric.metric f y) (manifoldGradient (I := I) HasMetric.metric f y)))) x
-      = HasMetric.metric.metricInner x
-            (connectionLaplacian HasMetric.metric (manifoldGradient (I := I) HasMetric.metric f) x)
-            ((manifoldGradient (I := I) HasMetric.metric f) x)
-        + frobeniusSq (I := I) (M := M) (Operators.hessianBilin (I := I) HasMetric.metric f) x := by
+    (1 / 2 : ℝ) * Operators.scalarLaplacian g
+        (fun y => g.metricInner y (manifoldGradient (I := I) g f y)
+                                  (manifoldGradient (I := I) g f y)) x
+      = g.metricInner x (connectionLaplacian g (manifoldGradient (I := I) g f) x)
+            (manifoldGradient (I := I) g f x)
+        + Operators.frobeniusSq (I := I) (M := M) (Operators.hessianBilin (I := I) g f) x := by
+  subst hg
   classical
   have h_grad := manifoldGradient_smooth_of_smooth HasMetric.metric f hf
   show (1 / 2 : ℝ) * Operators.scalarLaplacian (I := I) (M := M) HasMetric.metric ((fun y => HasMetric.metric.metricInner y (manifoldGradient (I := I) HasMetric.metric f y) (manifoldGradient (I := I) HasMetric.metric f y))) x
@@ -211,20 +214,6 @@ theorem bochner_leibniz_trace_reduction
       _ = ∑ j, ⟪v, b j⟫_ℝ ^ 2 := (b.sum_sq_inner_left v).symm
       _ = ∑ j, (HasMetric.metric.metricInner x v (b j)) ^ 2 := rfl
 
-/-- **Math.** **Explicit-`g` form of the Leibniz trace reduction**. -/
-theorem bochner_leibniz_trace_reduction_g
-    [IsManifold I 2 M]
-    (g : RiemannianMetric I M) (hg : g = hm.metric)
-    (f : M → ℝ) (hf : ContMDiff I 𝓘(ℝ, ℝ) ∞ f) (x : M) :
-    (1 / 2 : ℝ) * Operators.scalarLaplacian g
-        (fun y => g.metricInner y (manifoldGradient (I := I) g f y)
-                                  (manifoldGradient (I := I) g f y)) x
-      = g.metricInner x (connectionLaplacian g (manifoldGradient (I := I) g f) x)
-            (manifoldGradient (I := I) g f x)
-        + Operators.frobeniusSq (I := I) (M := M) (Operators.hessianBilin (I := I) g f) x := by
-  subst hg
-  exact bochner_leibniz_trace_reduction f hf x
-
 /-! ## The headline identity -/
 
 /-- **Math.** **Bochner–Weitzenböck identity** (unconditional under
@@ -239,23 +228,6 @@ Composes `bochner_leibniz_trace_reduction` (LHS step) with
 
 Reference: Petersen Ch. 7 §1 Prop 33; do Carmo §6; Schoen-Simon 1981 §1. -/
 theorem bochner_weitzenboeck
-    [IsManifold I 2 M]
-    (f : M → ℝ) (hf : ContMDiff I 𝓘(ℝ, ℝ) ∞ f) (x : M) :
-    (1 / 2 : ℝ) * (Operators.scalarLaplacian (I := I) HasMetric.metric ((fun y => HasMetric.metric.metricInner y (manifoldGradient (I := I) HasMetric.metric f y) (manifoldGradient (I := I) HasMetric.metric f y)))) x =
-      frobeniusSq (I := I) (M := M) (Operators.hessianBilin (I := I) HasMetric.metric f) x
-      + HasMetric.metric.metricInner x ((manifoldGradient (I := I) HasMetric.metric f) x)
-            ((manifoldGradient (I := I) HasMetric.metric (Operators.scalarLaplacian (I := I) HasMetric.metric f)) x)
-      + ricciTensor HasMetric.metric x ((manifoldGradient (I := I) HasMetric.metric f) x) ((manifoldGradient (I := I) HasMetric.metric f) x) := by
-  rw [bochner_leibniz_trace_reduction f hf x,
-      bochner_connectionLaplacian_grad_decomposition HasMetric.metric rfl f hf x]
-  abel
-
-/-- **Math.** **Explicit-`g` form of the Bochner–Weitzenböck identity**.
-Same statement as `bochner_weitzenboeck` but the metric `g` is an explicit
-`RiemannianMetric I M` parameter constrained by `hg : g = hm.metric`,
-giving consumers a `g`-parametric API without changing the underlying
-proof. Discharged via `subst hg` and `bochner_weitzenboeck`. -/
-theorem bochner_weitzenboeck_g
     [IsManifold I 2 M]
     (g : RiemannianMetric I M) (hg : g = hm.metric)
     (f : M → ℝ) (hf : ContMDiff I 𝓘(ℝ, ℝ) ∞ f) (x : M) :
@@ -267,8 +239,9 @@ theorem bochner_weitzenboeck_g
           (manifoldGradient (I := I) g (Operators.scalarLaplacian g f) x)
       + ricciTensor g x (manifoldGradient (I := I) g f x)
                         (manifoldGradient (I := I) g f x) := by
-  subst hg
-  exact bochner_weitzenboeck f hf x
+  rw [bochner_leibniz_trace_reduction g hg f hf x,
+      bochner_connectionLaplacian_grad_decomposition g hg f hf x]
+  abel
 
 end Operators
 end Riemannian

OpenGALib/Riemannian/Operators/Bochner/PerSummand.lean

@@ -589,19 +589,5 @@ theorem bochner_connectionLaplacian_grad_decomposition
 -- composing this file's `bochner_connectionLaplacian_grad_decomposition`
 -- with the anchor's `bochner_leibniz_trace_reduction`.
 
-/-- **Math.** **Explicit-`g` form of the heart-of-Bochner reduction**. -/
-theorem bochner_connectionLaplacian_grad_decomposition_g
-    [IsManifold I 2 M] [T2Space M]
-    (g : RiemannianMetric I M) (hg : g = hm.metric)
-    (f : M → ℝ) (hf : ContMDiff I 𝓘(ℝ, ℝ) ∞ f) (x : M) :
-    g.metricInner x (connectionLaplacian g (manifoldGradient (I := I) g f) x)
-        (manifoldGradient (I := I) g f x)
-      = g.metricInner x (manifoldGradient (I := I) g f x)
-            (manifoldGradient (I := I) g (Operators.scalarLaplacian g f) x)
-        + ricciTensor g x (manifoldGradient (I := I) g f x)
-                          (manifoldGradient (I := I) g f x) := by
-  subst hg
-  exact bochner_connectionLaplacian_grad_decomposition HasMetric.metric rfl f hf x
-
 end Operators
 end Riemannian

OpenGALib/Riemannian/Operators/ConnectionLaplacian.lean

@@ -415,8 +415,8 @@ where $B_i := \mathrm{smoothOrthoFrame}\,g\,\alpha\,i$.
 noncomputable def connectionLaplacian
     (Z : VectorFieldSection I M) (α : M) : TangentSpace I α :=
   ∑ i, secondCovDerivSection (I := I) (M := M) g Z
-        (Riemannian.Tensor.smoothOrthoFrame (I := I) hm.metric α i)
-        (Riemannian.Tensor.smoothOrthoFrame (I := I) hm.metric α i) α
+        (Riemannian.Tensor.smoothOrthoFrame (I := I) g α i)
+        (Riemannian.Tensor.smoothOrthoFrame (I := I) g α i) α
 
 /-- **Math.** The connection Laplacian on the zero vector field is zero. -/
 @[simp] theorem connectionLaplacian_zero (α : M) :
@@ -427,15 +427,15 @@ noncomputable def connectionLaplacian
   intro i _
   show secondCovDerivSection g (I := I) (M := M)
         (0 : VectorFieldSection I M)
-        (Riemannian.Tensor.smoothOrthoFrame (I := I) hm.metric α i)
-        (Riemannian.Tensor.smoothOrthoFrame (I := I) hm.metric α i) α = 0
+        (Riemannian.Tensor.smoothOrthoFrame (I := I) g α i)
+        (Riemannian.Tensor.smoothOrthoFrame (I := I) g α i) α = 0
   unfold secondCovDerivSection
   have h_inner_zero : ∀ y v, covDerivAt g (0 : VectorFieldSection I M) y v = 0 := by
     intro y v
     show ((leviCivitaConnection (I := I) (M := M) g).toFun 0 y) v = 0
     rw [CovariantDerivative.zero]; rfl
   have h_section_zero : (fun y : M => covDerivAt g (0 : VectorFieldSection I M) y
-        ((Riemannian.Tensor.smoothOrthoFrame (I := I) hm.metric α i) y))
+        ((Riemannian.Tensor.smoothOrthoFrame (I := I) g α i) y))
       = (0 : VectorFieldSection I M) := by
     funext y; exact h_inner_zero y _
   rw [h_section_zero]

OpenGALib/Riemannian/Util/ConnectionLaplacianSimp.lean

@@ -32,8 +32,8 @@ variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [InnerProductSpa
     (Z : VectorFieldSection I M) (α : M) :
     connectionLaplacian (I := I) (M := M) g Z α =
       ∑ i, Riemannian.Operators.secondCovDerivSection (I := I) (M := M) g Z
-        (Riemannian.Tensor.smoothOrthoFrame (I := I) hm.metric α i)
-        (Riemannian.Tensor.smoothOrthoFrame (I := I) hm.metric α i) α :=
+        (Riemannian.Tensor.smoothOrthoFrame (I := I) g α i)
+        (Riemannian.Tensor.smoothOrthoFrame (I := I) g α i) α :=
   rfl
 
 end Operators