comp_CLM — Mathlib

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

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