English
If g is analytic on a neighborhood of a closed ball and g never vanishes there, then circleAverage(log ||g||) equals log ||g|| evaluated at the center.
Русский
Если g аналитична на окрестности замкнутого шара и нигде не обнуляется, то среднее по окружности логарифм нормы g равно логарифму нормы g в центре.
LaTeX
$$$\forall R c g,\ AnalyticOnNhd(\mathbb{C}, g, \overline{\text{Ball}}) \to (\forall u \in \overline{\text{Ball}}, g(u) \neq 0) \Rightarrow \ circleAverage(\log ||g||) c R = \log ||g(c)||$$$
Lean4
/-- If `g : ℂ → ℂ` is analytic without zero on the closed ball with center `c` and radius `R`, then the
circle average `circleAverage (log ‖g ·‖) c R` equals `log ‖g c‖`.
-/
@[simp]
theorem circleAverage_log_norm_of_ne_zero {R : ℝ} {c : ℂ} {g : ℂ → ℂ} (h₁g : AnalyticOnNhd ℂ g (closedBall c |R|))
(h₂g : ∀ u ∈ closedBall c |R|, g u ≠ 0) : circleAverage (Real.log ‖g ·‖) c R = Real.log ‖g c‖ :=
HarmonicOnNhd.circleAverage_eq (fun x hx ↦ (h₁g x hx).harmonicAt_log_norm (h₂g x hx))
