The Poisson integral of the Euclidean unit ball and the Dirichlet problem

For boundary data g on the unit sphere S of ℝⁿ, the Poisson integral

P[g](x) = ∫_S K(x, y) g(y) dσ(y)

averages g against the Poisson kernel K = TauCeti.ballPoissonKernel of the unit ball, with respect to the surface measure σ = volume.toSphere on S. It is the candidate solution of the Dirichlet problem Δu = 0 in the ball, u = g on S.

This file proves that the Poisson kernel has mass one: ∫_S K(x, y) dσ(y) = 1 for every pole x in the open ball (n ≠ 0). For x = r θ with ‖θ‖ = 1 and a boundary point y, the distances ‖r θ - y‖ and ‖r y - θ‖ agree, so K(x, y) = K(r y, θ); the integral over y is then the sphere integral of the function K(·, θ), harmonic on the closed ball of radius r < 1, and the mean-value property evaluates it as σ(S) K(0, θ) = 1.

With positivity of the kernel and its far-field bound, mass one makes the Poisson kernel an approximate identity on the sphere: the Poisson integral of continuous boundary data tends to g z as its argument tends to a boundary point z from inside the ball (TauCeti.tendsto_ballPoissonIntegral).

The Poisson integral of integrable data is harmonic off the sphere: the kernel K(·, y) is harmonic away from y and smooth jointly in (x, y) off the diagonal, so the Laplacian may be taken under the integral sign (TauCeti.harmonicOnNhd_integral_smul_of_contDiffOn). Together with boundary attainment this solves the Dirichlet problem Δu = 0 in the ball, u = g on the sphere, for continuous data. Since harmonicity is invariant under isometries and homotheties, the same holds on every ball of a finite-dimensional real inner product space.

Main declarations

• TauCeti.integral_ballPoissonKernel: the Poisson kernel of the ball has mass one.
• TauCeti.ballPoissonIntegral: the Poisson integral of boundary data on the unit sphere.
• TauCeti.ballPoissonIntegral_const, TauCeti.ballPoissonIntegral_add, TauCeti.ballPoissonIntegral_smul, TauCeti.ballPoissonIntegral_mono: the Poisson integral is a positive linear operator preserving constants.
• TauCeti.tendsto_ballPoissonIntegral: the Poisson integral of continuous boundary data attains the boundary values.
• TauCeti.harmonicOnNhd_ballPoissonIntegral: the Poisson integral is harmonic off the sphere.
• TauCeti.exists_harmonicOnNhd_ball_continuousOn_closedBall_eq: existence of a solution of the Dirichlet problem on the unit ball for continuous boundary data.
• TauCeti.exists_harmonicOnNhd_ball_continuousOn_closedBall_eqOn_sphere: the same on every ball of a finite-dimensional real inner product space, by an isometry and a homothety.

References

The boundary argument and operator API are adapted from the planar formalization in TauCeti/Analysis/Complex/Poisson/Integral.lean.

• L. C. Evans, Partial Differential Equations, Section 2.2.4, Theorem 15.
• D. Gilbarg, N. S. Trudinger, Elliptic Partial Differential Equations of Second Order, Section 2.5, Theorem 2.6.

@[simp]

theorem TauCeti.integral_ballPoissonKernel {n : ℕ} (hn : n ≠ 0) {x : EuclideanSpace ℝ (Fin n)} (hx : ‖x‖ < 1) : ∫ (y : ↑(Metric.sphere 0 1)), ballPoissonKernel n x ↑y ∂MeasureTheory.volume.toSphere = 1

The Poisson kernel of the ball has mass one. For a pole x in the open unit ball of ℝⁿ, n ≠ 0, the Poisson kernel K(x, ·) integrates to one against the surface measure of the unit sphere.

theorem TauCeti.integrable_ballPoissonKernel_mul {n : ℕ} {g : ↑(Metric.sphere 0 1) → ℝ} (hg : MeasureTheory.Integrable g MeasureTheory.volume.toSphere) {x : EuclideanSpace ℝ (Fin n)} : MeasureTheory.Integrable (fun (y : ↑(Metric.sphere 0 1)) => ballPoissonKernel n x ↑y * g y) MeasureTheory.volume.toSphere

The Poisson kernel with any pole times integrable boundary data is integrable on the sphere.

noncomputable def TauCeti.ballPoissonIntegral {n : ℕ} (g : ↑(Metric.sphere 0 1) → ℝ) (x : EuclideanSpace ℝ (Fin n)) : ℝ

The Poisson integral of boundary data g on the unit sphere of ℝⁿ,

P[g](x) = ∫_S K(x, y) g(y) dσ(y),

where K is the Poisson kernel of the unit ball and σ is the surface measure of the unit sphere S. For continuous g it tends to g z at each boundary point z (TauCeti.tendsto_ballPoissonIntegral).

Equations

• TauCeti.ballPoissonIntegral g x = ∫ (y : ↑(Metric.sphere 0 1)), TauCeti.ballPoissonKernel n x ↑y * g y ∂MeasureTheory.volume.toSphere

theorem TauCeti.ballPoissonIntegral_def {n : ℕ} (g : ↑(Metric.sphere 0 1) → ℝ) (x : EuclideanSpace ℝ (Fin n)) : ballPoissonIntegral g x = ∫ (y : ↑(Metric.sphere 0 1)), ballPoissonKernel n x ↑y * g y ∂MeasureTheory.volume.toSphere

The defining formula for the Poisson integral of the ball.

theorem TauCeti.harmonicOnNhd_ballPoissonIntegral {n : ℕ} {g : ↑(Metric.sphere 0 1) → ℝ} (hg : MeasureTheory.Integrable g MeasureTheory.volume.toSphere) : InnerProductSpace.HarmonicOnNhd (ballPoissonIntegral g) (Metric.sphere 0 1)ᶜ

The Poisson integral is harmonic. For integrable boundary data g on the unit sphere of ℝⁿ, the Poisson integral P[g] is harmonic off the sphere, in particular throughout the open unit ball.

@[simp]

theorem TauCeti.ballPoissonIntegral_zero {n : ℕ} (x : EuclideanSpace ℝ (Fin n)) : ballPoissonIntegral (fun (x : ↑(Metric.sphere 0 1)) => 0) x = 0

The Poisson integral of zero boundary data is zero.

theorem TauCeti.ballPoissonIntegral_add {n : ℕ} {g₁ g₂ : ↑(Metric.sphere 0 1) → ℝ} (hg₁ : MeasureTheory.Integrable g₁ MeasureTheory.volume.toSphere) (hg₂ : MeasureTheory.Integrable g₂ MeasureTheory.volume.toSphere) {x : EuclideanSpace ℝ (Fin n)} : ballPoissonIntegral (g₁ + g₂) x = ballPoissonIntegral g₁ x + ballPoissonIntegral g₂ x

The Poisson integral is additive in integrable boundary data at every pole.

@[simp]

theorem TauCeti.ballPoissonIntegral_smul {n : ℕ} (a : ℝ) (g : ↑(Metric.sphere 0 1) → ℝ) (x : EuclideanSpace ℝ (Fin n)) : ballPoissonIntegral (a • g) x = a • ballPoissonIntegral g x

The Poisson integral commutes with real scalar multiplication of the boundary data.

@[simp]

theorem TauCeti.ballPoissonIntegral_const {n : ℕ} (hn : n ≠ 0) {x : EuclideanSpace ℝ (Fin n)} (hx : ‖x‖ < 1) (a : ℝ) : ballPoissonIntegral (fun (x : ↑(Metric.sphere 0 1)) => a) x = a

The Poisson integral preserves constant boundary data at every point of the open unit ball.

theorem TauCeti.ballPoissonIntegral_sub_const {n : ℕ} (hn : n ≠ 0) {g : ↑(Metric.sphere 0 1) → ℝ} (hg : MeasureTheory.Integrable g MeasureTheory.volume.toSphere) {x : EuclideanSpace ℝ (Fin n)} (hx : ‖x‖ < 1) (a : ℝ) : ballPoissonIntegral g x - a = ∫ (y : ↑(Metric.sphere 0 1)), ballPoissonKernel n x ↑y * (g y - a) ∂MeasureTheory.volume.toSphere

In the open unit ball, subtracting a constant from the Poisson integral subtracts it from the boundary data under the kernel.

theorem TauCeti.ballPoissonIntegral_mono {n : ℕ} {g₁ g₂ : ↑(Metric.sphere 0 1) → ℝ} (hg₁ : MeasureTheory.Integrable g₁ MeasureTheory.volume.toSphere) (hg₂ : MeasureTheory.Integrable g₂ MeasureTheory.volume.toSphere) (hle : g₁ ≤ g₂) {x : EuclideanSpace ℝ (Fin n)} (hx : ‖x‖ < 1) : ballPoissonIntegral g₁ x ≤ ballPoissonIntegral g₂ x

The Poisson integral preserves order between integrable boundary data in the open unit ball.

theorem TauCeti.ballPoissonIntegral_nonneg {n : ℕ} {g : ↑(Metric.sphere 0 1) → ℝ} (hg : 0 ≤ g) {x : EuclideanSpace ℝ (Fin n)} (hx : ‖x‖ < 1) : 0 ≤ ballPoissonIntegral g x

Nonnegative boundary data have a nonnegative Poisson integral in the open unit ball.

theorem TauCeti.tendsto_ballPoissonIntegral {n : ℕ} {g : ↑(Metric.sphere 0 1) → ℝ} (hg : Continuous g) (z : ↑(Metric.sphere 0 1)) : Filter.Tendsto (ballPoissonIntegral g) (nhdsWithin (↑z) (Metric.ball 0 1)) (nhds (g z))

The Poisson integral attains continuous boundary values. For continuous data g on the unit sphere of ℝⁿ and a point z of the sphere, the Poisson integral P[g](x) tends to g z as x tends to z through the open unit ball.

theorem TauCeti.exists_harmonicOnNhd_ball_continuousOn_closedBall_eq {n : ℕ} {g : ↑(Metric.sphere 0 1) → ℝ} (hg : Continuous g) : ∃ (u : EuclideanSpace ℝ (Fin n) → ℝ), InnerProductSpace.HarmonicOnNhd u (Metric.ball 0 1) ∧ ContinuousOn u (Metric.closedBall 0 1) ∧ ∀ (z : ↑(Metric.sphere 0 1)), u ↑z = g z

The Dirichlet problem on the unit ball. For continuous data g on the unit sphere of ℝⁿ there is a function harmonic in the open unit ball, continuous on the closed ball, and equal to g on the sphere: the Poisson integral of g inside the ball, extended by g on the sphere. Uniqueness on the closed ball is the maximum principle TauCeti.eqOn_of_harmonicOnNhd_of_eqOn_frontier.

theorem TauCeti.exists_harmonicOnNhd_ball_continuousOn_closedBall_eqOn_sphere {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {c : E} {r : ℝ} {g : E → ℝ} (hg : ContinuousOn g (Metric.sphere c r)) : ∃ (u : E → ℝ), InnerProductSpace.HarmonicOnNhd u (Metric.ball c r) ∧ ContinuousOn u (Metric.closedBall c r) ∧ Set.EqOn u g (Metric.sphere c r)

The Dirichlet problem on a ball. In a finite-dimensional real inner product space, for data g continuous on the sphere sphere c r, there is a function harmonic in the open ball ball c r, continuous on the closed ball, and equal to g on the sphere. For 0 < r it is the unit-ball solution TauCeti.exists_harmonicOnNhd_ball_continuousOn_closedBall_eq, transported along an isometry of E with ℝⁿ and the homothety y ↦ c + r • y; for r ≤ 0 the open ball is empty and the closed ball is contained in the sphere, so g itself is a solution.