laplacian_eq_iteratedFDeriv_complexPlane

English

Special case of standard formula for functions on ℂ with real inner product structure.

Русский

Особый случай стандартной формулы для функций на ℂ с реальной структурой скалярного произведения.

LaTeX

$$Δ f = f''(z) при z ∈ ℂ с базисом (1,i)$$

Lean4

/-- Special case of the standard formula for functions on `ℂ`, with the standard real inner product
structure.
-/
theorem laplacian_eq_iteratedFDeriv_complexPlane (f : ℂ → F) :
    Δ f = fun x ↦ iteratedFDeriv ℝ 2 f x ![1, 1] + iteratedFDeriv ℝ 2 f x ![Complex.I, Complex.I] := by
  simp [laplacian_eq_iteratedFDeriv_orthonormalBasis f Complex.orthonormalBasisOneI]

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