Documentation

LeanPool.LeanComplexAnalysis.Harmonic.PoissonIntegral2

The Poisson Integral Formula on Disc #

Main results #

Theorems poisson_integral_of_harmonicOn_disc_continuousOn_closedDisc and poisson_integral_of_harmonicOn_disc_continuousOn_closedDisc_ker_re: Every function u : ℂ → ℝ harmonic on the disc with radius R and center 0, and continuous on the closed disc, can be represented as

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

for z in the disc.

Theorem poisson_integral_of_diffContOnCl_disc and poisson_integral_of_diffContOnCl_disc_ker_re: Every function f : ℂ → E ℂ-differentiable on the disc with radius R and center 0, and continuous on the closed disc, with values in a complex Banach space E, can be represented as

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

for z in the disc.

Implementation Notes #

The proof follows from

References #

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

Tags #

ℂ-differentiable function, harmonic function, Poisson integral.

theorem LeanPool.LeanComplexAnalysis.mem_disc_of_scaled {z : } {r R : } (hR : 0 < R) (hz : z R) (hr : r Set.Ioo 0 1) :
r * z Metric.ball 0 R

Scaling by r ∈ (0,1) a point in a closed disc centerd at 0 is in the open disc.

theorem LeanPool.LeanComplexAnalysis.mem_disc_of_scaled_exp_ofReal_mul_I {r R : } (hR : 0 < R) (hr : r Set.Ioo 0 1) (t : ) :
r * R * Complex.exp (t * Complex.I) Metric.ball 0 R

r * R * exp (t * I) is in the disc of radius R and center 0, for r ∈ (0,1).

R * exp (t * I) is not equal to any z in the disc of radius R, centered at 0.

R * star (exp (t * I)) is not equal to any z in the disc of radius R, centered at 0.

R ^ 2 - star z * w ≠ 0, for z in the disc with radius R and center 0, and for w in the closed disc.

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

If f is -differentiable on a disc centered at zero, then ζ ↦ f (r * ζ) is differentiable at z for r in (0,1) and z in the closed disc.

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

Cauchy's integral formula applied to f -differentiable on a disc centered at 0, at the point r*z, for r in (0,1) and z in the disc.

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

Cauchy's integral formula for -differentiable functions on a disc centred at 0, evaluated at scaled points r * z with r ∈ (0,1).

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

If f is -differentiable on a disc centered at zero, then ζ ↦ (star z / (I * (R ^ 2 - star z * ζ))) • f (r * ζ) is differentiable at w in the closed disc with radius R and center 0, for r in (0,1).

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

We apply the Cauchy-Goursat theorem to the function ζ ↦ (star z / (I * (R ^ 2 - star z * ζ))) • (f (r * ζ))) on the circle of radius R, centered at 0.

theorem LeanPool.LeanComplexAnalysis.goursat_integrand_eq_aux_disc (z : ) (t R : ) (hR : 0 < R) :
star z / (R * star (Complex.exp (t * Complex.I)) - star z) = Complex.I * R * Complex.exp (t * Complex.I) * (star z / (Complex.I * (R ^ 2 - star z * R * Complex.exp (t * Complex.I))))

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

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

The Cauchy-Goursat theorem for a disc centered at 0 implies the integral of a -differentiable function against a conjugate Cauchy kernel vanishes.

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

We put together cauchy_integral_formula_scaled_disc and vanishing_goursat_integral_scaled_disc.

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

For a ℂ-differentiable function f : ℂ → E on a disc centered at 0, f(r*z) equals the integral of f(r*R*e^{it}) against the Poisson kernel, where r ∈ (0,1) and z is in the disc.

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

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

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

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

theorem LeanPool.LeanComplexAnalysis.tendsto_integral_prod_of_continuousOn_circle_closedDisc {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {k : } {r : } {R : } (hR : 0 < R) (hf : ContinuousOn f (Metric.closedBall 0 R)) (hk : ContinuousOn k (Metric.sphere 0 R)) (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 (R * Complex.exp (t * Complex.I)) f ((r n) * R * Complex.exp (t * Complex.I))) Filter.atTop (nhds ( (t : ) in 0..2 * Real.pi, k (R * Complex.exp (t * Complex.I)) f (R * Complex.exp (t * Complex.I))))

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

theorem LeanPool.LeanComplexAnalysis.poisson_ker_continousOn_circle {z : } {R : } (hz : z Metric.ball 0 R) :
ContinuousOn (fun (ζ : ) => (R ^ 2 - z ^ 2) / ζ - z ^ 2) (Metric.sphere 0 R)

The Poisson kernel is continuous on the circle.

If rₙ tends to 1, then f (rₙ * z) tends to f z, for z in a disc centered at 0, when f is continuous on the closed disc.

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

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

Poisson integral formula for ℂ-differentiable functions on a disc: A function f : ℂ → E -differentiable on a disc with radius R and center 0, and continuous on the closed disc, satisfies f(z) = (1/2π) ∫_0^{2π} (R² - |z|²) / |R*e^{it} - z|² f(R*e^{it}) dt for z in the disc.

theorem LeanPool.LeanComplexAnalysis.realPart_herglotz_ker_eq_poisson_ker {R : } (x w : ) (hx : x = R) :
((x + w) / (x - w)).re = (R ^ 2 - w ^ 2) / x - w ^ 2

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

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

theorem LeanPool.LeanComplexAnalysis.poisson_integral_of_diffContOnCl_disc_ker_re {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] {f : E} {z : } {R : } (hf : DiffContOnCl f (Metric.ball 0 R)) (hz : z Metric.ball 0 R) :
f z = (1 / (2 * Real.pi)) (t : ) in 0..2 * Real.pi, ((R * Complex.exp (t * Complex.I) + z) / (R * Complex.exp (t * Complex.I) - z)).re f (R * Complex.exp (t * Complex.I))

Poisson integral formula for ℂ-differentiable functions on a disc: A function f : ℂ → E -differentiable on a disc with radius R and center 0, and continuous on the closed disc, satisfies f(z) = (1/2π) ∫_0^{2π} Re((R*e^{it} + z) / (R*e^{it} - z)) • f(R*e^{it}) dt for z in the disc.

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

theorem LeanPool.LeanComplexAnalysis.circleAverage_of_diffContOnCl_disc {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] {f : E} {z : } {R : } (hf : DiffContOnCl f (Metric.ball 0 R)) (hz : z Metric.ball 0 R) :
f z = Real.circleAverage (fun (ζ : ) => ((ζ + z) / (ζ - z)).re f ζ) 0 R

Poisson integral formula for ℂ-differentiable functions on a disc: A function f : ℂ → E -differentiable on a disc with radius R and center 0, and continuous on the closed disc, satisfies f(z) = (1/2π) ∫_0^{2π} Re((R*e^{it} + z) / (R*e^{it} - z)) • f(R*e^{it}) dt for z in the disc.