circleAverage_log_norm_sub_const₂

English

If ‖a‖ > 1, then circleAverage(log ‖· − a‖) 0 1 = log ‖a‖.

Русский

Если ‖a‖ > 1, то circleAverage(log ‖z − a‖) 0 1 = log ‖a‖.

LaTeX

$$$$\|a\| > 1 \implies circleAverage(\log \|\cdot - a\|)\,0\,1 = \log \|a\|.$$$$

Lean4

/-- If `a : ℂ` has norm greater than one, then `circleAverage (log ‖· - a‖) 0 1` equals `log ‖a‖`.
-/
@[simp]
theorem circleAverage_log_norm_sub_const₂ (h : 1 < ‖a‖) : circleAverage (log ‖· - a‖) 0 1 = log ‖a‖ :=
  by
  rw [HarmonicOnNhd.circleAverage_eq, zero_sub, norm_neg]
  intro x hx
  apply AnalyticAt.harmonicAt_log_norm (by fun_prop)
  rw [sub_ne_zero]
  by_contra!
  simp_all only [abs_one, Metric.mem_closedBall, dist_zero_right]
  linarith

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