laplacian — Mathlib

English

In the real setting, Laplacian within a set reduces to second derivative within the set.

Русский

В реальном случае лапласиан внутри множества равен вторичной производной внутри множества.

LaTeX

$$Δ[s] f = iteratedDerivWithin 2 f s$$

Lean4

/-- Laplacian for functions on real inner product spaces. Use `open InnerProductSpace` to access the
notation `Δ` for `InnerProductSpace.Laplacian`.
-/
noncomputable def laplacian : E → F := fun x ↦
  tensorIteratedFDerivTwo ℝ f x (InnerProductSpace.canonicalCovariantTensor E)

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