laplacianWithin_univ — Mathlib

English

Equality of Laplacian with iteratedFDerivWithin orthonormal basis expression.

Русский

Согласование лапласиана с выражением через ортонормированный базис и итеративные производные.

LaTeX

$$Δ[s] f = ∑ i iteratedFDerivWithin 2 f s e_i e_i$$

Lean4

/-- The Laplacian equals the Laplacian with respect to `Set.univ`.
-/
@[simp]
theorem laplacianWithin_univ : Δ[(Set.univ : Set E)]f = Δ f :=
  by
  ext x
  simp [laplacian, tensorIteratedFDerivTwo, bilinearIteratedFDerivTwo, laplacianWithin, tensorIteratedFDerivWithinTwo,
    bilinearIteratedFDerivWithinTwo]

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