Documentation

LeanPool.LeanComplexAnalysis.Harmonic.PoissonIntegral

The Poisson Integral Formula on the Unit Disc #

Main results #

Theorems poisson_integral_of_harmonicOn_unitDisc_continuousOn_closedUnitDisc and poisson_integral_of_harmonicOn_unitDisc_continuousOn_closedUnitDisc_re_kernel: Every function u : ℂ → ℝ harmonic on the unit disc and continuous on the closed unit disc can be represented as

u(z) = 1/(2π) ∫_0^{2π} (1 - |z|^2) / |e^{it} - z|^2 * u(e^{it}) dt
     = 1/(2π) ∫_0^{2π} Re((e^{it} + z) / (e^{it} - z)) * u(e^{it}) dt,

for z in the unit disc.

Theorem poisson_integral_of_analyticOn_unitDisc_continuousOn_closedUnitDisc and poisson_integral_of_analyticOn_unitDisc_continuousOn_closedUnitDisc_re_kernel: Every function f : ℂ → E analytic on the unit disc, continuous on the closed unit disc, with values in a complex Banach space E, can be represented as

f(z) = 1/(2π) ∫_0^{2π} (1 - |z|^2) / |e^{it} - z|^2 • f(e^{it}) dt
     = 1/(2π) ∫_0^{2π} Re((e^{it} + z) / (e^{it} - z)) • f(e^{it}) dt,

for z in the unit disc.

Implementation Notes #

The proof follows from the

References #

[Rudin, Real and Complex Analysis (Theorem 11.9)][rudin2006real]

Tags #

harmonic function, Poisson integral, analytic function, unit disc

Scaling a point in the closed unit ball by r ∈ (0,1) remains in the unit disc.

r* exp (t * I) is in the unit disc for r ∈ (0,1).

exp (t * I) is not equal to any z in the unit disc.

The conjugate of exp (t * I) is its inverse.

1 - star z * w ≠ 0, for z in unit disc and w in closed unit disc

theorem LeanPool.LeanComplexAnalysis.differentiableAt_of_analyticOn_unitDisc_of_mul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {z : } {r : } (hf : AnalyticOn f (Metric.ball 0 1)) (hz : z Metric.closedBall 0 1) (hr : r Set.Ioo 0 1) :
DifferentiableAt (fun (ζ : ) => f (r * ζ)) z

If f is analytic on the unit disc, then ζ ↦ f (r * ζ) is differentiable at z for r in (0,1) and z in the closed unit ball.

theorem LeanPool.LeanComplexAnalysis.cauchy_circleIntegral_formula_on_scaled_unitDisc {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] {f : E} {z : } {r : } (hf : AnalyticOn f (Metric.ball 0 1)) (hr : r Set.Ioo 0 1) (hz : z Metric.ball 0 1) :
f (r * z) = (1 / (2 * Real.pi * Complex.I)) (ζ : ) in C(0, 1), (1 / (ζ - z)) f (r * ζ)

Cauchy integral formula applied to f analytic on the unit disc at the point r*z, for r in (0,1) and z in the unit disc.

theorem LeanPool.LeanComplexAnalysis.cauchy_integral_formula_on_scaled_unitDisc {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] {f : E} {z : } {r : } (hf : AnalyticOn f (Metric.ball 0 1)) (hr : r Set.Ioo 0 1) (hz : z Metric.ball 0 1) :
f (r * z) = (1 / (2 * Real.pi)) (t : ) in 0..2 * Real.pi, (Complex.exp (t * Complex.I) / (Complex.exp (t * Complex.I) - z)) f (r * Complex.exp (t * Complex.I))

Cauchy's integral formula for analytic functions on the unit disc, evaluated at scaled points r * z with r ∈ (0,1).

theorem LeanPool.LeanComplexAnalysis.diffferentiableAt_goursat_integrand_scaled_unitDisc {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {z w : } {r : } (hf : AnalyticOn f (Metric.ball 0 1)) (hr : r Set.Ioo 0 1) (hz : z Metric.ball 0 1) (hw : w Metric.closedBall 0 1) :
DifferentiableAt (fun (ζ : ) => (star z / (Complex.I * (1 - star z * ζ))) f (r * ζ)) w

If f is analytic on the unit disc, then ζ ↦ (star z / (I * (1 - star z * ζ))) • f (r * ζ) is differentiable at w in the closed unit disc, for r in (0,1).

theorem LeanPool.LeanComplexAnalysis.vanishing_goursat_circleIntegral_scaled_unitDisc {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {z : } {r : } (hf : AnalyticOn f (Metric.ball 0 1)) (hr : r Set.Ioo 0 1) (hz : z Metric.ball 0 1) :
(w : ) in C(0, 1), (star z / (Complex.I * (1 - star z * w))) f (r * w) = 0

We apply the Cauchy-Goursat theorem to the function ζ ↦ (star z / (I * (1 - star z * ζ))) • (f (r * ζ))) on the unit circle.

An auxiliary identity that will be used in the integrand of the Cauchy-Goursat theorem.

theorem LeanPool.LeanComplexAnalysis.vanishing_goursat_integral_scaled_unitDisc {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {z : } {r : } (hf : AnalyticOn f (Metric.ball 0 1)) (hr : r Set.Ioo 0 1) (hz : z Metric.ball 0 1) :
(t : ) in 0..2 * Real.pi, (star z / (star (Complex.exp (t * Complex.I)) - star z)) f (r * Complex.exp (t * Complex.I)) = 0

Cauchy-Goursat theorem for the unit disc implies the integral of an analytic function against the conjugate Cauchy kernel vanishes.

theorem LeanPool.LeanComplexAnalysis.poisson_formula_of_analyticOn_scaled_unitDisc {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] {f : E} {z : } {r : } (hf : AnalyticOn f (Metric.ball 0 1)) (hr : r Set.Ioo 0 1) (hz : z Metric.ball 0 1) :
f (r * z) = (1 / (2 * Real.pi)) (t : ) in 0..2 * Real.pi, ((1 - z ^ 2) / Complex.exp (t * Complex.I) - z ^ 2) f (r * Complex.exp (t * Complex.I))

For an analytic function f : ℂ → E on the unit disc, f(r*z) equals the integral of f(r*e^{it}) against the Poisson kernel, where r ∈ (0,1) and z is in the unit disc.

theorem LeanPool.LeanComplexAnalysis.poisson_formula_of_harmonicOn_scaled_unitDisc {u : } {z : } {r : } (hu : InnerProductSpace.HarmonicOnNhd u (Metric.ball 0 1)) (hr : r Set.Ioo 0 1) (hz : z Metric.ball 0 1) :
u (r * z) = 1 / (2 * Real.pi) * (t : ) in 0..2 * Real.pi, (1 - z ^ 2) / Complex.exp (t * Complex.I) - z ^ 2 * u (r * Complex.exp (t * Complex.I))

For a harmonic function u on the unit disc, u(r*z) equals the integral of u(r*e^{it}) times the Poisson kernel, where r ∈ (0,1) and z is in the unit disc.

theorem LeanPool.LeanComplexAnalysis.bounds_of_continuousOn_unitCircle_closedUnitDisc {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {k : } {r t : } (hr : r Set.Ioo 0 1) (hf : ContinuousOn f (Metric.closedBall 0 1)) (hk : ContinuousOn k (Metric.sphere 0 1)) :
k (Complex.exp (t * Complex.I)) f (r * Complex.exp (t * Complex.I)) sSup ((fun (ζ : ) => |k ζ|) '' Metric.sphere 0 1) * sSup ((fun (w : ) => f w) '' Metric.closedBall 0 1)

We bound t ↦ ‖k (exp (t * I)) • f (r * exp (t * I))‖, for k continuous on the unit circle and f continuous on the closed unit disc.

theorem LeanPool.LeanComplexAnalysis.tendsto_integral_prod_of_continuousOn_unitCircle_closedUnitDisc {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {k : } {r : } (hf : ContinuousOn f (Metric.closedBall 0 1)) (hk : ContinuousOn k (Metric.sphere 0 1)) (hr : ∀ (n : ), r n Set.Ioo 0 1) (hr_lim : Filter.Tendsto r Filter.atTop (nhds 1)) :
Filter.Tendsto (fun (n : ) => (t : ) in 0..2 * Real.pi, k (Complex.exp (t * Complex.I)) f ((r n) * Complex.exp (t * Complex.I))) Filter.atTop (nhds ( (t : ) in 0..2 * Real.pi, k (Complex.exp (t * Complex.I)) f (Complex.exp (t * Complex.I))))

For a sequence r_n → 1 with r_n ∈ (0,1), the integral of t ↦ k(e^{it}) • f(r_n*e^{it}) on [0 , 2π] converges to the integral of t ↦ k(e^{it}) • f(e^{it}) on [0 , 2π], when f is continuous on the closed unit disc and k is continuous on the unit circle, by the Lebesgue Dominated Convergence Theorem.

The Poisson kernel is continuous on the unit circle.

theorem LeanPool.LeanComplexAnalysis.seq_tendsto_to_oneIn_unit_interval_aux :
have r := fun (n : ) => 1 - 1 / (n + 2); (∀ (n : ), r n Set.Ioo 0 1) Filter.Tendsto r Filter.atTop (nhds 1)

The sequence r_n = 1 - 1 / (n + 2) is in (0,1) and tends to 1 as n → ∞.

If r n tends to 1, then f (r n * z) tends to f z, for z in the unit disc, when f is continuous on the closed unit disc.

Poisson integral formula for harmonic functions on the unit disc: A function u harmonic on the unit disc and continuous on the closed unit disc satisfies u(z) = (1/2π) ∫_0^{2π} (1 - |z|²) / |e^{it} - z|² u(e^{it}) dt for z in the unit disc.

Poisson integral formula for analytic functions on the unit disc: A function f : ℂ → E analytic on the unit disc and continuous on the closed unit disc satisfies f(z) = (1/2π) ∫_0^{2π} (1 - |z|²) / |e^{it} - z|² f(e^{it}) dt for z in the unit disc.

The real part of the Herglotz–Riesz kernel is equal to the Poisson kernel.

Poisson integral formula for harmonic functions on the unit disc: A function u : ℂ → ℝ harmonic on the unit disc and continuous on the closed unit disc satisfies u(z) = (1/2π) ∫_0^{2π} Re((e^{it} + z) / (e^{it} - z)) * u(e^{it}) dt for z in the unit disc.

Poisson integral formula for analytic functions on the unit disc: A function f : ℂ → E analytic on the unit disc and continuous on the closed unit disc satisfies f(z) = (1/2π) ∫_0^{2π} Re((e^{it} + z) / (e^{it} - z)) • f(e^{it}) dt for z in the unit disc.