English
If a ∈ ℂ has norm less than 1, then the circle average of log ||· − a|| around 0 with radius 1 vanishes: circleAverage(log ||· − a||)0 1 = 0.
Русский
Если ‖a‖ < 1, то круговое среднее log ||z − a|| вокруг нуля радиуса 1 равно 0: circleAverage(log ||· − a||)0 1 = 0.
LaTeX
$$$$circleAverage(\log \|\cdot - a\|)\,0\,1 = 0\quad\text{if } \|a\| < 1.$$$$
Lean4
/-- If `a : ℂ` has norm smaller than one, then `circleAverage (log ‖· - a‖) 0 1` vanishes.
-/
@[simp]
theorem circleAverage_log_norm_sub_const₀ (h : ‖a‖ < 1) : circleAverage (log ‖· - a‖) 0 1 = 0 := by
calc
circleAverage (log ‖· - a‖) 0 1
_ = circleAverage (log ‖1 - ·⁻¹ * a‖) 0 1 :=
by
apply circleAverage_congr_sphere
intro z hz
simp_all only [abs_one, mem_sphere_iff_norm, sub_zero]
congr 1
have : z ≠ 0 := fun h ↦ by simp [h] at hz
calc
‖z - a‖
_ = ‖z⁻¹ * (z - a)‖ := by simp [hz]
_ = ‖1 - z⁻¹ * a‖ := by field_simp
_ = 0 :=
by
rw [circleAverage_zero_one_congr_inv (f := fun x ↦ log ‖1 - x * a‖), HarmonicOnNhd.circleAverage_eq, zero_mul,
sub_zero, CStarRing.norm_of_mem_unitary (unitary ℂ).one_mem, log_one]
intro x hx
have : ‖x * a‖ < 1 := by
calc
‖x * a‖
_ = ‖x‖ * ‖a‖ := by simp
_ ≤ ‖a‖ := (mul_le_of_le_one_left (norm_nonneg _) (by aesop))
_ < 1 := h
apply AnalyticAt.harmonicAt_log_norm (by fun_prop)
rw [sub_ne_zero]
by_contra! hCon
rwa [← hCon, CStarRing.norm_of_mem_unitary (unitary ℂ).one_mem, lt_self_iff_false] at this
