Documentation

Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage

Representation of log⁺ as a Circle Average #

If a is any complex number, circleAverage_log_norm_sub_const_eq_posLog represents log⁺ a as the circle average of log ‖· - a‖ over the unit circle.

Circle Integrability #

source
theorem circleIntegrable_log_norm_sub_const {a c : ℂ} (r : ℝ) :
CircleIntegrable (fun (x : ℂ) => Real.log ‖x - a‖) c r

If a is any complex number, the function (log ‖· - a‖) is circle integrable over every circle.

Computing circleAverage (log ‖· - a‖) 0 1 in case where ‖a‖ < 1. #

source
@[simp]
theorem circleAverage_log_norm_sub_const₀ {a : ℂ} (h : ‖a‖ < 1) :
Real.circleAverage (fun (x : ℂ) => Real.log ‖x - a‖) 0 1 = 0

If a : ℂ has norm smaller than one, then circleAverage (log ‖· - a‖) 0 1 vanishes.

Computing circleAverage (log ‖· - a‖) 0 1 in case where ‖a‖ = 1. #

source
theorem circleAverage_log_norm_sub_const₁ {a : ℂ} (h : ‖a‖ = 1) :
Real.circleAverage (fun (x : ℂ) => Real.log ‖x - a‖) 0 1 = 0

If a : ℂ has norm one, then the circle average circleAverage (log ‖· - a‖) 0 1 vanishes.

Computing circleAverage (log ‖· - a‖) 0 1 in case where 1 < ‖a‖. #

source
@[simp]
theorem circleAverage_log_norm_sub_const₂ {a : ℂ} (h : 1 < ‖a‖) :
Real.circleAverage (fun (x : ℂ) => Real.log ‖x - a‖) 0 1 = Real.log ‖a‖

If a : ℂ has norm greater than one, then circleAverage (log ‖· - a‖) 0 1 equals log ‖a‖.

Presentation of log⁺ in Terms of Circle Averages #

source
@[simp]
theorem circleAverage_log_norm_sub_const_eq_posLog {a : ℂ} :
Real.circleAverage (fun (x : ℂ) => Real.log ‖x - a‖) 0 1 = ‖a‖.posLog

The circleAverage (log ‖· - a‖) 0 1 equals log⁺ ‖a‖.

source
@[simp]
theorem circleAverage_log_norm_add_const_eq_posLog {a : ℂ} :
Real.circleAverage (fun (x : ℂ) => Real.log ‖x + a‖) 0 1 = ‖a‖.posLog

The circleAverage (log ‖· + a‖) 0 1 equals log⁺ ‖a‖.

source
theorem circleAverage_log_norm_sub_const_eq_log_radius_add_posLog {a c : ℂ} {R : ℝ} (hR : R ≠ 0) :
Real.circleAverage (fun (x : ℂ) => Real.log ‖x - a‖) c R = Real.log R + (R⁻¹ * ‖c - a‖).posLog

Generalization of circleAverage_log_norm_sub_const_eq_posLog: The circleAverage (log ‖· - a‖) c R equals log R + log⁺ (|R|⁻¹ * ‖c - a‖).

source
theorem circleAverage_log_norm_sub_const_of_mem_closedBall {a c : ℂ} {R : ℝ} (hu : a ∈ Metric.closedBall c |R|) :
Real.circleAverage (fun (x : ℂ) => Real.log ‖x - a‖) c R = Real.log R

Trivial corollary of circleAverage_log_norm_sub_const_eq_log_radius_add_posLog: If u : ℂ lies within the closed ball with center c and radius R, then the circle average circleAverage (log ‖· - u‖) c R equals log R.