English
Composing a harmonic function on a neighborhood with a continuous linear map yields a harmonic function on that neighborhood.
Русский
Сочетание гармоничной функции на окрестности с непрерывно линейным отображением даёт гармоничную функцию на той же окрестности.
LaTeX
$$$\operatorname{HarmonicOnNhd}(f,s) \Rightarrow \operatorname{HarmonicOnNhd}(l\circ f,s)$$$
Lean4
/-- Continuously complex-differentiable functions on ℂ are harmonic.
-/
theorem harmonicAt (h : ContDiffAt ℂ 2 f x) : HarmonicAt f x :=
by
refine ⟨h.restrict_scalars ℝ, ?_⟩
filter_upwards [h.restrictScalars_iteratedFDeriv_eventuallyEq (𝕜 := ℝ)] with a ha
have : (iteratedFDeriv ℂ 2 f a) (I • ![1, 1]) = (∏ i, I) • ((iteratedFDeriv ℂ 2 f a) ![1, 1]) :=
(iteratedFDeriv ℂ 2 f a).map_smul_univ (fun _ ↦ I) ![1, 1]
simp_all [laplacian_eq_iteratedFDeriv_complexPlane f, ← ha, ContinuousMultilinearMap.coe_restrictScalars]
