laplacianWithin — Mathlib

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)

Похожие утверждения