A radial argument on the upper half disk

Mathlib has no Cauchy theorem for a half disk. This file replaces it, for the one function A015 needs, by differentiating the half-circle mean with respect to the radius.

Let F be holomorphic on the open unit disk, and put H(ρ) = ∫₀^π F(ρ e^{iθ}) dθ. Differentiating under the integral sign and then integrating in θ, H'(ρ) = ∫₀^π F'(ρ e^{iθ}) e^{iθ} dθ = (F(ρ e^{iπ}) - F(ρ)) / (iρ) = i (F(ρ) - F(-ρ))/ρ.

For F(z) = log³((1+z)/2) the values F(±ρ) are real, so h(ρ) = Im H(ρ) has derivative (F(ρ) - F(-ρ))/ρ and h(0) = 0. At ρ = 1 the function h is continuous by dominated convergence: for ρ > 1/2, |1 + ρ e^{iθ}| ≥ ρ sin θ bounds |Re log((1 + ρ e^{iθ})/2)| by log 4 + |log sin θ|, and Im log³ = 3 Re² Im - Im³ only involves the square of the real part, which is integrable.

Main results

• LeanPolyLog.Radial.hasDerivAt_integral: for F with a continuous derivative F' on the unit disk and |ρ| < 1, d/dρ ∫₀^π F(ρ e^{iθ}) dθ = ∫₀^π F'(ρ e^{iθ}) e^{iθ} dθ.
• LeanPolyLog.Radial.integral_deriv_mul_exp: for 0 < |ρ| < 1, ∫₀^π F'(ρ e^{iθ}) e^{iθ} dθ = i (F(ρ) - F(-ρ))/ρ.
• LeanPolyLog.Radial.integral_im_logCube: ∫₀^π Im log³((1 + e^{iθ})/2) dθ = ∫₀¹ (log³((1+r)/2) - log³((1-r)/2))/r dr, provided the integrand on the right is integrable on [0, 1].
• LeanPolyLog.Radial.im_logCube_exp_two_mul: for |x| < π/2, Im log³((1 + e^{2ix})/2) = 3x log² cos x - x³, because log((1 + e^{2ix})/2) = log cos x + ix.

theorem LeanPolyLog.Radial.norm_ofReal_mul_exp (ρ θ : ℝ) : ‖↑ρ * Complex.exp (↑θ * Complex.I)‖ = |ρ|

‖ρ e^{iθ}‖ = |ρ|.

Holomorphic functions on the unit disk

theorem LeanPolyLog.Radial.hasDerivAt_integral {F F' : ℂ → ℂ} (hF : ∀ z ∈ Metric.ball 0 1, HasDerivAt F (F' z) z) (hF' : ContinuousOn F' (Metric.ball 0 1)) {ρ₀ : ℝ} (hρ₀ : |ρ₀| < 1) : HasDerivAt (fun (ρ : ℝ) => ∫ (θ : ℝ) in 0..Real.pi, F (↑ρ * Complex.exp (↑θ * Complex.I))) (∫ (θ : ℝ) in 0..Real.pi, F' (↑ρ₀ * Complex.exp (↑θ * Complex.I)) * Complex.exp (↑θ * Complex.I)) ρ₀

Differentiation under the integral sign: if F has the continuous derivative F' on the unit disk, then for |ρ₀| < 1, d/dρ ∫₀^π F(ρ e^{iθ}) dθ = ∫₀^π F'(ρ₀ e^{iθ}) e^{iθ} dθ at ρ₀.

theorem LeanPolyLog.Radial.integral_deriv_mul_exp {F F' : ℂ → ℂ} (hF : ∀ z ∈ Metric.ball 0 1, HasDerivAt F (F' z) z) (hF' : ContinuousOn F' (Metric.ball 0 1)) {ρ : ℝ} (hρ0 : ρ ≠ 0) (hρ : |ρ| < 1) : ∫ (θ : ℝ) in 0..Real.pi, F' (↑ρ * Complex.exp (↑θ * Complex.I)) * Complex.exp (↑θ * Complex.I) = Complex.I * (F ↑ρ - F (-↑ρ)) / ↑ρ

The fundamental theorem of calculus in θ: for 0 < |ρ| < 1, ∫₀^π F'(ρ e^{iθ}) e^{iθ} dθ = (F(-ρ) - F(ρ))/(iρ) = i (F(ρ) - F(-ρ))/ρ.

The function log³((1+z)/2)

theorem LeanPolyLog.Radial.one_add_ne_zero {z : ℂ} (hz : ‖z‖ < 1) : 1 + z ≠ 0

For ‖z‖ < 1, 1 + z ≠ 0.

theorem LeanPolyLog.Radial.mem_slitPlane {z : ℂ} (hz : ‖z‖ < 1) : (1 + z) / 2 ∈ Complex.slitPlane

For ‖z‖ < 1, (1 + z)/2 lies in the slit plane: its real part is positive.

theorem LeanPolyLog.Radial.hasDerivAt_logCube {z : ℂ} (hz : z ∈ Metric.ball 0 1) : HasDerivAt (fun (z : ℂ) => Complex.log ((1 + z) / 2) ^ 3) (3 * Complex.log ((1 + z) / 2) ^ 2 / (1 + z)) z

d/dz log³((1+z)/2) = 3 log²((1+z)/2)/(1+z) on the unit disk.

theorem LeanPolyLog.Radial.continuousOn_deriv_logCube : ContinuousOn (fun (z : ℂ) => 3 * Complex.log ((1 + z) / 2) ^ 2 / (1 + z)) (Metric.ball 0 1)

3 log²((1+z)/2)/(1+z) is continuous on the unit disk.

theorem LeanPolyLog.Radial.logCube_ofReal {ρ : ℝ} (hρ : -1 ≤ ρ) : Complex.log ((1 + ↑ρ) / 2) ^ 3 = ↑(Real.log ((1 + ρ) / 2) ^ 3)

On real arguments ρ ≥ -1, log³((1+ρ)/2) is the real log³((1+ρ)/2).

theorem LeanPolyLog.Radial.logCube_neg_ofReal {ρ : ℝ} (hρ : ρ ≤ 1) : Complex.log ((1 + -↑ρ) / 2) ^ 3 = ↑(Real.log ((1 - ρ) / 2) ^ 3)

On real arguments ρ ≤ 1, log³((1-ρ)/2) is the real log³((1-ρ)/2).

The half-circle mean of Im log³((1+z)/2)

noncomputable def LeanPolyLog.Radial.halfCircleIm (ρ : ℝ) : ℝ

halfCircleIm ρ = ∫₀^π Im log³((1 + ρ e^{iθ})/2) dθ.

Equations

• LeanPolyLog.Radial.halfCircleIm ρ = ∫ (θ : ℝ) in 0..Real.pi, (Complex.log ((1 + ↑ρ * Complex.exp (↑θ * Complex.I)) / 2) ^ 3).im

theorem LeanPolyLog.Radial.continuous_logCube_mul_exp {ρ : ℝ} (hρ : |ρ| < 1) : Continuous fun (θ : ℝ) => Complex.log ((1 + ↑ρ * Complex.exp (↑θ * Complex.I)) / 2) ^ 3

For |ρ| < 1, θ ↦ log³((1 + ρ e^{iθ})/2) is continuous.

theorem LeanPolyLog.Radial.halfCircleIm_eventuallyEq {ρ₀ : ℝ} (hρ₀ : |ρ₀| < 1) : halfCircleIm =ᶠ[nhds ρ₀] fun (ρ : ℝ) => (∫ (θ : ℝ) in 0..Real.pi, Complex.log ((1 + ↑ρ * Complex.exp (↑θ * Complex.I)) / 2) ^ 3).im

Near any |ρ| < 1, halfCircleIm is the imaginary part of ∫₀^π log³((1 + ρ e^{iθ})/2) dθ.

theorem LeanPolyLog.Radial.hasDerivAt_integral_logCube {ρ : ℝ} (hρ : |ρ| < 1) : HasDerivAt (fun (ρ : ℝ) => ∫ (θ : ℝ) in 0..Real.pi, Complex.log ((1 + ↑ρ * Complex.exp (↑θ * Complex.I)) / 2) ^ 3) (∫ (θ : ℝ) in 0..Real.pi, 3 * Complex.log ((1 + ↑ρ * Complex.exp (↑θ * Complex.I)) / 2) ^ 2 / (1 + ↑ρ * Complex.exp (↑θ * Complex.I)) * Complex.exp (↑θ * Complex.I)) ρ

The complex half-circle mean has a derivative at every |ρ| < 1.

theorem LeanPolyLog.Radial.hasDerivAt_halfCircleIm {ρ : ℝ} (hρ0 : 0 < ρ) (hρ1 : ρ < 1) : HasDerivAt halfCircleIm ((Real.log ((1 + ρ) / 2) ^ 3 - Real.log ((1 - ρ) / 2) ^ 3) / ρ) ρ

For 0 < ρ < 1, halfCircleIm' ρ = (log³((1+ρ)/2) - log³((1-ρ)/2))/ρ.

theorem LeanPolyLog.Radial.halfCircleIm_zero : halfCircleIm 0 = 0

halfCircleIm 0 = 0: the integrand is Im log³(1/2) = 0.

theorem LeanPolyLog.Radial.im_pow_three (z : ℂ) : (z ^ 3).im = 3 * z.re ^ 2 * z.im - z.im ^ 3

The imaginary part of z³ is 3 (Re z)² Im z - (Im z)³.

theorem LeanPolyLog.Radial.abs_im_logCube_le {ρ θ : ℝ} (hρ : ρ ∈ Set.Ioc (1 / 2) 1) (hθ : θ ∈ Set.Ioo 0 Real.pi) : ‖(Complex.log ((1 + ↑ρ * Complex.exp (↑θ * Complex.I)) / 2) ^ 3).im‖ ≤ 3 * Real.pi * (2 * Real.log 4 ^ 2 + 2 * Real.log (Real.sin θ) ^ 2) + Real.pi ^ 3

For 1/2 < ρ ≤ 1 and 0 < θ < π: |Im log³((1 + ρ e^{iθ})/2)| ≤ 3π (2 log² 4 + 2 log² sin θ) + π³.

theorem LeanPolyLog.Radial.ae_ne_pi : ∀ᵐ (θ : ℝ), θ ≠ Real.pi

Almost every θ differs from π.

theorem LeanPolyLog.Radial.continuousWithinAt_halfCircleIm_one : ContinuousWithinAt halfCircleIm (Set.Icc 0 1) 1

halfCircleIm is continuous at 1 within [0, 1], by dominated convergence.

theorem LeanPolyLog.Radial.continuousOn_halfCircleIm : ContinuousOn halfCircleIm (Set.Icc 0 1)

halfCircleIm is continuous on [0, 1].

theorem LeanPolyLog.Radial.integral_im_logCube (hint : IntervalIntegrable (fun (r : ℝ) => (Real.log ((1 + r) / 2) ^ 3 - Real.log ((1 - r) / 2) ^ 3) / r) MeasureTheory.volume 0 1) : ∫ (θ : ℝ) in 0..Real.pi, (Complex.log ((1 + Complex.exp (↑θ * Complex.I)) / 2) ^ 3).im = ∫ (r : ℝ) in 0..1, (Real.log ((1 + r) / 2) ^ 3 - Real.log ((1 - r) / 2) ^ 3) / r

The radial identity: if (log³((1+r)/2) - log³((1-r)/2))/r is integrable on [0, 1], then ∫₀^π Im log³((1 + e^{iθ})/2) dθ = ∫₀¹ (log³((1+r)/2) - log³((1-r)/2))/r dr.

The boundary values

theorem LeanPolyLog.Radial.log_one_add_exp_two_mul {x : ℝ} (hx : |x| < Real.pi / 2) : Complex.log ((1 + Complex.exp (↑(2 * x) * Complex.I)) / 2) = ↑(Real.log (Real.cos x)) + ↑x * Complex.I

For |x| < π/2: log((1 + e^{2ix})/2) = log cos x + ix, since (1 + e^{2ix})/2 = cos x · e^{ix} with cos x > 0.

theorem LeanPolyLog.Radial.im_logCube_exp_two_mul {x : ℝ} (hx : |x| < Real.pi / 2) : (Complex.log ((1 + Complex.exp (↑(2 * x) * Complex.I)) / 2) ^ 3).im = 3 * x * Real.log (Real.cos x) ^ 2 - x ^ 3

For |x| < π/2: Im log³((1 + e^{2ix})/2) = 3x log² cos x - x³.