English
Generalization: circleAverage(log ‖· − a‖) c R equals log R plus the positive part of (R⁻¹ times ‖c − a‖), i.e. circleAverage(log ‖· − a‖) c R = log R + log⁺(R⁻¹ · ‖c − a‖) for R ≠ 0.
Русский
Обобщение: circleAverage(log ‖· − a‖) c R = log R + log⁺(R⁻¹ · ‖c − a‖) при R ≠ 0.
LaTeX
$$$$R \neq 0 \;\Rightarrow\; circleAverage(\log \|\cdot - a\|)\, c\, R = \log R + \log^+ \bigl(R^{-1} \|c - a\|\bigr).$$$$
Lean4
/-- Generalization of `circleAverage_log_norm_sub_const_eq_posLog`: The
`circleAverage (log ‖· - a‖) c R` equals `log R + log⁺ (|R|⁻¹ * ‖c - a‖)`.
-/
theorem circleAverage_log_norm_sub_const_eq_log_radius_add_posLog (hR : R ≠ 0) :
circleAverage (log ‖· - a‖) c R = log R + log⁺ (R⁻¹ * ‖c - a‖) := by
calc
circleAverage (log ‖· - a‖) c R
_ = circleAverage (fun z ↦ log ‖R * (z + R⁻¹ * (c - a))‖) 0 1 :=
by
rw [circleAverage_eq_circleAverage_zero_one]
congr
ext z
congr
rw [Complex.ofReal_inv R]
field_simp [Complex.ofReal_ne_zero.mpr hR]
ring
_ = circleAverage (fun z ↦ log ‖R‖ + log ‖z + R⁻¹ * (c - a)‖) 0 1 :=
by
apply circleAverage_congr_codiscreteWithin _ (zero_ne_one' ℝ).symm
have : {z | ‖z + ↑R⁻¹ * (c - a)‖ ≠ 0} ∈ codiscreteWithin (Metric.sphere (0 : ℂ) |1|) :=
by
apply codiscreteWithin_iff_locallyFiniteComplementWithin.2
intro z hz
use Set.univ
simp only [univ_mem, abs_one, Complex.ofReal_inv, ne_eq, norm_eq_zero, Set.univ_inter, true_and]
apply Set.Subsingleton.finite
intro z₁ hz₁ z₂ hz₂
simp_all only [ne_eq, abs_one, mem_sphere_iff_norm, sub_zero, Set.mem_diff, Set.mem_setOf_eq, Decidable.not_not]
rw [add_eq_zero_iff_eq_neg.1 hz₁.2, add_eq_zero_iff_eq_neg.1 hz₂.2]
filter_upwards [this] with z hz
rw [norm_mul, log_mul (norm_ne_zero_iff.2 (Complex.ofReal_ne_zero.mpr hR)) hz]
simp
_ = log R + log⁺ (|R|⁻¹ * ‖c - a‖) :=
by
rw [← Pi.add_def,
circleAverage_add (circleIntegrable_const (log ‖R‖) 0 1)
(circleIntegrable_log_norm_meromorphicOn (fun _ _ ↦ by fun_prop)),
circleAverage_const]
simp
_ = log R + log⁺ (R⁻¹ * ‖c - a‖) := by
congr 1
rcases hR.lt_or_gt with h | h
· simp [abs_of_neg h]
· rw [abs_of_pos h]
