harmonicAt_conj — Mathlib

English

If f is complex-analytic without zero, then log of the norm of f is harmonic.

Русский

Если f комплексно-аналитична без нуля, то log нормы f гармоничен.

LaTeX

$$$\operatorname{HarmonicAt}(\log \|f\|, x) \text{ under appropriate analytic assumptions}$$$

Lean4

/-- If `f : ℂ → ℂ` is complex-analytic, then its complex conjugate is harmonic.
-/
theorem harmonicAt_conj {f : ℂ → ℂ} (h : AnalyticAt ℂ f x) : HarmonicAt (conj f) x :=
  (harmonicAt_comp_CLE_iff conjCLE).2 h.harmonicAt

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