AcceptedTheorem · Statement with omitted proof

Poisson integral for a disc

The Poisson-kernel integral represents the harmonic extension of smooth periodic boundary data in the disc setting.

Larsson & Thomée ↗
Theorem 3.3 · printed p. 28

Download Lean file ↓

Formal statement. The assumptions and conclusion are explicit; the theorem proof is omitted (sorry).

01 / MATHEMATICAL STATEMENT

Meaning & conditions

Mathematical summary

The Poisson-kernel integral represents the harmonic extension of smooth periodic boundary data in the disc setting.

u(r,\theta)=\frac1{2\pi}\int_0^{2\pi}\frac{R^2-r^2}{R^2+r^2-2rR\cos(\theta-\varphi)}\,g(\varphi)\,d\varphi.

Assumptions & context

Smooth boundary data with period $2\pi$ and the disc solution predicate defined in the accompanying Lean file.

Source

Larsson & Thomée. Partial differential equations with numerical methods.

Theorem 3.3 · printed p. 28

02 / LEAN REPRESENTATION

Formal statement

Statement with omitted proof. Expand the complete file below to read imports, local definitions and surrounding context.

theorem poisson_integral_formula (R : ℝ) (g : ℝ → ℝ)
    (hg : ContDiff ℝ (⊤ : ℕ∞) g) (hper : Function.Periodic g (2 * Real.pi)) :
    SolvesDiscDirichlet R g (poissonIntegral R g) := by
  sorry

Complete Lean file and local definitions

import PDETextbook.Base

open MeasureTheory
open scoped BigOperators ENNReal

noncomputable section

namespace PDETextbook.LarssonThomee.Thm33

/-- The Poisson kernel `P_R(r, φ) = (R² - r²) / (R² + r² - 2 r R cos φ)`. -/
def poissonKernel (R r φ : ℝ) : ℝ :=
  (R ^ 2 - r ^ 2) / (R ^ 2 + r ^ 2 - 2 * r * R * Real.cos φ)

/-- Polar angle `φ` of `x = (r cos φ, r sin φ)`, with `r = ‖x‖`. -/
def polarAngle (x : Euclidean 2) : ℝ :=
  Complex.arg ⟨x 0, x 1⟩

/-- The function defined by (3.9):
`u(x) = (1/2π) ∫₀^{2π} P_R(r, φ - ψ) g(ψ) dψ` with `x = (r cos φ, r sin φ)`. -/
def poissonIntegral (R : ℝ) (g : ℝ → ℝ) (x : Euclidean 2) : ℝ :=
  1 / (2 * Real.pi) *
    ∫ ψ in (0 : ℝ)..(2 * Real.pi), poissonKernel R ‖x‖ (polarAngle x - ψ) * g ψ

/-- Classical Laplacian `Δu = ∂₁²u + ∂₂²u` in the plane. -/
def laplacian (u : Euclidean 2 → ℝ) (x : Euclidean 2) : ℝ :=
  ∑ i : Fin 2, partialDeriv (fun y => partialDeriv u i y) i x

/-- `u` is a solution of the Dirichlet problem (3.8) in the disc `|x| < R`:
`-Δu = 0` for `|x| < R` (classically, `u` being C² there), and the boundary condition
`u(R cos φ, R sin φ) = g(φ)` for `0 ≤ φ < 2π`, understood as the boundary values
attained by `u` from inside the disc. -/
def SolvesDiscDirichlet (R : ℝ) (g : ℝ → ℝ) (u : Euclidean 2 → ℝ) : Prop :=
  ContDiffOn ℝ 2 u (Metric.ball (0 : Euclidean 2) R) ∧
  (∀ x ∈ Metric.ball (0 : Euclidean 2) R, -laplacian u x = 0) ∧
  ∀ φ : ℝ, 0 ≤ φ → φ < 2 * Real.pi →
    ∀ x : Euclidean 2, x 0 = R * Real.cos φ → x 1 = R * Real.sin φ →
      Filter.Tendsto u (nhdsWithin x (Metric.ball (0 : Euclidean 2) R)) (nhds (g φ))

/-- Theorem 3.3 (Poisson's integral formula). For `g` appropriately smooth (realized as a
smooth 2π-periodic function, i.e. smooth data on the circle), the function defined by (3.9)
is a solution of (3.8). -/
theorem poisson_integral_formula (R : ℝ) (g : ℝ → ℝ)
    (hg : ContDiff ℝ (⊤ : ℕ∞) g) (hper : Function.Periodic g (2 * Real.pi)) :
    SolvesDiscDirichlet R g (poissonIntegral R g) := by
  sorry

end PDETextbook.LarssonThomee.Thm33

How to read the formalization

The radius is an unrestricted parameter in the saved declaration; the exact predicate and parameter scope are visible below.

← Back to all statements