English
Laplacian within a subset s is defined by tensoring the second iterated derivative with a canonical tensor.
Русский
Лапласиан внутри множества s определяется тензорованием второго повторного производного с каноническим тензором.
LaTeX
$$$\Delta[s] f := tensorIteratedFDerivWithinTwo \mathbb{R} f s$$$
Lean4
/-- Laplacian for functions on real inner product spaces, with respect to a set `s`. Use `open
InnerProductSpace` to access the notation `Δ[s]` for `InnerProductSpace.LaplacianWithin`.
-/
noncomputable def laplacianWithin : E → F := fun x ↦
tensorIteratedFDerivWithinTwo ℝ f s x (InnerProductSpace.canonicalCovariantTensor E)