9g (part 2): drop Riem, ‖·‖²_g, II, (∇R)— last typeclass-dispatch notations

OpenGALib/Riemannian/Connection/LeviCivita.lean

@@ -660,12 +660,6 @@ noncomputable def riemannCurvature
   covDeriv g X (covDeriv g Y Z) x - covDeriv g Y (covDeriv g X Z) x
     - covDeriv g (mlieBracket I X Y) Z x
 
-/-- **Math.** Notation `Riem(X, Y) Z` for `riemannCurvature (HasMetric.metric) X Y Z`.
-The notation pipes the ambient `[HasMetric I M]` metric so downstream code
-continues to write `Riem(X, Y) Z` unchanged during Phase 1. -/
-scoped[Riemannian] notation:max "Riem(" X ", " Y ") " Z:max =>
-  riemannCurvature (HasMetric.metric) X Y Z
-
 /-! ### `riem_simp` lemmas
 
 Two rewrites that drive the `riem_simp` simp set, populated for the
@@ -703,7 +697,7 @@ theorem covDeriv_mlieBracket_swap_apply
       ((leviCivitaConnection (I := I) (M := M) g).toFun Z x).map_neg]
 
 -- riemannCurvature_antisymm lives in Curvature.lean: its statement
--- uses the post-Bianchi `Riem(X, Y) Z` notation, so it must be in a
+-- uses the post-Bianchi `riemannCurvature HasMetric.metric X Y Z` notation, so it must be in a
 -- file that imports `Util/Notation/Curvature`.
 
 /-! ## Algebraic Bianchi I
@@ -920,14 +914,11 @@ 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 :=
-  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
+  covDeriv HasMetric.metric X.toFun (riemannCurvature HasMetric.metric Y Z W) x
+    - riemannCurvature HasMetric.metric (covDeriv HasMetric.metric X Y) Z.toFun W.toFun x
+    - riemannCurvature HasMetric.metric Y.toFun (covDeriv HasMetric.metric X Z) W.toFun x
+    - riemannCurvature HasMetric.metric Y.toFun Z.toFun (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 =>
-  covDerivRiemann X Y Z W
 
 /-- **Math.** **Second (differential) Bianchi identity** for the
 Levi-Civita connection:
@@ -948,7 +939,7 @@ Estimated 80-120 LOC; repair tracked separately. -/
 theorem bianchi_second
     [IsManifold I 3 M]
     (X Y Z W : SmoothVectorField I M) (x : M) :
-    (∇R)[X](Y, Z) W x + (∇R)[Y](Z, X) W x + (∇R)[Z](X, Y) W x = 0 := by
+    covDerivRiemann X Y Z W x + covDerivRiemann Y Z X W x + covDerivRiemann Z X Y W x = 0 := by
   sorry
 
 end Riemannian

OpenGALib/Riemannian/Curvature/RiemannCurvature.lean

@@ -3,7 +3,7 @@ import OpenGALib.Riemannian.Connection.LeviCivita
 import OpenGALib.Riemannian.TangentBundle.TangentSmooth
 import OpenGALib.Riemannian.Operators.HessianLie
 import OpenGALib.Riemannian.Util.MetricInnerSmoothness
--- `Riem(X, Y) Z` notation is now defined inline in `Connection.lean`
+-- `riemannCurvature HasMetric.metric X Y Z` notation is now defined inline in `Connection.lean`
 -- alongside `riemannCurvature`; it transitively reaches us via the
 -- `import OpenGALib.Riemannian.Connection.LeviCivita` above.
 import Mathlib.LinearAlgebra.Trace
@@ -583,8 +583,8 @@ theorem riemannCurvature_metric_skew
     [IsManifold I 2 M]
     (X Y Z W : SmoothVectorField I M) (x : M)
     (h_interior : extChartAt I x x ∈ closure (interior (Set.range I))) :
-    metricInner x (Riem(X.toFun, Y.toFun) Z.toFun x) (W x)
-      + metricInner x (Riem(X.toFun, Y.toFun) W.toFun x) (Z x) = 0 := by
+    metricInner x (riemannCurvature HasMetric.metric X.toFun Y.toFun Z.toFun x) (W x)
+      + metricInner x (riemannCurvature HasMetric.metric X.toFun Y.toFun W.toFun x) (Z x) = 0 := by
   -- Diagonal-zero applied to U = Z+W, Z, W.
   have h_ZW := riemannCurvature_inner_self_zero HasMetric.metric X Y (Z + W) x h_interior
   have h_Z := riemannCurvature_inner_self_zero HasMetric.metric X Y Z x h_interior
@@ -614,21 +614,21 @@ Reference: do Carmo §4 Proposition 2.5 (iv); Petersen Ch. 3. -/
 theorem riemannCurvature_pair_symm
     [IsManifold I 2 M]
     (X Y Z W : SmoothVectorField I M) (x : M) :
-    metricInner x (Riem(X, Y) Z x) (W x)
-      = metricInner x (Riem(Z, W) X x) (Y x) := by
+    metricInner x (riemannCurvature HasMetric.metric X Y Z x) (W x)
+      = metricInner x (riemannCurvature HasMetric.metric Z W X x) (Y x) := by
   -- Strict-interior hypothesis used by `riemannCurvature_metric_skew`.
   have h_interior : extChartAt I x x ∈ closure (interior (Set.range I)) := by
     rw [ModelWithCorners.Boundaryless.range_eq_univ, interior_univ, closure_univ]
     exact Set.mem_univ _
   -- Four cyclic Bianchi I instances, paired with the respective 4th vector.
   have bianchi_inner : ∀ (A B C D : SmoothVectorField I M),
-      metricInner x (Riem(A, B) C x) (D x)
-        + metricInner x (Riem(B, C) A x) (D x)
-        + metricInner x (Riem(C, A) B x) (D x) = 0 := by
+      metricInner x (riemannCurvature HasMetric.metric A B C x) (D x)
+        + metricInner x (riemannCurvature HasMetric.metric B C A x) (D x)
+        + metricInner x (riemannCurvature HasMetric.metric C A B x) (D x) = 0 := by
     intro A B C D
     have h := bianchi_first HasMetric.metric A B C x
     have : metricInner x
-              (Riem(A, B) C x + Riem(B, C) A x + Riem(C, A) B x) (D x)
+              (riemannCurvature HasMetric.metric A B C x + riemannCurvature HasMetric.metric B C A x + riemannCurvature HasMetric.metric C A B x) (D x)
             = metricInner x (0 : TangentSpace I x) (D x) := by rw [h]
     rw [metricInner_add_left, metricInner_add_left] at this
     -- `metricInner x 0 (D x) = 0`.
@@ -643,14 +643,14 @@ theorem riemannCurvature_pair_symm
   have b4 := bianchi_inner W X Y Z
   -- (1,2)-antisymmetry, scalar form via metricInner congrArg.
   have antisym12 : ∀ (A B C D : SmoothVectorField I M),
-      metricInner x (Riem(A, B) C x) (D x)
-        = -metricInner x (Riem(B, A) C x) (D x) := by
+      metricInner x (riemannCurvature HasMetric.metric A B C x) (D x)
+        = -metricInner x (riemannCurvature HasMetric.metric B A C x) (D x) := by
     intro A B C D
     rw [riemannCurvature_antisymm HasMetric.metric A B C x, metricInner_neg_left]
   -- (3,4)-antisymmetry from `riemannCurvature_metric_skew`.
   have antisym34 : ∀ (A B C D : SmoothVectorField I M),
-      metricInner x (Riem(A, B) C x) (D x)
-        = -metricInner x (Riem(A, B) D x) (C x) := by
+      metricInner x (riemannCurvature HasMetric.metric A B C x) (D x)
+        = -metricInner x (riemannCurvature HasMetric.metric A B D x) (C x) := by
     intro A B C D
     have h := riemannCurvature_metric_skew A B C D x h_interior
     linarith
@@ -786,7 +786,7 @@ already consume the metric through the typeclass. -/
 /-- **Math.** The ambient Riemannian metric is **flat** if its Riemann
 curvature tensor vanishes pointwise. -/
 def IsFlat : Prop :=
-  ∀ (X Y Z : VectorFieldSection I M) (x : M), Riem(X, Y) Z x = 0
+  ∀ (X Y Z : VectorFieldSection I M) (x : M), riemannCurvature HasMetric.metric X Y Z x = 0
 
 /-! ## Killing vector fields -/
 
@@ -921,7 +921,7 @@ private lemma second_covDeriv_commutator
         - covDeriv HasMetric.metric (fun y => covDeriv HasMetric.metric U.toFun V.toFun y) X.toFun x)
       - (covDeriv HasMetric.metric V.toFun (fun y => covDeriv HasMetric.metric U.toFun X.toFun y) x
         - covDeriv HasMetric.metric (fun y => covDeriv HasMetric.metric V.toFun U.toFun y) X.toFun x)
-      = Riem(U, V) X x := by
+      = riemannCurvature HasMetric.metric U V X x := by
   rw [riemannCurvature_commutator_form]
   have h_torsion := covDeriv_sub_swap_eq_mlieBracket HasMetric.metric U.toFun V.toFun x
     (U.smoothAt x) (V.smoothAt x)
@@ -942,7 +942,7 @@ of constant-sectional-curvature manifolds.
 
 With OpenGA's convention
 `Riem(U,V)X = ∇_U∇_V X - ∇_V∇_U X - ∇_[U,V] X`, the right-hand side is
-`Riem(Y, X) Z`, equivalently `-Riem(X, Y) Z`.
+`riemannCurvature HasMetric.metric Y X Z`, equivalently `-riemannCurvature HasMetric.metric X Y Z`.
 
 Reference: do Carmo, *Riemannian Geometry*, §3 Ex. 5; Petersen, Ch. 8 §2;
 Cheeger–Ebin §1.84. -/
@@ -951,7 +951,7 @@ theorem IsKilling.second_covDeriv_eq_curvature
     (Y Z : SmoothVectorField I M) (x : M) :
     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
+      = riemannCurvature HasMetric.metric Y X Z x := by
   classical
   apply (metricInner_eq_iff_eq x _ _).mp
   intro w
@@ -961,7 +961,7 @@ theorem IsKilling.second_covDeriv_eq_curvature
       (covDeriv HasMetric.metric U.toFun (fun y => covDeriv HasMetric.metric V.toFun X.toFun y) x
         - covDeriv HasMetric.metric (fun y => covDeriv HasMetric.metric U.toFun V.toFun y) X.toFun x) (W x)
   let C (U V W : SmoothVectorField I M) : ℝ :=
-    metricInner x (Riem(U, V) X x) (W x)
+    metricInner x (riemannCurvature HasMetric.metric U V X x) (W x)
   have h_skew_Y : A Y Z W + A Y W Z = 0 := by
     simpa [A] using IsKilling.second_covDeriv_inner_skew X hX Y Z W x
   have h_skew_Z : A Z W Y + A Z Y W = 0 := by
@@ -976,7 +976,7 @@ theorem IsKilling.second_covDeriv_eq_curvature
             - covDeriv HasMetric.metric (fun y => covDeriv HasMetric.metric Y.toFun Z.toFun y) X.toFun x)
           - (covDeriv HasMetric.metric Z.toFun (fun y => covDeriv HasMetric.metric Y.toFun X.toFun y) x
             - covDeriv HasMetric.metric (fun y => covDeriv HasMetric.metric Z.toFun Y.toFun y) X.toFun x)) (W x)
-        = metricInner x (Riem(Y, Z) X x) (W x) at h
+        = metricInner x (riemannCurvature HasMetric.metric Y Z X x) (W x) at h
     rw [metricInner_sub_left] at h
     simpa [A, C] using h
   have h_comm_ZW : A Z W Y - A W Z Y = C Z W Y := by
@@ -987,7 +987,7 @@ theorem IsKilling.second_covDeriv_eq_curvature
             - covDeriv HasMetric.metric (fun y => covDeriv HasMetric.metric Z.toFun W.toFun y) X.toFun x)
           - (covDeriv HasMetric.metric W.toFun (fun y => covDeriv HasMetric.metric Z.toFun X.toFun y) x
             - covDeriv HasMetric.metric (fun y => covDeriv HasMetric.metric W.toFun Z.toFun y) X.toFun x)) (Y x)
-        = metricInner x (Riem(Z, W) X x) (Y x) at h
+        = metricInner x (riemannCurvature HasMetric.metric Z W X x) (Y x) at h
     rw [metricInner_sub_left] at h
     simpa [A, C] using h
   have h_comm_WY : A W Y Z - A Y W Z = C W Y Z := by
@@ -998,31 +998,31 @@ theorem IsKilling.second_covDeriv_eq_curvature
             - covDeriv HasMetric.metric (fun y => covDeriv HasMetric.metric W.toFun Y.toFun y) X.toFun x)
           - (covDeriv HasMetric.metric Y.toFun (fun y => covDeriv HasMetric.metric W.toFun X.toFun y) x
             - covDeriv HasMetric.metric (fun y => covDeriv HasMetric.metric Y.toFun W.toFun y) X.toFun x)) (Z x)
-        = metricInner x (Riem(W, Y) X x) (Z x) at h
+        = metricInner x (riemannCurvature HasMetric.metric W Y X x) (Z x) at h
     rw [metricInner_sub_left] at h
     simpa [A, C] using h
   have h_curv : C Y Z W - C Z W Y + C W Y Z
-      = 2 * metricInner x (Riem(Y, X) Z x) (W x) := by
+      = 2 * metricInner x (riemannCurvature HasMetric.metric Y X Z x) (W x) := by
     have h_bianchi := bianchi_first HasMetric.metric X W Y x
     have h_inner :
-        metricInner x (Riem(X, W) Y x + Riem(W, Y) X x + Riem(Y, X) W x) (Z x)
+        metricInner x (riemannCurvature HasMetric.metric X W Y x + riemannCurvature HasMetric.metric W Y X x + riemannCurvature HasMetric.metric Y X W x) (Z x)
           = 0 := by
       rw [h_bianchi]
       exact metricInner_zero_left x (Z x)
     rw [metricInner_add_left, metricInner_add_left] at h_inner
-    have h_pair₁ : C Y Z W = metricInner x (Riem(X, W) Y x) (Z x) := by
+    have h_pair₁ : C Y Z W = metricInner x (riemannCurvature HasMetric.metric X W Y x) (Z x) := by
       simpa [C] using riemannCurvature_pair_symm Y Z X W x
-    have h_pair₂ : C Z W Y = metricInner x (Riem(X, Y) Z x) (W x) := by
+    have h_pair₂ : C Z W Y = metricInner x (riemannCurvature HasMetric.metric X Y Z x) (W x) := by
       simpa [C] using riemannCurvature_pair_symm Z W X Y x
-    have h_pair₃ : C W Y Z = metricInner x (Riem(X, Z) W x) (Y x) := by
+    have h_pair₃ : C W Y Z = metricInner x (riemannCurvature HasMetric.metric X Z W x) (Y x) := by
       simpa [C] using riemannCurvature_pair_symm W Y X Z x
     have h_antisym12 :
-        metricInner x (Riem(X, Y) Z x) (W x)
-          = -metricInner x (Riem(Y, X) Z x) (W x) := by
+        metricInner x (riemannCurvature HasMetric.metric X Y Z x) (W x)
+          = -metricInner x (riemannCurvature HasMetric.metric Y X Z x) (W x) := by
       rw [riemannCurvature_antisymm HasMetric.metric X.toFun Y.toFun Z.toFun x, metricInner_neg_left]
     have h_antisym34 :
-        metricInner x (Riem(Y, X) W x) (Z x)
-          = -metricInner x (Riem(Y, X) Z x) (W x) := by
+        metricInner x (riemannCurvature HasMetric.metric Y X W x) (Z x)
+          = -metricInner x (riemannCurvature HasMetric.metric Y X Z x) (W x) := by
       have h := riemannCurvature_metric_skew Y X W Z x (by
         rw [ModelWithCorners.Boundaryless.range_eq_univ, interior_univ, closure_univ]
         exact Set.mem_univ _)
@@ -1031,7 +1031,7 @@ theorem IsKilling.second_covDeriv_eq_curvature
     linarith [h_inner, h_antisym12, h_antisym34]
   have h_A : 2 * A Y Z W = C Y Z W - C Z W Y + C W Y Z := by
     linarith [h_skew_Y, h_skew_Z, h_skew_W, h_comm_YZ, h_comm_ZW, h_comm_WY]
-  have h_target : A Y Z W = metricInner x (Riem(Y, X) Z x) (W x) := by
+  have h_target : A Y Z W = metricInner x (riemannCurvature HasMetric.metric Y X Z x) (W x) := by
     linarith [h_A, h_curv]
   simpa [A, hW_def] using h_target
 
@@ -1058,7 +1058,7 @@ independent (denominator non-zero). At linearly dependent inputs, the
 formula returns the junk value $0$ via division by zero. -/
 noncomputable def sectionalCurvature
     (X Y : VectorFieldSection I M) (x : M) : ℝ :=
-  metricInner x (Riem(X, Y) Y x) (X x) /
+  metricInner x (riemannCurvature HasMetric.metric X Y Y x) (X x) /
     (metricInner x (X x) (X x) * metricInner x (Y x) (Y x)
       - metricInner x (X x) (Y x) ^ 2)
 

OpenGALib/Riemannian/Operators/Bochner.lean

@@ -56,14 +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 : ℝ) * (Operators.scalarLaplacian (I := I) HasMetric.metric (‖manifoldGradient (I := I) HasMetric.metric f‖²_g)) x
+    (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)
-        + ‖Operators.hessianBilin (I := I) HasMetric.metric f‖²_g x := by
+        + frobeniusSq (I := I) (M := M) (Operators.hessianBilin (I := I) HasMetric.metric f) 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 (‖manifoldGradient (I := I) HasMetric.metric f‖²_g) x
+  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
       = metricInner x
           (connectionLaplacian (I := I) (M := M) HasMetric.metric (manifoldGradient (I := I) HasMetric.metric f) x)
           (manifoldGradient (I := I) HasMetric.metric f x)
@@ -75,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 (‖manifoldGradient (I := I) HasMetric.metric f‖²_g) x
-        = ∑ i, hessian (I := I) (M := M) HasMetric.metric (‖manifoldGradient (I := I) HasMetric.metric f‖²_g)
+      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
+        = ∑ i, hessian (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)))
             (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 (‖manifoldGradient (I := I) HasMetric.metric f‖²_g)) x = _
+        (hessianBilin (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 = _
     unfold laplacian
     rw [trace_def]
     rw [← Riemannian.Tensor.sum_diagonal_smoothOrthoFrame_eq_std (I := I) x
-          (hessianBilin (I := I) HasMetric.metric (‖manifoldGradient (I := I) HasMetric.metric f‖²_g) x)]
+          (hessianBilin (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)]
     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 (‖manifoldGradient (I := I) HasMetric.metric f‖²_g)
+      (1 / 2 : ℝ) * hessian (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)))
         (Bi i).toFun (Bi i).toFun x
       = metricInner x
             (secondCovDerivSection (I := I) (M := M) HasMetric.metric
@@ -241,8 +241,8 @@ 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 (‖manifoldGradient (I := I) HasMetric.metric f‖²_g)) x =
-      ‖Operators.hessianBilin (I := I) HasMetric.metric f‖²_g x
+    (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

OpenGALib/Riemannian/Operators/Hessian.lean

@@ -396,11 +396,4 @@ variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [InnerProductSpa
   {M : Type*} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I ∞ M] [T2Space M]
   [HasMetric I M]
 
-/-- **Math.** Frobenius squared norm on `(0,2)`-tensor sections, w.r.t. a $g$-orthonormal
-frame: `‖B‖²_g x = ∑_{ij} B(x)(εᵢ, εⱼ)²` where $\{\varepsilon_i\}$ is the
-`stdOrthonormalBasis` of $T_x M$ (geometric Hilbert-Schmidt norm). -/
-noncomputable instance instMetricNormSqBilin :
-    MetricNormSq (Riemannian.Operators.Bilin (M := M) I) (M → ℝ) where
-  normSqG B := fun x => Riemannian.Operators.frobeniusSq (I := I) (M := M) B x
-
 end Riemannian