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.