English
Composing a harmonic function with a continuous linear map yields a harmonic function at the same point.
Русский
Составление гармоничной функции с непрерывно линейным отображением сохраняет гармоничность в той же точке.
LaTeX
$$$\text{If } h:\, F\to G \text{ is a continuous linear map and } \operatorname{HarmonicAt}(f,x), \text{ then } \operatorname{HarmonicAt}(h\circ f,x)$$$
Lean4
/-- Compositions of continuous `ℝ`-linear maps with harmonic functions are harmonic.
-/
theorem comp_CLM (h : HarmonicAt f x) (l : F →L[ℝ] G) : HarmonicAt (l ∘ f) x :=
by
constructor
· exact h.1.continuousLinearMap_comp l
· filter_upwards [h.1.laplacian_CLM_comp_left_nhds (l := l), h.2]
simp_all