9g (part 1): drop 9 _g typeclass-dispatch notations

OpenGALib/Riemannian/Connection/LeviCivita.lean

@@ -325,13 +325,6 @@ noncomputable def covDeriv
     TangentSpace I x :=
   ((leviCivitaConnection (I := I) (M := M) g).toFun Y x) (X x)
 
-/-- **Math.** Notation `∇[X] Y` for `covDeriv (HasMetric.metric) X Y`. The
-notation pipes the ambient `[HasMetric I M]` metric so downstream code
-continues to write `∇[X] Y` unchanged during Phase 1 (typeclass retained
-until #19). -/
-scoped[Riemannian] notation:max "∇[" X "] " Y:max =>
-  covDeriv (HasMetric.metric) X Y
-
 /-- **Math.** Notation `⟦X, Y⟧` for the manifold Lie bracket
 `mlieBracket _ X Y` (model `I` inferred from section types). -/
 scoped[Riemannian] notation:max "⟦" X ", " Y "⟧" =>
@@ -927,10 +920,10 @@ This is the standard $(1,4)$-tensor covariant-derivative pattern: $\nabla$
 acts on each slot of $R$ as a derivation. -/
 noncomputable def covDerivRiemann
     (X Y Z W : SmoothVectorField I M) (x : M) : TangentSpace I x :=
-  (∇[X] (Riem(Y, Z) W)) x
-    - Riem(∇[X] Y, Z) W x
-    - Riem(Y, ∇[X] Z) W x
-    - Riem(Y, Z) (∇[X] W) x
+  covDeriv HasMetric.metric X.toFun (Riem(Y, Z) W) x
+    - Riem(covDeriv HasMetric.metric X Y, Z) W x
+    - Riem(Y, covDeriv HasMetric.metric X Z) W x
+    - Riem(Y, Z) (covDeriv HasMetric.metric X W) x
 
 /-- **Math.** Notation `(∇R)[X](Y, Z) W` for `covDerivRiemann X Y Z W`. -/
 scoped[Riemannian] notation:max "(∇R)[" X "](" Y ", " Z ") " W:max =>

OpenGALib/Riemannian/Curvature/RicciTensorBundle.lean

@@ -552,18 +552,7 @@ noncomputable def scalarCurvature
     (g : RiemannianMetric I M) (x : M) : ℝ :=
   LinearMap.trace ℝ (TangentSpace I x) (ricciSharp (I := I) (M := M) g x)
 
-/-- **Math.** Notation `scal_g[I]` for the scalar curvature on the ambient
-`[HasMetric I M]` metric. `I` is bracketed because `x : M` does not expose
-the model with corners. The notation pipes `HasMetric.metric` so downstream
-consumers continue to write `scal_g[I] x` during Phase 1 (typeclass
-retained until #19). -/
-scoped[Riemannian] notation:max "scal_g[" I "]" =>
-  scalarCurvature (I := I) (HasMetric.metric)
 
-/-- **Math.** Notation `Ric_g(v, w) x` for `ricciTensor HasMetric.metric x v w`
-on the ambient `[HasMetric I M]` metric. -/
-scoped[Riemannian] notation:max "Ric_g(" v ", " w ") " x:max =>
-  ricciTensor (HasMetric.metric) x v w
 
 /-! ## Ricci-flat and Einstein metric predicates
 
@@ -575,7 +564,7 @@ explicit argument because the underlying notations (`Ric_g`,
 /-- **Math.** The ambient Riemannian metric is **Ricci-flat** if its
 Ricci tensor vanishes pointwise. -/
 def IsRicciFlat : Prop :=
-  ∀ (x : M) (V W : TangentSpace I x), Ric_g(V, W) x = 0
+  ∀ (x : M) (V W : TangentSpace I x), ricciTensor HasMetric.metric x V W = 0
 
 /-- **Math.** The ambient Riemannian metric is **Einstein** if its Ricci
 tensor is a constant scalar multiple of the metric:
@@ -585,7 +574,7 @@ fixed real constant $c$ (the *Einstein constant*).
 Reference: do Carmo §4 Ex. 6; Petersen Ch. 3 §6. -/
 def IsEinstein : Prop :=
   ∃ c : ℝ, ∀ (x : M) (V W : TangentSpace I x),
-    Ric_g(V, W) x = c * metricInner x V W
+    ricciTensor HasMetric.metric x V W = c * metricInner x V W
 
 end Riemannian
 

OpenGALib/Riemannian/Curvature/RiemannCurvature.lean

@@ -215,13 +215,6 @@ noncomputable def ricci
     (X Y : SmoothVectorField I M) (x : M) : ℝ :=
   LinearMap.trace ℝ (TangentSpace I x) (curvatureEndo g X Y x)
 
-/-- **Math.** The Ricci curvature as a scalar function on the manifold:
-`(Ric(X, Y))(x) = ricci HasMetric.metric X Y x`. The notation pipes the
-ambient `[HasMetric I M]` metric so downstream consumers continue to
-write `Ric(X, Y)` unchanged during Phase 1 (typeclass retained). -/
-scoped[Riemannian] notation:max "Ric(" X ", " Y ")" =>
-  ricci (HasMetric.metric) X Y
-
 /-! ### Diagonal `(3,4)` vanishing: $g(R(X,Y)Z, Z) = 0$
 
 do Carmo §4 Proposition 2.5(iii) closure. The proof reduces, via metric
@@ -759,12 +752,12 @@ theorem ricci_symm
   set b := stdOrthonormalBasis ℝ (TangentSpace I x) with hb_def
   -- Expand each Ricci scalar as `∑ i, ⟪b i, R(const b i, ·) · x⟫_ℝ` via
   -- `LinearMap.trace_eq_sum_inner`.
-  have h_RXY : Ric(X, Y) x =
+  have h_RXY : ricci HasMetric.metric X Y x =
       ∑ i, ⟪b i, riemannCurvature HasMetric.metric (fun _ : M => (b i : E)) X.toFun Y.toFun x⟫_ℝ := by
     show LinearMap.trace ℝ (TangentSpace I x)
           (curvatureEndo (HasMetric.metric) X Y x) = _
     exact LinearMap.trace_eq_sum_inner _ b
-  have h_RYX : Ric(Y, X) x =
+  have h_RYX : ricci HasMetric.metric Y X x =
       ∑ i, ⟪b i, riemannCurvature HasMetric.metric (fun _ : M => (b i : E)) Y.toFun X.toFun x⟫_ℝ := by
     show LinearMap.trace ℝ (TangentSpace I x)
           (curvatureEndo (HasMetric.metric) Y X x) = _
@@ -806,7 +799,7 @@ is by isometries).
 Reference: do Carmo §3 Ex. 5; Petersen Ch. 8. -/
 def IsKilling (X : SmoothVectorField I M) : Prop :=
   ∀ (U W : SmoothVectorField I M) (y : M),
-    metricInner y ((∇[U] X) y) (W y) + metricInner y ((∇[W] X) y) (U y) = 0
+    metricInner y ((covDeriv HasMetric.metric U X) y) (W y) + metricInner y ((covDeriv HasMetric.metric W X) y) (U y) = 0
 
 /-- **Math.** Covariantly differentiating the Killing equation.
 
@@ -956,7 +949,9 @@ Cheeger–Ebin §1.84. -/
 theorem IsKilling.second_covDeriv_eq_curvature
     (X : SmoothVectorField I M) (hX : IsKilling X)
     (Y Z : SmoothVectorField I M) (x : M) :
-    (∇[Y] (∇[Z] X)) x - (∇[∇[Y] Z] X) x = Riem(Y, X) Z x := by
+    covDeriv HasMetric.metric Y.toFun (covDeriv HasMetric.metric Z X) x
+      - covDeriv HasMetric.metric (covDeriv HasMetric.metric Y Z) X.toFun x
+      = Riem(Y, X) Z x := by
   classical
   apply (metricInner_eq_iff_eq x _ _).mp
   intro w
@@ -1067,10 +1062,6 @@ noncomputable def sectionalCurvature
     (metricInner x (X x) (X x) * metricInner x (Y x) (Y x)
       - metricInner x (X x) (Y x) ^ 2)
 
-/-- **Math.** Notation `K_g[I](X, Y)` for `sectionalCurvature X Y`. -/
-scoped[Riemannian] notation:max "K_g[" I "](" X ", " Y ")" =>
-  sectionalCurvature (I := I) X Y
-
 /-- **Math.** **Tangent-vector form** of sectional curvature: same
 formula as `sectionalCurvature` but consuming the pointwise tangent
 vectors $v, w \in T_xM$ directly via constant-section lifts. Useful when
@@ -1093,7 +1084,7 @@ Denominator: symmetric in $X, Y$ via `metricInner_comm`. -/
 theorem sectionalCurvature_symmetric
     [IsManifold I 2 M]
     (X Y : SmoothVectorField I M) (x : M) :
-    K_g[I](X, Y) x = K_g[I](Y, X) x := by
+    sectionalCurvature (I := I) X Y x = sectionalCurvature (I := I) Y X x := by
   unfold sectionalCurvature
   congr 1
   · -- Numerator: g(R(X,Y) Y, X) = g(R(Y,X) X, Y) via pair-symmetry + double antisym.

OpenGALib/Riemannian/Operators/Bochner.lean

@@ -56,12 +56,14 @@ Combines `hessian_gradientNormSq_apply_chartFrame` summed over
 theorem bochner_leibniz_trace_reduction
     [IsManifold I 2 M]
     (f : M → ℝ) (hf : ContMDiff I 𝓘(ℝ, ℝ) ∞ f) (x : M) :
-    (1 / 2 : ℝ) * (Δ_g[I] ‖grad_g[I] f‖²_g) x
-      = ⟪connectionLaplacian HasMetric.metric (grad_g[I] f) x, (grad_g[I] f) x⟫_g
-        + ‖hess_g[I] f‖²_g x := by
+    (1 / 2 : ℝ) * (Operators.scalarLaplacian (I := I) HasMetric.metric (‖manifoldGradient (I := I) HasMetric.metric f‖²_g)) x
+      = HasMetric.metric.metricInner x
+            (connectionLaplacian HasMetric.metric (manifoldGradient (I := I) HasMetric.metric f) x)
+            ((manifoldGradient (I := I) HasMetric.metric f) x)
+        + ‖Operators.hessianBilin (I := I) HasMetric.metric f‖²_g x := by
   classical
   have h_grad := manifoldGradient_smooth_of_smooth HasMetric.metric f hf
-  show (1 / 2 : ℝ) * Operators.scalarLaplacian (I := I) (M := M) HasMetric.metric (‖grad_g[I] f‖²_g) x
+  show (1 / 2 : ℝ) * Operators.scalarLaplacian (I := I) (M := M) HasMetric.metric (‖manifoldGradient (I := I) HasMetric.metric f‖²_g) x
       = metricInner x
           (connectionLaplacian (I := I) (M := M) HasMetric.metric (manifoldGradient (I := I) HasMetric.metric f) x)
           (manifoldGradient (I := I) HasMetric.metric f x)
@@ -73,23 +75,23 @@ theorem bochner_leibniz_trace_reduction
   -- Step 1: convert `scalarLaplacian` from std-basis trace to smoothOrthoFrame trace
   -- via Stage 7 basis-invariance of trace (`sum_diagonal_smoothOrthoFrame_eq_std`).
   have h_scalarLap_eq :
-      Operators.scalarLaplacian (I := I) (M := M) HasMetric.metric (‖grad_g[I] f‖²_g) x
-        = ∑ i, hessian (I := I) (M := M) HasMetric.metric (‖grad_g[I] f‖²_g)
+      Operators.scalarLaplacian (I := I) (M := M) HasMetric.metric (‖manifoldGradient (I := I) HasMetric.metric f‖²_g) x
+        = ∑ i, hessian (I := I) (M := M) HasMetric.metric (‖manifoldGradient (I := I) HasMetric.metric f‖²_g)
             (Bi i).toFun (Bi i).toFun x := by
     rw [scalarLaplacian_eq_laplacian_hessianBilin HasMetric.metric]
     show laplacian (I := I) (M := M)
-        (hessianBilin (I := I) HasMetric.metric (‖grad_g[I] f‖²_g)) x = _
+        (hessianBilin (I := I) HasMetric.metric (‖manifoldGradient (I := I) HasMetric.metric f‖²_g)) x = _
     unfold laplacian
     rw [trace_def]
     rw [← Riemannian.Tensor.sum_diagonal_smoothOrthoFrame_eq_std (I := I) x
-          (hessianBilin (I := I) HasMetric.metric (‖grad_g[I] f‖²_g) x)]
+          (hessianBilin (I := I) HasMetric.metric (‖manifoldGradient (I := I) HasMetric.metric f‖²_g) x)]
     refine Finset.sum_congr rfl ?_
     intro i _
     rfl
   rw [h_scalarLap_eq, Finset.mul_sum]
   -- Step 2: per-summand section-form Hess identity (`hessian_gradientNormSq_apply_section`).
   have h_summand : ∀ i,
-      (1 / 2 : ℝ) * hessian (I := I) (M := M) HasMetric.metric (‖grad_g[I] f‖²_g)
+      (1 / 2 : ℝ) * hessian (I := I) (M := M) HasMetric.metric (‖manifoldGradient (I := I) HasMetric.metric f‖²_g)
         (Bi i).toFun (Bi i).toFun x
       = metricInner x
             (secondCovDerivSection (I := I) (M := M) HasMetric.metric
@@ -239,10 +241,11 @@ 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 : ℝ) * (Δ_g[I] ‖grad_g[I] f‖²_g) x =
-      ‖hess_g[I] f‖²_g x
-      + ⟪(grad_g[I] f) x, (grad_g[I] (Δ_g[I] f)) x⟫_g
-      + Ric_g((grad_g[I] f) x, (grad_g[I] f) x) x := by
+    (1 / 2 : ℝ) * (Operators.scalarLaplacian (I := I) HasMetric.metric (‖manifoldGradient (I := I) HasMetric.metric f‖²_g)) x =
+      ‖Operators.hessianBilin (I := I) HasMetric.metric f‖²_g 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 f hf x]
   abel

OpenGALib/Riemannian/Operators/Bochner/BochnerExpansion.lean

@@ -61,7 +61,7 @@ endomorphism. -/
 theorem ricciTensor_eq_sum_inner_orthonormal
     [IsManifold I 2 M]
     (x : M) (V W : TangentSpace I x) :
-    Ric_g(V, W) x =
+    ricciTensor HasMetric.metric x V W =
       ∑ i, ⟪(stdOrthonormalBasis ℝ (TangentSpace I x)) i,
             curvatureEndo (HasMetric.metric)
               (SmoothVectorField.const (I := I) (M := M) V)
@@ -339,7 +339,7 @@ theorem heart_curvature_orthonormal_sum_eq_ricci
           (Riemannian.Tensor.smoothOrthoFrame (I := I) hm.metric x i)
           W.toFun (manifoldGradient (I := I) HasMetric.metric f) x)
         (Riemannian.Tensor.smoothOrthoFrame (I := I) hm.metric x i x)
-      = Ric_g(manifoldGradient (I := I) HasMetric.metric f x, W.toFun x) x := by
+      = ricciTensor HasMetric.metric x (manifoldGradient (I := I) HasMetric.metric f x) (W.toFun x) := by
   classical
   have h_interior : extChartAt I x x ∈ closure (interior (Set.range I)) := by
     rw [ModelWithCorners.Boundaryless.range_eq_univ, interior_univ, closure_univ]
@@ -401,7 +401,7 @@ theorem heart_curvature_orthonormal_sum_eq_ricci
     _ = ∑ i, Φ ((stdOrthonormalBasis ℝ (TangentSpace I x)) i)
                 ((stdOrthonormalBasis ℝ (TangentSpace I x)) i) :=
         Riemannian.Tensor.sum_diagonal_smoothOrthoFrame_eq_std (I := I) x Φ
-    _ = Ric_g(W.toFun x, gradF.toFun x) x := by
+    _ = ricciTensor HasMetric.metric x (W.toFun x) (gradF.toFun x) := by
         rw [ricciTensor_eq_sum_inner_orthonormal x (W.toFun x) (gradF.toFun x)]
         apply Finset.sum_congr rfl
         intro i _
@@ -413,7 +413,7 @@ theorem heart_curvature_orthonormal_sum_eq_ricci
             = ⟪(stdOrthonormalBasis ℝ (TangentSpace I x)) i,
                 curvatureEndo (HasMetric.metric) WV GV x ((stdOrthonormalBasis ℝ (TangentSpace I x)) i)⟫_ℝ
         exact real_inner_comm _ _
-    _ = Ric_g(gradF.toFun x, W.toFun x) x := by
+    _ = ricciTensor HasMetric.metric x (gradF.toFun x) (W.toFun x) := by
         show ricciTensor (HasMetric.metric) x (W.toFun x) (gradF.toFun x)
           = ricciTensor (HasMetric.metric) x (gradF.toFun x) (W.toFun x)
         show ricci (HasMetric.metric) WV GV x
@@ -431,7 +431,7 @@ theorem sum_hessianBilin_smoothOrthoFrame_eventuallyEq_laplacian
     (fun b => ∑ i, hessianBilin (I := I) HasMetric.metric f b
                     (Riemannian.Tensor.smoothOrthoFrame (I := I) hm.metric x i b)
                     (Riemannian.Tensor.smoothOrthoFrame (I := I) hm.metric x i b))
-      =ᶠ[𝓝 x] (Δ_g[I] f : M → ℝ) := by
+      =ᶠ[𝓝 x] (Operators.scalarLaplacian (I := I) HasMetric.metric f : M → ℝ) := by
   filter_upwards [Riemannian.Tensor.smoothOrthoFrameNbhd_mem_nhds (I := I) (M := M) x]
     with b hb
   -- At b ∈ nbhd, basis-invariance of trace of `hessianBilin f b`.
@@ -656,17 +656,17 @@ theorem sum_inner_secondCovDerivAt_grad_smoothOrthoFrame_of_inner_form
             (Riemannian.Tensor.smoothOrthoFrame (I := I) hm.metric x i x)
             (Riemannian.Tensor.smoothOrthoFrame (I := I) hm.metric x i x))
           w
-        = metricInner x (manifoldGradient (I := I) HasMetric.metric (Δ_g[I] f) x) w
-          + Ric_g(manifoldGradient (I := I) HasMetric.metric f x, w) x) :
+        = metricInner x (manifoldGradient (I := I) HasMetric.metric (Operators.scalarLaplacian (I := I) HasMetric.metric f) x) w
+          + ricciTensor HasMetric.metric x (manifoldGradient (I := I) HasMetric.metric f x) w) :
     ∑ i, metricInner x
         (secondCovDerivAt (I := I) (M := M) HasMetric.metric (manifoldGradient (I := I) HasMetric.metric f) x
           (Riemannian.Tensor.smoothOrthoFrame (I := I) hm.metric x i x)
           (Riemannian.Tensor.smoothOrthoFrame (I := I) hm.metric x i x))
         (manifoldGradient (I := I) HasMetric.metric f x)
       = metricInner x (manifoldGradient (I := I) HasMetric.metric f x)
-            (manifoldGradient (I := I) HasMetric.metric (Δ_g[I] f) x)
-        + Ric_g((manifoldGradient (I := I) HasMetric.metric f x),
-                (manifoldGradient (I := I) HasMetric.metric f x)) x := by
+            (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
   classical
   -- Specialise hInner at w = ∇f x.
   have h := hInner (manifoldGradient (I := I) HasMetric.metric f x)
@@ -685,15 +685,15 @@ theorem sum_inner_secondCovDerivAt_grad_smoothOrthoFrame_of_inner_form
             (Riemannian.Tensor.smoothOrthoFrame (I := I) hm.metric x i x))
           (manifoldGradient (I := I) HasMetric.metric f x) :=
         (sum_inner Finset.univ _ (manifoldGradient (I := I) HasMetric.metric f x)).symm
-    _ = metricInner x (manifoldGradient (I := I) HasMetric.metric (Δ_g[I] f) x)
+    _ = metricInner x (manifoldGradient (I := I) HasMetric.metric (Operators.scalarLaplacian (I := I) HasMetric.metric f) x)
             (manifoldGradient (I := I) HasMetric.metric f x)
-          + Ric_g(manifoldGradient (I := I) HasMetric.metric f x,
-                  manifoldGradient (I := I) HasMetric.metric f x) x := h
+          + ricciTensor HasMetric.metric x (manifoldGradient (I := I) HasMetric.metric f x)
+                                            (manifoldGradient (I := I) HasMetric.metric f x) := h
     _ = metricInner x (manifoldGradient (I := I) HasMetric.metric f x)
-            (manifoldGradient (I := I) HasMetric.metric (Δ_g[I] f) x)
-          + Ric_g(manifoldGradient (I := I) HasMetric.metric f x,
-                  manifoldGradient (I := I) HasMetric.metric f x) x := by
-        rw [metricInner_comm x (manifoldGradient (I := I) HasMetric.metric (Δ_g[I] 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 [metricInner_comm x (manifoldGradient (I := I) HasMetric.metric (Operators.scalarLaplacian (I := I) HasMetric.metric f) x)]
 
 end Operators
 end Riemannian