laplacianWithin_eq_iteratedFDerivWithin_stdOrthonormalBasis

English

A commuting family of symmetric endomorphisms decomposes space into joint eigenspaces as an internal direct sum.

Русский

Семейство симметричных эндоморфизмов, коммутирующее между собой, распадается на общие собственные пространства как внутренняя прямая сумма.

LaTeX

$$DirectSum.IsInternal (fun α => ⨅ i, (T i).eigenspace (α i))$$

Lean4

/-- Standard formula, computing the Laplacian from the standard orthonormal basis of a real inner
product space.
-/
theorem laplacianWithin_eq_iteratedFDerivWithin_stdOrthonormalBasis {e : E} (hs : UniqueDiffOn ℝ s) (he : e ∈ s) :
    (Δ[s]f) e = ∑ i, iteratedFDerivWithin ℝ 2 f s e ![(stdOrthonormalBasis ℝ E) i, (stdOrthonormalBasis ℝ E) i] := by
  apply laplacianWithin_eq_iteratedFDerivWithin_orthonormalBasis f hs he (stdOrthonormalBasis ℝ E)

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