English
In finite dimensions, given a commuting family of symmetric linear maps, the inner product space decomposes into joint eigenspaces with respect to those maps.
Русский
В конечномерном пространстве, данная коммутирующаяся совокупность симметричных отображений приводит к разложению пространства на общие собственные пространства по этим отображениям.
LaTeX
$$DirectSum.IsInternal (fun α => (Eig(T 1, α 1) ⊓ Eig(T 2, α 2))).$$
Lean4
/-- For a function on `ℝ`, the Laplacian is the second derivative: version within a set. -/
theorem laplacianWithin_eq_iteratedDerivWithin_real {e : ℝ} {s : Set ℝ} (f : ℝ → F) (hs : UniqueDiffOn ℝ s)
(he : e ∈ s) : (Δ[s]f) e = iteratedDerivWithin 2 f s e :=
by
simp only [laplacianWithin_eq_iteratedFDerivWithin_orthonormalBasis f hs he (OrthonormalBasis.singleton (Fin 1) ℝ),
Finset.univ_unique, Fin.default_eq_zero, Fin.isValue, OrthonormalBasis.singleton_apply, Finset.sum_const,
Finset.card_singleton, one_smul, iteratedDerivWithin_eq_iteratedFDerivWithin]
congr with i
fin_cases i <;> simp
