English
If f has no zeros, log of the norm of f is harmonic.
Русский
Если у f нет нулей, log нормы f гармоничен.
LaTeX
$$$\operatorname{HarmonicAt}(\log \|f\|, x)$ under £no-zero condition$$$
Lean4
/-- If `f : ℂ → ℂ` is complex-analytic without zero, then `log ‖f‖` is harmonic.
-/
theorem harmonicAt_log_norm {f : ℂ → ℂ} {z : ℂ} (h₁f : AnalyticAt ℂ f z) (h₂f : f z ≠ 0) :
HarmonicAt (Real.log ‖f ·‖) z :=
by
have : (Real.log ‖f ·‖) = (2 : ℝ)⁻¹ • (Real.log ∘ Complex.normSq ∘ f) :=
by
funext z
simp only [Pi.smul_apply, Function.comp_apply, smul_eq_mul]
rw [Complex.norm_def, Real.log_sqrt]
linarith
exact (f z).normSq_nonneg
rw [this]
apply HarmonicAt.const_smul
by_cases h₃f : f z ∈ Complex.slitPlane
· exact analyticAt_harmonicAt_log_normSq h₁f h₂f h₃f
· rw [(by aesop : Complex.normSq ∘ f = Complex.normSq ∘ (-f))]
exact
analyticAt_harmonicAt_log_normSq h₁f.neg (by simpa) ((mem_slitPlane_or_neg_mem_slitPlane h₂f).resolve_left h₃f)
