Prove scalarLaplacian_mul (Laplace–Beltrami product rule)

[Xinze-Li-Moqian]

Statement to prove

OpenGALib/Riemannian/Operators/Laplacian.lean:149

theorem scalarLaplacian_mul (f g : M → ℝ) (x : M) :
    Δ_g[I] (f * g) x =
      Δ_g[I] f x * g x + 2 * ⟪grad_g[I] f x, grad_g[I] g x⟫_g + f x * Δ_g[I] g x := by
  sorry

Math

The Laplacian product rule

$$\Delta_g(fg) = (\Delta_g f) \cdot g + 2 \langle \nabla f, \nabla g \rangle_g + f \cdot (\Delta_g g).$$

PDE workhorse on Riemannian manifolds — appears in maximum principle, harmonic-function rigidity, Bochner estimates.

Repair plan (sketched in the docstring)

1. Unfold scalarLaplacian to its stdOrthonormalBasis trace form.
2. Apply mfderiv_mul + covDeriv Leibniz on each frame coordinate.
3. Use manifoldGradient_inner_eq to identify $df(\varepsilon_i) = \langle \nabla f, \varepsilon_i \rangle_g$.
4. Resum.

Standard textbook proof. Estimated 80–120 LOC.

Ground truth

• do Carmo §4 (warmup)
• Petersen Ch. 7 §1
• Schoen–Yau Lectures on Differential Geometry §1.1