structure LaplacePoisson.IsLipschitzDomain {n : ℕ} (Ω : Set (Fin n → ℝ)) : Prop

A bounded Lipschitz domain in $\mathbb{R}^n$: an open, bounded, nonempty, connected set whose boundary can be locally straightened by bi-Lipschitz maps. This is the natural class of domains for the Poisson Dirichlet problem.

• isOpen : IsOpen Ω
• isBounded : Bornology.IsBounded Ω
• nonempty : Ω.Nonempty
• isConnected : IsConnected Ω
• frontier_nonempty : (frontier Ω).Nonempty
• lipschitz_boundary (x : Fin n → ℝ) : x ∈ frontier Ω → ∃ (U : Set (Fin n → ℝ)), IsOpen U ∧ x ∈ U ∧ ∃ (φ : (Fin n → ℝ) → Fin n → ℝ), LipschitzWith 1 φ ∧ ∃ (ψ : (Fin n → ℝ) → Fin n → ℝ), LipschitzWith 1 ψ ∧ (∀ y ∈ U, ψ (φ y) = y) ∧ ∀ z ∈ φ '' U, φ (ψ z) = z

noncomputable def LaplacePoisson.euclidNormLP {n : ℕ} (x : Fin n → ℝ) : ℝ

Euclidean norm on $\mathbb{R}^n$ written as $|x| = \sqrt{\sum_i (x^i)^2}$, for vectors represented as Fin n → ℝ (the LP suffix marks the L^p-style function space presentation).

theorem LaplacePoisson.euclidNormLP_neg {n : ℕ} (x : Fin n → ℝ) : euclidNormLP (-x) = euclidNormLP x

The Euclidean norm is invariant under negation: $|-x| = |x|$.

theorem LaplacePoisson.euclidNormLP_eq_norm_withLp {n : ℕ} (v : Fin n → ℝ) : euclidNormLP v = ‖(WithLp.equiv 2 (Fin n → ℝ)).symm v‖

The custom euclidNormLP agrees with the Mathlib L^2 norm on Fin n → ℝ via the WithLp 2 equivalence.

theorem LaplacePoisson.euclidNormLP_nonneg {n : ℕ} (x : Fin n → ℝ) : euclidNormLP x ≥ 0

The Euclidean norm is nonnegative: $|x| \ge 0$.

theorem LaplacePoisson.euclidNormLP_sub_le {n : ℕ} (a b : Fin n → ℝ) : euclidNormLP a - euclidNormLP b ≤ euclidNormLP (a - b)

Reverse triangle inequality for the Euclidean norm: $|a| - |b| \le |a - b|$.

noncomputable def LaplacePoisson.unitSphereArea (n : ℕ) : ℝ

Surface area $\omega_n$ of the unit sphere in $\mathbb{R}^n$, defined via the Gamma function: $\omega_n = 2\pi^{n/2}/\Gamma(n/2)$ for $n \ge 1$. For example $\omega_3 = 4\pi$. The convention $\omega_0 = 1$ is taken here.

theorem LaplacePoisson.unitSphereArea_pos (n : ℕ) : unitSphereArea n > 0

The unit sphere area $\omega_n$ is strictly positive for every $n$.

theorem LaplacePoisson.unitSphereArea_three : unitSphereArea 3 = 4 * Real.pi

Classical formula: the area of the unit $2$-sphere in $\mathbb{R}^3$ is $\omega_3 = 4\pi$.

noncomputable def LaplacePoisson.fundamentalSolution (n : ℕ) (x : Fin n → ℝ) : ℝ

The fundamental solution $\Phi$ for the Laplacian $\Delta$ in $\mathbb{R}^n$ (Definition 1.0.1 of CM7): $\Phi(x) = \frac{1}{2\pi} \ln|x|$ for $n=2$, and $\Phi(x) = -\frac{1}{\omega_n |x|^{n-2}}$ for $n \ge 3$, where $\omega_n$ is the surface area of the unit sphere in $\mathbb{R}^n$.

theorem LaplacePoisson.fundamentalSolution_neg {n : ℕ} (x : Fin n → ℝ) : fundamentalSolution n (-x) = fundamentalSolution n x

The fundamental solution is radially symmetric: $\Phi(-x) = \Phi(x)$.

noncomputable def LaplacePoisson.laplacianLP {n : ℕ} (f : (Fin n → ℝ) → ℝ) (x : Fin n → ℝ) : ℝ

The Laplacian $\Delta f(x) = \sum_{i=1}^n \partial_i^2 f(x)$ on $\mathbb{R}^n$, expressed in terms of fderiv applied twice in coordinate directions.

def LaplacePoisson.IsHarmonicLP {n : ℕ} (u : (Fin n → ℝ) → ℝ) (Ω : Set (Fin n → ℝ)) : Prop

A function $u$ is harmonic on $\Omega$ when $\Delta u = 0$ pointwise on $\Omega$.

noncomputable def LaplacePoisson.phiConvolutionLP (n : ℕ) (f : (Fin n → ℝ) → ℝ) (x : Fin n → ℝ) : ℝ

Convolution of the fundamental solution with $f$: $(\Phi * f)(x) = \int_{\mathbb{R}^n} \Phi(x - y)\,f(y)\,d^n y$. This is the candidate solution of $\Delta u = f$ in Theorem 1.1 of CM7.

opaque LaplacePoisson.outwardUnitNormal {n : ℕ} (Ω : Set (Fin n → ℝ)) : (Fin n → ℝ) → Fin n → ℝ

Outward unit normal vector field on the boundary of $\Omega \subset \mathbb{R}^n$, treated abstractly via an opaque declaration.

opaque LaplacePoisson.surfaceMeasure {n : ℕ} (Ω : Set (Fin n → ℝ)) : MeasureTheory.Measure (Fin n → ℝ)

The $(n-1)$-dimensional surface (Hausdorff) measure attached to the boundary of $\Omega$, treated abstractly via an opaque declaration.

theorem LaplacePoisson.outwardUnitNormal_zero_off_frontier {n : ℕ} (Ω : Set (Fin n → ℝ)) (σ : Fin n → ℝ) (hσ : σ ∉ frontier Ω) : outwardUnitNormal Ω σ = 0

The outward unit normal is zero off the boundary of $\Omega$.

theorem LaplacePoisson.outwardUnitNormal_component_le_one {n : ℕ} (Ω : Set (Fin n → ℝ)) (σ : Fin n → ℝ) (i : Fin n) : |outwardUnitNormal Ω σ i| ≤ 1

Each component of the outward unit normal has absolute value at most $1$.

theorem LaplacePoisson.fderiv_bounded_on_compact_closure {n : ℕ} (u : (Fin n → ℝ) → ℝ) (Ω : Set (Fin n → ℝ)) (hu : ContDiffOn ℝ 2 u (closure Ω)) (hΩb : Bornology.IsBounded Ω) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ σ ∈ closure Ω, ‖fderiv ℝ u σ‖ ≤ C

A $C^2$ function on the closure of a bounded set has uniformly bounded Fréchet derivative on that closure.

noncomputable def LaplacePoisson.normalDerivLP {n : ℕ} (Ω : Set (Fin n → ℝ)) (f : (Fin n → ℝ) → ℝ) (σ : Fin n → ℝ) : ℝ

Outer normal derivative $\partial_\nu f(\sigma) = \nabla f(\sigma) \cdot \nu(\sigma)$ on the boundary of $\Omega$.

noncomputable def LaplacePoisson.surfaceIntegralLP {n : ℕ} (Ω : Set (Fin n → ℝ)) (f : (Fin n → ℝ) → ℝ) : ℝ

Surface integral $\int_{\partial \Omega} f \, dS$ of $f$ over the boundary of $\Omega$ with respect to the surface measure.

theorem LaplacePoisson.outwardUnitNormal_exterior_sphere_spec {n : ℕ} (ε : ℝ) (hε : 0 < ε) (σ : Fin n → ℝ) (hσ : euclidNormLP σ = ε) (i : Fin n) : outwardUnitNormal {z : Fin n → ℝ | euclidNormLP z ≥ ε} σ i = -σ i / euclidNormLP σ

On the inner sphere $|z| = \varepsilon$ bounding the exterior region $\{|z| \ge \varepsilon\}$, the outward unit normal points toward the origin: $\nu_i(\sigma) = -\sigma_i / |\sigma|$.

theorem LaplacePoisson.pointwise_normalDerivLP_fundamentalSolution_on_sphere {n : ℕ} (hn : n ≥ 3) (ε : ℝ) (hε : 0 < ε) (σ : Fin n → ℝ) (hσ : euclidNormLP σ = ε) : normalDerivLP {z : Fin n → ℝ | euclidNormLP z ≥ ε} (fundamentalSolution n) σ = -1 / (unitSphereArea n * ε ^ (n - 1))

Pointwise computation: the inward normal derivative of $\Phi$ on the sphere $|\sigma| = \varepsilon$ equals the constant $-1/(\omega_n \varepsilon^{n-1})$ (here $n \ge 3$).

theorem LaplacePoisson.normalDerivLP_fundamentalSolution_sphere_ae {n : ℕ} (hn : n ≥ 3) (ε : ℝ) (hε : 0 < ε) : (fun (σ : Fin n → ℝ) => normalDerivLP {z : Fin n → ℝ | euclidNormLP z ≥ ε} (fundamentalSolution n) σ) =ᵐ[(surfaceMeasure {z : Fin n → ℝ | euclidNormLP z = ε}).restrict (frontier {z : Fin n → ℝ | euclidNormLP z = ε})] fun (x : Fin n → ℝ) => -1 / (unitSphereArea n * ε ^ (n - 1))

Almost-everywhere version of the pointwise computation: on the boundary of $\{|z| = \varepsilon\}$ the normal derivative of $\Phi$ is constantly $-1/(\omega_n \varepsilon^{n-1})$ with respect to surface measure.

theorem LaplacePoisson.surfaceMeasure_sphere_measureReal {n : ℕ} (hn : n ≥ 3) (ε : ℝ) (hε : 0 < ε) : (surfaceMeasure {z : Fin n → ℝ | euclidNormLP z = ε}).real (frontier {z : Fin n → ℝ | euclidNormLP z = ε}) = unitSphereArea n * ε ^ (n - 1)

The total surface measure of the sphere $\{|z| = \varepsilon\}$ in $\mathbb{R}^n$ equals $\omega_n \varepsilon^{n-1}$.

theorem LaplacePoisson.hasFDerivAt_sum_sq {n : ℕ} (x : Fin n → ℝ) : HasFDerivAt (fun (y : Fin n → ℝ) => ∑ j : Fin n, y j ^ 2) (∑ j : Fin n, (2 * x j) • ContinuousLinearMap.proj j) x

The Fréchet derivative of $y \mapsto \sum_j y_j^2$ at $x$ is the linear functional $v \mapsto \sum_j 2 x_j \, v_j$.

theorem LaplacePoisson.sum_sq_pos_of_ne_zero {n : ℕ} (x : Fin n → ℝ) (hx : x ≠ 0) : ∑ j : Fin n, x j ^ 2 > 0

If $x \ne 0$ in $\mathbb{R}^n$ then $\sum_j x_j^2 > 0$.

theorem LaplacePoisson.hasFDerivAt_euclidNormLP {n : ℕ} (x : Fin n → ℝ) (hx : x ≠ 0) : HasFDerivAt euclidNormLP ((1 / (2 * euclidNormLP x)) • ∑ j : Fin n, (2 * x j) • ContinuousLinearMap.proj j) x

Away from the origin the Euclidean norm is differentiable; its Fréchet derivative is computed via the chain rule from $|x| = \sqrt{\sum_j x_j^2}$.

theorem LaplacePoisson.euclidNormLP_pos {n : ℕ} (x : Fin n → ℝ) (hx : x ≠ 0) : euclidNormLP x > 0

The Euclidean norm is strictly positive at nonzero points: $x \ne 0 \Rightarrow |x| > 0$.

theorem LaplacePoisson.first_partial_eq_near {n : ℕ} (g : ℝ → ℝ) (hg : ContDiffOn ℝ 2 g (Set.Ioi 0)) (x : Fin n → ℝ) (hx : x ≠ 0) (i : Fin n) : (fun (y : Fin n → ℝ) => (fderiv ℝ (fun (z : Fin n → ℝ) => g (euclidNormLP z)) y) (Pi.single i 1)) =ᶠ[nhds x] fun (y : Fin n → ℝ) => (fderiv ℝ g (euclidNormLP y)) 1 * (y i / euclidNormLP y)

Near a nonzero point $x$, the $i$-th partial derivative of a radial function $g(|z|)$ equals $g'(|y|)\,(y_i/|y|)$ by the chain rule.

theorem LaplacePoisson.differentiableAt_coord_over_norm {n : ℕ} (x : Fin n → ℝ) (hx : x ≠ 0) (i : Fin n) : DifferentiableAt ℝ (fun (y : Fin n → ℝ) => y i / euclidNormLP y) x

Away from the origin, the function $y \mapsto y_i / |y|$ is differentiable.

theorem LaplacePoisson.fderiv_coord_over_norm_single {n : ℕ} (x : Fin n → ℝ) (hx : x ≠ 0) (i : Fin n) : (fderiv ℝ (fun (y : Fin n → ℝ) => y i / euclidNormLP y) x) (Pi.single i 1) = 1 / euclidNormLP x - x i ^ 2 / euclidNormLP x ^ 3

The partial derivative of $y \mapsto y_i/|y|$ in the direction $e_i$ is $\partial_i (y_i/|y|) = 1/|y| - y_i^2 / |y|^3$ at points $x \ne 0$.

theorem LaplacePoisson.differentiableAt_gprime_comp_norm {n : ℕ} (g : ℝ → ℝ) (hg : ContDiffOn ℝ 2 g (Set.Ioi 0)) (x : Fin n → ℝ) (hx : x ≠ 0) : DifferentiableAt ℝ (fun (y : Fin n → ℝ) => (fderiv ℝ g (euclidNormLP y)) 1) x

Away from the origin, $y \mapsto g'(|y|)$ is differentiable for $g \in C^2$ on $(0, \infty)$.

theorem LaplacePoisson.fderiv_gprime_comp_norm_single {n : ℕ} (g : ℝ → ℝ) (hg : ContDiffOn ℝ 2 g (Set.Ioi 0)) (x : Fin n → ℝ) (hx : x ≠ 0) (i : Fin n) : (fderiv ℝ (fun (y : Fin n → ℝ) => (fderiv ℝ g (euclidNormLP y)) 1) x) (Pi.single i 1) = (fderiv ℝ (fun (s : ℝ) => (fderiv ℝ g s) 1) (euclidNormLP x)) 1 * (x i / euclidNormLP x)

Chain rule for $\partial_i [g'(|y|)] = g''(|y|) \, (y_i / |y|)$ at $x \ne 0$.

theorem LaplacePoisson.axm_second_partial_comp_norm {n : ℕ} (g : ℝ → ℝ) (hg : ContDiffOn ℝ 2 g (Set.Ioi 0)) (x : Fin n → ℝ) (hx : x ≠ 0) (i : Fin n) : have r := euclidNormLP x; (fderiv ℝ (fun (y : Fin n → ℝ) => (fderiv ℝ (fun (z : Fin n → ℝ) => g (euclidNormLP z)) y) (Pi.single i 1)) x) (Pi.single i 1) = (fderiv ℝ (fun (s : ℝ) => (fderiv ℝ g s) 1) r) 1 * (x i / r) ^ 2 + (fderiv ℝ g r) 1 * (1 / r - x i ^ 2 / r ^ 3)

Second partial derivative of a radial function: $\partial_i^2 [g(|x|)] = g''(|x|) (x_i/|x|)^2 + g'(|x|)(1/|x| - x_i^2/|x|^3)$ at points $x \ne 0$.

theorem LaplacePoisson.continuous_euclidNormLP {n : ℕ} : Continuous fun (x : Fin n → ℝ) => euclidNormLP x

The Euclidean norm $x \mapsto |x|$ is continuous on $\mathbb{R}^n$.

theorem LaplacePoisson.norm_sum_div_sq {n : ℕ} (x : Fin n → ℝ) (hx : x ≠ 0) : ∑ i : Fin n, (x i / euclidNormLP x) ^ 2 = 1

The squared components of the unit vector $x/|x|$ sum to $1$: $\sum_i (x_i/|x|)^2 = 1$ for $x \ne 0$.

theorem LaplacePoisson.spherical_laplacian_identity {n : ℕ} (hn : n ≥ 2) (g : ℝ → ℝ) (hg : ContDiffOn ℝ 2 g (Set.Ioi 0)) (x : Fin n → ℝ) (hx : x ≠ 0) : have r := euclidNormLP x; laplacianLP (fun (y : Fin n → ℝ) => g (euclidNormLP y)) x = (fderiv ℝ (fun (s : ℝ) => (fderiv ℝ g s) 1) r) 1 + ↑(n - 1) / r * (fderiv ℝ g r) 1

Radial form of the Laplacian: for a radial function $u(x) = g(|x|)$ in $\mathbb{R}^n$ with $n \ge 2$ and $x \ne 0$, $\Delta u(x) = g''(r) + \frac{n-1}{r} g'(r)$ where $r = |x|$.

theorem LaplacePoisson.radial_fundamental_smooth (n : ℕ) (_hn : n ≥ 3) : ContDiffOn ℝ 2 (fun (r : ℝ) => -1 / (unitSphereArea n * r ^ (n - 2))) (Set.Ioi 0)

For $n \ge 3$, the radial profile $r \mapsto -1/(\omega_n r^{n-2})$ of the fundamental solution is $C^2$ on $(0, \infty)$.

theorem LaplacePoisson.power_radial_first_deriv (n : ℕ) (hn : n ≥ 3) (r : ℝ) (hr : r > 0) : (fderiv ℝ (fun (s : ℝ) => -1 / (unitSphereArea n * s ^ (n - 2))) r) 1 = ↑(n - 2) / (unitSphereArea n * r ^ (n - 1))

First derivative of the radial profile of $\Phi$ for $n \ge 3$: $\frac{d}{dr}\!\left(-\frac{1}{\omega_n r^{n-2}}\right) = \frac{n-2}{\omega_n r^{n-1}}$.

theorem LaplacePoisson.power_radial_second_deriv (n : ℕ) (hn : n ≥ 3) (r : ℝ) (hr : r > 0) : (fderiv ℝ (fun (s : ℝ) => (fderiv ℝ (fun (t : ℝ) => -1 / (unitSphereArea n * t ^ (n - 2))) s) 1) r) 1 = -↑(n - 2) * ↑(n - 1) / (unitSphereArea n * r ^ n)

Second derivative of the radial profile of $\Phi$ for $n \ge 3$: $\frac{d^2}{dr^2}\!\left(-\frac{1}{\omega_n r^{n-2}}\right) = -\frac{(n-2)(n-1)}{\omega_n r^n}$.

theorem LaplacePoisson.fundamental_solution_harmonic_away {n : ℕ} (hn : n ≥ 3) (x : Fin n → ℝ) (hx : x ≠ 0) : laplacianLP (fundamentalSolution n) x = 0

Lemma 1.0.1 of CM7: the fundamental solution is harmonic away from the origin. That is, $\Delta \Phi(x) = 0$ for $x \ne 0$ (here $n \ge 3$).

theorem LaplacePoisson.greens_second_identity {n : ℕ} (Ω : Set (Fin n → ℝ)) (u v : (Fin n → ℝ) → ℝ) (hu : ContDiffOn ℝ 2 u (closure Ω)) (hv : ContDiffOn ℝ 2 v (closure Ω)) (hΩ : IsOpen Ω) (hΩb : Bornology.IsBounded Ω) : ∫ (x : Fin n → ℝ) in Ω, v x * laplacianLP u x - u x * laplacianLP v x = surfaceIntegralLP Ω fun (σ : Fin n → ℝ) => v σ * normalDerivLP Ω u σ - u σ * normalDerivLP Ω v σ

Green's second identity for sufficiently regular $u, v$ on a bounded open $\Omega$: $\int_\Omega (v \Delta u - u \Delta v) = \int_{\partial \Omega} (v \, \partial_\nu u - u \, \partial_\nu v)\,dS$.

theorem LaplacePoisson.leibniz_laplacian_under_integral {n : ℕ} (_hn : n ≥ 3) (f : (Fin n → ℝ) → ℝ) (_hf_smooth : ContDiff ℝ ⊤ f) (_hf_supp : HasCompactSupport f) (x : Fin n → ℝ) : laplacianLP (fun (x' : Fin n → ℝ) => ∫ (y : Fin n → ℝ), fundamentalSolution n y * f (x' - y)) x = ∫ (y : Fin n → ℝ), fundamentalSolution n y * laplacianLP (fun (x' : Fin n → ℝ) => f (x' - y)) x

Differentiation under the integral sign: the Laplacian commutes with the $\Phi$-convolution against a smooth compactly supported $f$.

theorem LaplacePoisson.convolution_substitution {n : ℕ} (f : (Fin n → ℝ) → ℝ) (x : Fin n → ℝ) : ∫ (y : Fin n → ℝ), fundamentalSolution n (x - y) * f y = ∫ (y : Fin n → ℝ), fundamentalSolution n y * f (x - y)

Substitution $y \mapsto x - y$ in the convolution integral: $\int \Phi(x - y) f(y)\,dy = \int \Phi(y) f(x - y)\,dy$.

theorem LaplacePoisson.fderiv_comp_const_sub_LP {n : ℕ} (g : (Fin n → ℝ) → ℝ) (x z' : Fin n → ℝ) (hg : DifferentiableAt ℝ g (x - z')) : fderiv ℝ (fun (z : Fin n → ℝ) => g (x - z)) z' = -fderiv ℝ g (x - z')

Chain rule for $z \mapsto g(x - z)$: its derivative at $z'$ is the negative of the derivative of $g$ at $x - z'$.

theorem LaplacePoisson.laplacianLP_chain_rule_sub {n : ℕ} (f : (Fin n → ℝ) → ℝ) (_hf : ContDiff ℝ ⊤ f) (x y : Fin n → ℝ) : laplacianLP (fun (x' : Fin n → ℝ) => f (x' - y)) x = laplacianLP (fun (z : Fin n → ℝ) => f (x - z)) y

Variable swap for the Laplacian under translation: the Laplacian of $x' \mapsto f(x' - y)$ at $x$ equals the Laplacian of $z \mapsto f(x - z)$ at $y$, since each equals $\Delta f(x - y)$.

theorem LaplacePoisson.laplacian_convolution_eq_integral {n : ℕ} (hn : n ≥ 3) (f : (Fin n → ℝ) → ℝ) (hf_smooth : ContDiff ℝ ⊤ f) (hf_supp : HasCompactSupport f) (x : Fin n → ℝ) : laplacianLP (phiConvolutionLP n f) x = ∫ (y : Fin n → ℝ), fundamentalSolution n y * laplacianLP (fun (z : Fin n → ℝ) => f (x - z)) y

Combining the substitution and Leibniz rules: $\Delta_x (\Phi * f)(x) = \int \Phi(y) \, \Delta_z f(x - z)|_{z = y}\,dy$.

theorem LaplacePoisson.laplacianLP_bounded_of_smooth_compactSupport {n : ℕ} (g : (Fin n → ℝ) → ℝ) (_hg_smooth : ContDiff ℝ ⊤ g) (_hg_supp : HasCompactSupport g) : ∃ (M : ℝ), 0 ≤ M ∧ ∀ (y : Fin n → ℝ), |laplacianLP g y| ≤ M

The Laplacian of a smooth, compactly supported function is uniformly bounded.

theorem LaplacePoisson.coarea_euclidBall_abs_fundamentalSolution_eq {n : ℕ} (_hn : n ≥ 3) (ε : ℝ) (_hε : 0 < ε) : ∫ (y : Fin n → ℝ) in {z : Fin n → ℝ | euclidNormLP z < ε}, |fundamentalSolution n y| = ∫ (r : ℝ) in 0..ε, r

Polar/coarea formula identification: the integral of $|\Phi|$ over the Euclidean ball of radius $\varepsilon$ equals the 1D integral $\int_0^\varepsilon r\,dr$.

theorem LaplacePoisson.euclidBall_integral_fundamentalSolution_abs_le {n : ℕ} (hn : n ≥ 3) (ε : ℝ) (hε : 0 < ε) : ∫ (y : Fin n → ℝ) in {z : Fin n → ℝ | euclidNormLP z < ε}, |fundamentalSolution n y| ≤ ε ^ 2 / 2

Bound on $\int_{|y|<\varepsilon} |\Phi(y)|\,dy \le \varepsilon^2/2$ for $n \ge 3$.

theorem LaplacePoisson.unitSphereArea_ge_dim_sub_two {n : ℕ} (_hn : n ≥ 3) : ↑n - 2 ≤ unitSphereArea n

Crude lower bound on the surface area of the unit sphere: $n - 2 \le \omega_n$ for $n \ge 3$.

theorem LaplacePoisson.polar_coord_radial_integral {n : ℕ} (hn : n ≥ 3) (ε : ℝ) (hε : 0 < ε) : ∫ (y : Fin n → ℝ) in {z : Fin n → ℝ | euclidNormLP z < ε}, |fundamentalSolution n y| ≤ unitSphereArea n / (2 * (↑n - 2)) * ε ^ 2

Polar-coordinate bound on $\int_{|y|<\varepsilon} |\Phi(y)|\,dy \le \omega_n / (2(n-2)) \cdot \varepsilon^2$ for $n \ge 3$.

theorem LaplacePoisson.fundamentalSolution_integral_near_origin_bound {n : ℕ} (hn : n ≥ 3) (ε : ℝ) (hε : 0 < ε) : ∫ (y : Fin n → ℝ) in {z : Fin n → ℝ | euclidNormLP z < ε}, |fundamentalSolution n y| ≤ unitSphereArea n / (2 * (↑n - 2)) * ε ^ 2

Restatement of polar_coord_radial_integral used downstream.

theorem LaplacePoisson.fundamentalSolution_abs_integrableOn_ball {n : ℕ} (_hn : n ≥ 3) (ε : ℝ) (_hε : 0 < ε) : MeasureTheory.IntegrableOn (fun (y : Fin n → ℝ) => |fundamentalSolution n y|) {z : Fin n → ℝ | euclidNormLP z < ε} MeasureTheory.volume

$|\Phi|$ is integrable on the Euclidean ball of radius $\varepsilon$ for $n \ge 3$.

theorem LaplacePoisson.fundamentalSolution_mul_bounded_integrableOn_ball {n : ℕ} (_hn : n ≥ 3) (g : (Fin n → ℝ) → ℝ) (ε : ℝ) (_hε : 0 < ε) (_hg_bound : ∃ (M : ℝ), ∀ (y : Fin n → ℝ), |g y| ≤ M) : MeasureTheory.IntegrableOn (fun (y : Fin n → ℝ) => fundamentalSolution n y * g y) {z : Fin n → ℝ | euclidNormLP z < ε} MeasureTheory.volume

For a bounded function $g$, the product $\Phi \cdot g$ is integrable on the Euclidean ball of radius $\varepsilon$ for $n \ge 3$.

theorem LaplacePoisson.fundamentalSolution_locallyIntegrable {n : ℕ} (_hn : n ≥ 2) : MeasureTheory.LocallyIntegrable (fundamentalSolution n) MeasureTheory.volume

The fundamental solution $\Phi$ is locally integrable on $\mathbb{R}^n$ for $n \ge 2$.

theorem LaplacePoisson.near_field_spherical_bound {n : ℕ} (hn : n ≥ 3) (f : (Fin n → ℝ) → ℝ) (hf_smooth : ContDiff ℝ ⊤ f) (hf_supp : HasCompactSupport f) (x : Fin n → ℝ) : ∃ (C : ℝ), ∀ (ε : ℝ), 0 < ε → ‖∫ (y : Fin n → ℝ) in {z : Fin n → ℝ | euclidNormLP z < ε}, fundamentalSolution n y * laplacianLP (fun (z : Fin n → ℝ) => f (x - z)) y‖ ≤ C * ε ^ 2

Near-origin estimate: the integral of $\Phi(y) \, \Delta_z f(x - z)|_y$ over the ball of radius $\varepsilon$ is $O(\varepsilon^2)$.

theorem LaplacePoisson.near_field_integral_vanishes {n : ℕ} (hn : n ≥ 3) (f : (Fin n → ℝ) → ℝ) (hf_smooth : ContDiff ℝ ⊤ f) (hf_supp : HasCompactSupport f) (x : Fin n → ℝ) : Filter.Tendsto (fun (ε : ℝ) => ∫ (y : Fin n → ℝ) in {z : Fin n → ℝ | euclidNormLP z < ε}, fundamentalSolution n y * laplacianLP (fun (z : Fin n → ℝ) => f (x - z)) y) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

The near-origin contribution to the convolution integral vanishes as $\varepsilon \to 0^+$.

theorem LaplacePoisson.greens_second_identity_exterior_compactSupp {n : ℕ} (hn : n ≥ 3) (u v : (Fin n → ℝ) → ℝ) (hu_smooth : ContDiff ℝ ⊤ u) (hu_supp : HasCompactSupport u) (ε : ℝ) (hε : 0 < ε) (hv_harmonic : ∀ (y : Fin n → ℝ), euclidNormLP y ≥ ε → laplacianLP v y = 0) : ∫ (y : Fin n → ℝ) in {z : Fin n → ℝ | euclidNormLP z ≥ ε}, v y * laplacianLP u y = surfaceIntegralLP {z : Fin n → ℝ | euclidNormLP z = ε} fun (σ : Fin n → ℝ) => v σ * normalDerivLP {z : Fin n → ℝ | euclidNormLP z ≥ ε} u σ - u σ * normalDerivLP {z : Fin n → ℝ | euclidNormLP z ≥ ε} v σ

Green's second identity on the exterior $\{|z| \ge \varepsilon\}$, using that $u$ is compactly supported (so boundary contributions at infinity vanish) and that $v$ is harmonic in this region.

theorem LaplacePoisson.greens_identity_annular_reduction {n : ℕ} (_hn : n ≥ 3) (f : (Fin n → ℝ) → ℝ) (_hf_smooth : ContDiff ℝ ⊤ f) (_hf_supp : HasCompactSupport f) (x : Fin n → ℝ) (ε : ℝ) (_hε : 0 < ε) : ∫ (y : Fin n → ℝ) in {z : Fin n → ℝ | euclidNormLP z ≥ ε}, fundamentalSolution n y * laplacianLP (fun (z : Fin n → ℝ) => f (x - z)) y = surfaceIntegralLP {z : Fin n → ℝ | euclidNormLP z = ε} fun (σ : Fin n → ℝ) => fundamentalSolution n σ * normalDerivLP {z : Fin n → ℝ | euclidNormLP z ≥ ε} (fun (z : Fin n → ℝ) => f (x - z)) σ - f (x - σ) * normalDerivLP {z : Fin n → ℝ | euclidNormLP z ≥ ε} (fundamentalSolution n) σ

Application of Green's identity in the exterior region to the pair $(\text{f-translated},\, \Phi)$: the exterior volume integral becomes a surface integral over $\{|z| = \varepsilon\}$.

theorem LaplacePoisson.surfaceMeasure_sphere_finite {n : ℕ} (ε : ℝ) (_hε : 0 < ε) : (surfaceMeasure {z : Fin n → ℝ | euclidNormLP z = ε}) (frontier {z : Fin n → ℝ | euclidNormLP z = ε}) < ⊤

The surface measure of the sphere $\{|z| = \varepsilon\}$ is finite.

theorem LaplacePoisson.surfaceMeasure_sphere_real_le {n : ℕ} (ε : ℝ) (hε : 0 < ε) : (surfaceMeasure {z : Fin n → ℝ | euclidNormLP z = ε}).real (frontier {z : Fin n → ℝ | euclidNormLP z = ε}) ≤ ↑n * unitSphereArea n * ε ^ (n - 1)

Crude upper bound on the surface measure of $\{|z| = \varepsilon\}$: $\le n \omega_n \varepsilon^{n-1}$.

theorem LaplacePoisson.normalDerivLP_uniform_bound_of_smooth_compactSupport {n : ℕ} (f : (Fin n → ℝ) → ℝ) (_hf_smooth : ContDiff ℝ ⊤ f) (_hf_supp : HasCompactSupport f) : ∃ (M : ℝ), 0 ≤ M ∧ ∀ (Ω : Set (Fin n → ℝ)) (σ : Fin n → ℝ), |normalDerivLP Ω f σ| ≤ M

The normal derivative of a smooth compactly supported function admits a uniform bound that is independent of the domain $\Omega$ and point $\sigma$.

theorem LaplacePoisson.surface_gradient_term_bounded {n : ℕ} (_hn : n ≥ 3) (f : (Fin n → ℝ) → ℝ) (_hf_smooth : ContDiff ℝ ⊤ f) (_hf_supp : HasCompactSupport f) (x : Fin n → ℝ) : ∃ (C : ℝ), ∀ ε > 0, ‖surfaceIntegralLP {z : Fin n → ℝ | euclidNormLP z = ε} fun (σ : Fin n → ℝ) => fundamentalSolution n σ * normalDerivLP {z : Fin n → ℝ | euclidNormLP z ≥ ε} (fun (z : Fin n → ℝ) => f (x - z)) σ‖ ≤ C * ε

The boundary integral $\int_{|z| = \varepsilon} \Phi(\sigma)\, \partial_\nu f(x - \sigma)\,dS$ is bounded by $C \varepsilon$ for some constant $C$ independent of $\varepsilon$.

theorem LaplacePoisson.surfaceIntegralLP_normalDeriv_Phi_origin_eq_neg_one {n : ℕ} (hn : n ≥ 3) (ε : ℝ) (hε : 0 < ε) : (surfaceIntegralLP {z : Fin n → ℝ | euclidNormLP z = ε} fun (σ : Fin n → ℝ) => normalDerivLP {z : Fin n → ℝ | euclidNormLP z ≥ ε} (fundamentalSolution n) σ) = -1

Normalization identity: $\int_{|σ|=\varepsilon} \partial_\nu \Phi(\sigma)\,dS = -1$ for $n \ge 3$. This is the key fact that produces $f(x)$ in the Poisson formula.

theorem LaplacePoisson.surfaceIntegralLP_origin_bddAbove_aux {n : ℕ} (hn : n ≥ 3) (g : (Fin n → ℝ) → ℝ) (ε : ℝ) (hε : 0 < ε) (hint : MeasureTheory.IntegrableOn g (frontier {z : Fin n → ℝ | euclidNormLP z = ε}) (surfaceMeasure {z : Fin n → ℝ | euclidNormLP z = ε})) : BddAbove (Set.range fun (σ : Fin n → ℝ) => ⨆ (_ : σ ∈ frontier {z : Fin n → ℝ | euclidNormLP z = ε}), |g σ|)

Technical auxiliary: the supremum-indicator family $\sigma \mapsto \sup_{\sigma \in \partial S} |g(\sigma)|$ is bounded above when $g$ is integrable on the sphere.

theorem LaplacePoisson.surfaceIntegralLP_origin_oscillation_bound {n : ℕ} (hn : n ≥ 3) (g : (Fin n → ℝ) → ℝ) (ε : ℝ) (hε : 0 < ε) : ‖surfaceIntegralLP {z : Fin n → ℝ | euclidNormLP z = ε} fun (σ : Fin n → ℝ) => g σ * normalDerivLP {z : Fin n → ℝ | euclidNormLP z ≥ ε} (fundamentalSolution n) σ‖ ≤ ⨆ σ ∈ frontier {z : Fin n → ℝ | euclidNormLP z = ε}, |g σ|

Oscillation bound: the surface integral $\int_{|\sigma|=\varepsilon} g(\sigma)\, \partial_\nu \Phi(\sigma)\,dS$ is bounded by the supremum of $|g|$ over the sphere. This uses the identity $\partial_\nu \Phi = -\frac{1}{\omega_n \varepsilon^{n-1}}$ together with the area of the sphere being $\omega_n \varepsilon^{n-1}$.

theorem LaplacePoisson.norm_le_euclidNormLP {n : ℕ} (σ : Fin n → ℝ) : ‖σ‖ ≤ euclidNormLP σ

The sup-norm on $\mathbb{R}^n$ is dominated by the Euclidean L² norm: $\|\sigma\|_\infty \le \|\sigma\|_2$.

theorem LaplacePoisson.oscillation_origin_sphere_tendsto_zero {n : ℕ} (f : (Fin n → ℝ) → ℝ) (hf : Continuous f) (x : Fin n → ℝ) : Filter.Tendsto (fun (ε : ℝ) => ⨆ σ ∈ frontier {z : Fin n → ℝ | euclidNormLP z = ε}, |f (x - σ) - f x|) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

Continuity at $x$ implies that the oscillation $\sup_{|\sigma|=\varepsilon} |f(x-\sigma) - f(x)|$ tends to $0$ as $\varepsilon \to 0^+$.

theorem LaplacePoisson.surfaceIntegral_integrable_LP_early {n : ℕ} (Ω : Set (Fin n → ℝ)) (f : (Fin n → ℝ) → ℝ) : MeasureTheory.IntegrableOn f (frontier Ω) (surfaceMeasure Ω)

Integrability on the boundary $\partial\Omega$: every function is integrable against the (auxiliary) surface measure used in this development.

theorem LaplacePoisson.surface_fvalue_decomposition {n : ℕ} (hn : n ≥ 3) (f : (Fin n → ℝ) → ℝ) (hf_smooth : ContDiff ℝ ⊤ f) (hf_supp : HasCompactSupport f) (x : Fin n → ℝ) : ∃ (error : ℝ → ℝ), (∀ ε > 0, (-surfaceIntegralLP {z : Fin n → ℝ | euclidNormLP z = ε} fun (σ : Fin n → ℝ) => f (x - σ) * normalDerivLP {z : Fin n → ℝ | euclidNormLP z ≥ ε} (fundamentalSolution n) σ) = f x + error ε) ∧ Filter.Tendsto error (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

Decomposition of the surface integral of $f(x-\sigma)\,\partial_\nu \Phi(\sigma)$: this equals $-f(x)$ plus an error term that vanishes as $\varepsilon \to 0^+$.

theorem LaplacePoisson.surface_fvalue_term_limit {n : ℕ} (hn : n ≥ 3) (f : (Fin n → ℝ) → ℝ) (hf_smooth : ContDiff ℝ ⊤ f) (hf_supp : HasCompactSupport f) (x : Fin n → ℝ) : Filter.Tendsto (fun (ε : ℝ) => -surfaceIntegralLP {z : Fin n → ℝ | euclidNormLP z = ε} fun (σ : Fin n → ℝ) => f (x - σ) * normalDerivLP {z : Fin n → ℝ | euclidNormLP z ≥ ε} (fundamentalSolution n) σ) (nhdsWithin 0 (Set.Ioi 0)) (nhds (f x))

Pointwise limit: $-\int_{|\sigma|=\varepsilon} f(x-\sigma)\,\partial_\nu \Phi(\sigma)\, dS \to f(x)$ as $\varepsilon \to 0^+$. This is the source of the Dirac delta in the Poisson formula.

theorem LaplacePoisson.far_field_greens_computation {n : ℕ} (hn : n ≥ 3) (f : (Fin n → ℝ) → ℝ) (hf_smooth : ContDiff ℝ ⊤ f) (hf_supp : HasCompactSupport f) (x : Fin n → ℝ) : ∃ (gradient_term : ℝ → ℝ) (f_term : ℝ → ℝ), (∀ ε > 0, ∫ (y : Fin n → ℝ) in {z : Fin n → ℝ | euclidNormLP z ≥ ε}, fundamentalSolution n y * laplacianLP (fun (z : Fin n → ℝ) => f (x - z)) y = gradient_term ε + f_term ε) ∧ (∃ (C : ℝ), ∀ ε > 0, ‖gradient_term ε‖ ≤ C * ε) ∧ Filter.Tendsto f_term (nhdsWithin 0 (Set.Ioi 0)) (nhds (f x))

Far-field Green's identity computation: the volume integral $\int_{|z|\ge \varepsilon} \Phi(y)\,\Delta f(x-y)\,dy$ decomposes as a "gradient term" that is $O(\varepsilon)$ plus an "$f$-term" that converges to $f(x)$.

theorem LaplacePoisson.far_field_greens_identity_decomposition {n : ℕ} (hn : n ≥ 3) (f : (Fin n → ℝ) → ℝ) (hf_smooth : ContDiff ℝ ⊤ f) (hf_supp : HasCompactSupport f) (x : Fin n → ℝ) : ∃ (gradient_term : ℝ → ℝ) (f_term : ℝ → ℝ), (∀ ε > 0, ∫ (y : Fin n → ℝ) in {z : Fin n → ℝ | euclidNormLP z ≥ ε}, fundamentalSolution n y * laplacianLP (fun (z : Fin n → ℝ) => f (x - z)) y = gradient_term ε + f_term ε) ∧ Filter.Tendsto gradient_term (nhdsWithin 0 (Set.Ioi 0)) (nhds 0) ∧ Filter.Tendsto f_term (nhdsWithin 0 (Set.Ioi 0)) (nhds (f x))

Stronger version of the far-field decomposition: the "gradient term" actually tends to $0$ (rather than merely being $O(\varepsilon)$).

theorem LaplacePoisson.far_field_integral_limit {n : ℕ} (hn : n ≥ 3) (f : (Fin n → ℝ) → ℝ) (hf_smooth : ContDiff ℝ ⊤ f) (hf_supp : HasCompactSupport f) (x : Fin n → ℝ) : Filter.Tendsto (fun (ε : ℝ) => ∫ (y : Fin n → ℝ) in {z : Fin n → ℝ | euclidNormLP z ≥ ε}, fundamentalSolution n y * laplacianLP (fun (z : Fin n → ℝ) => f (x - z)) y) (nhdsWithin 0 (Set.Ioi 0)) (nhds (f x))

The far-field integral converges to $f(x)$: $\int_{|y|\ge\varepsilon} \Phi(y)\,\Delta f(x-y)\,dy \to f(x)$ as $\varepsilon \to 0^+$.

theorem LaplacePoisson.fundamentalSolution_laplacian_integrableOn {n : ℕ} (u : (Fin n → ℝ) → ℝ) (Ω : Set (Fin n → ℝ)) (hu : ContDiffOn ℝ 2 u (closure Ω)) (hΩ : IsOpen Ω) (x : Fin n → ℝ) (hx : x ∈ Ω) : MeasureTheory.IntegrableOn (fun (y : Fin n → ℝ) => fundamentalSolution n (x - y) * laplacianLP u y) Ω MeasureTheory.volume

Integrability of the convolution kernel: $y \mapsto \Phi(x - y)\,\Delta u(y)$ is integrable on $\Omega$ when $u$ is $C^2$ on $\overline{\Omega}$.

theorem LaplacePoisson.convolution_integrand_integrable {n : ℕ} (f : (Fin n → ℝ) → ℝ) (hf_smooth : ContDiff ℝ ⊤ f) (hf_supp : HasCompactSupport f) (x : Fin n → ℝ) : MeasureTheory.Integrable (fun (y : Fin n → ℝ) => fundamentalSolution n y * laplacianLP (fun (z : Fin n → ℝ) => f (x - z)) y) MeasureTheory.volume

Integrability of the convolution integrand $y \mapsto \Phi(y)\,\Delta f(x-y)$ on $\mathbb{R}^n$, for smooth compactly supported $f$.

theorem LaplacePoisson.integral_split_ball_complement {n : ℕ} (g : (Fin n → ℝ) → ℝ) (ε : ℝ) (_hε : ε > 0) (hg : MeasureTheory.Integrable g MeasureTheory.volume) : ∫ (y : Fin n → ℝ), g y = (∫ (y : Fin n → ℝ) in {z : Fin n → ℝ | euclidNormLP z < ε}, g y) + ∫ (y : Fin n → ℝ) in {z : Fin n → ℝ | euclidNormLP z ≥ ε}, g y

Decomposition of an integral on $\mathbb{R}^n$ as a sum of an integral over the open ball $\{|y|<\varepsilon\}$ and over its complement $\{|y|\ge\varepsilon\}$.

theorem LaplacePoisson.poisson_convolution_laplacian {n : ℕ} (hn : n ≥ 3) (f : (Fin n → ℝ) → ℝ) (hf_smooth : ContDiff ℝ ⊤ f) (hf_supp : HasCompactSupport f) (x : Fin n → ℝ) : laplacianLP (phiConvolutionLP n f) x = f x

Core PDE identity for $n \ge 3$ (Theorem 1.1): the Laplacian of the convolution $u = \Phi * f$ recovers $f$, i.e.\ $\Delta(\Phi * f) = f$ on $\mathbb{R}^n$.

theorem LaplacePoisson.poisson_equation_solution {n : ℕ} (hn : n ≥ 3) (f : (Fin n → ℝ) → ℝ) (hf_smooth : ContDiff ℝ ⊤ f) (hf_supp : HasCompactSupport f) (x : Fin n → ℝ) : laplacianLP (phiConvolutionLP n f) x = f x

Universal-quantifier form: for $n \ge 3$, $u = \Phi * f$ solves $\Delta u = f$ everywhere on $\mathbb{R}^n$.

theorem LaplacePoisson.laplacian_convolution_eq_integral_n2 (f : (Fin 2 → ℝ) → ℝ) (hf_smooth : ContDiff ℝ ⊤ f) (hf_supp : HasCompactSupport f) (x : Fin 2 → ℝ) : laplacianLP (phiConvolutionLP 2 f) x = ∫ (y : Fin 2 → ℝ), fundamentalSolution 2 y * laplacianLP (fun (z : Fin 2 → ℝ) => f (x - z)) y

$n = 2$ variant of laplacian_convolution_eq_integral: the Laplacian of the convolution $\Phi * f$ equals $\int \Phi(y)\,\Delta f(x-y)\,dy$.

theorem LaplacePoisson.near_field_spherical_bound_n2 (f : (Fin 2 → ℝ) → ℝ) (hf_smooth : ContDiff ℝ ⊤ f) (hf_supp : HasCompactSupport f) (x : Fin 2 → ℝ) : ∃ (C : ℝ), ∀ (ε : ℝ), 0 < ε → ε < 1 → ‖∫ (y : Fin 2 → ℝ) in {z : Fin 2 → ℝ | euclidNormLP z < ε}, fundamentalSolution 2 y * laplacianLP (fun (z : Fin 2 → ℝ) => f (x - z)) y‖ ≤ C * (ε ^ 2 * |Real.log ε|)

$n = 2$ near-field bound: $\bigl|\int_{|y|<\varepsilon} \Phi(y)\, \Delta f(x-y)\,dy\bigr| \le C\,\varepsilon^2\,|\log \varepsilon|$ for $0 < \varepsilon < 1$.

theorem LaplacePoisson.eps_sq_abs_log_tendsto_zero : Filter.Tendsto (fun (ε : ℝ) => ε ^ 2 * |Real.log ε|) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

Auxiliary limit for $n = 2$: $\varepsilon^2\,|\log \varepsilon| \to 0$ as $\varepsilon \to 0^+$.

theorem LaplacePoisson.near_field_integral_vanishes_n2 (f : (Fin 2 → ℝ) → ℝ) (hf_smooth : ContDiff ℝ ⊤ f) (hf_supp : HasCompactSupport f) (x : Fin 2 → ℝ) : Filter.Tendsto (fun (ε : ℝ) => ∫ (y : Fin 2 → ℝ) in {z : Fin 2 → ℝ | euclidNormLP z < ε}, fundamentalSolution 2 y * laplacianLP (fun (z : Fin 2 → ℝ) => f (x - z)) y) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

$n = 2$ near-field vanishing: the integral over the small ball vanishes as $\varepsilon \to 0^+$.

theorem LaplacePoisson.far_field_greens_identity_decomposition_n2 (f : (Fin 2 → ℝ) → ℝ) (hf_smooth : ContDiff ℝ ⊤ f) (hf_supp : HasCompactSupport f) (x : Fin 2 → ℝ) : ∃ (gradient_term : ℝ → ℝ) (f_term : ℝ → ℝ), (∀ ε > 0, ∫ (y : Fin 2 → ℝ) in {z : Fin 2 → ℝ | euclidNormLP z ≥ ε}, fundamentalSolution 2 y * laplacianLP (fun (z : Fin 2 → ℝ) => f (x - z)) y = gradient_term ε + f_term ε) ∧ Filter.Tendsto gradient_term (nhdsWithin 0 (Set.Ioi 0)) (nhds 0) ∧ Filter.Tendsto f_term (nhdsWithin 0 (Set.Ioi 0)) (nhds (f x))

$n = 2$ far-field Green's identity decomposition: same shape as the $n \ge 3$ case but with the logarithmic fundamental solution.

theorem LaplacePoisson.far_field_integral_limit_n2 (f : (Fin 2 → ℝ) → ℝ) (hf_smooth : ContDiff ℝ ⊤ f) (hf_supp : HasCompactSupport f) (x : Fin 2 → ℝ) : Filter.Tendsto (fun (ε : ℝ) => ∫ (y : Fin 2 → ℝ) in {z : Fin 2 → ℝ | euclidNormLP z ≥ ε}, fundamentalSolution 2 y * laplacianLP (fun (z : Fin 2 → ℝ) => f (x - z)) y) (nhdsWithin 0 (Set.Ioi 0)) (nhds (f x))

$n = 2$ far-field integral limit: $\int_{|y|\ge\varepsilon} \Phi(y)\, \Delta f(x-y)\,dy \to f(x)$ as $\varepsilon \to 0^+$.

theorem LaplacePoisson.poisson_convolution_laplacian_n2 (f : (Fin 2 → ℝ) → ℝ) (hf_smooth : ContDiff ℝ ⊤ f) (hf_supp : HasCompactSupport f) (x : Fin 2 → ℝ) : laplacianLP (phiConvolutionLP 2 f) x = f x

$n = 2$ version of the Poisson formula: $\Delta(\Phi * f) = f$ on $\mathbb{R}^2$.

theorem LaplacePoisson.contDiff_convolution_locallyIntegrable_compactSupport {n : ℕ} (_hn : n ≥ 2) (K : (Fin n → ℝ) → ℝ) (_hK : MeasureTheory.LocallyIntegrable K MeasureTheory.volume) (g : (Fin n → ℝ) → ℝ) (_hg_smooth : ContDiff ℝ ⊤ g) (_hg_supp : HasCompactSupport g) : ContDiff ℝ ⊤ fun (x : Fin n → ℝ) => ∫ (y : Fin n → ℝ), K (x - y) * g y

Smoothness of convolution: convolution of a locally integrable kernel $K$ with a smooth compactly supported function $g$ is smooth, $K * g \in C^\infty$.

theorem LaplacePoisson.poisson_solution_smooth {n : ℕ} (hn : n ≥ 2) (f : (Fin n → ℝ) → ℝ) (hf_smooth : ContDiff ℝ ⊤ f) (hf_supp : HasCompactSupport f) : ContDiff ℝ ⊤ (phiConvolutionLP n f)

The Poisson solution $u = \Phi * f$ is smooth: $u \in C^\infty(\mathbb{R}^n)$ whenever $f \in C_c^\infty(\mathbb{R}^n)$.

theorem LaplacePoisson.poisson_solution_decay_nge3 {n : ℕ} (hn : n ≥ 3) (f : (Fin n → ℝ) → ℝ) (hf_smooth : ContDiff ℝ ⊤ f) (hf_supp : HasCompactSupport f) : ∃ C > 0, ∀ (x : Fin n → ℝ), euclidNormLP x ≥ 1 → |phiConvolutionLP n f x| ≤ C / euclidNormLP x ^ (n - 2)

Pointwise decay estimate at infinity for $n \ge 3$: there exists $C > 0$ such that $|(\Phi * f)(x)| \le C / |x|^{n-2}$ for $|x| \ge 1$.

theorem LaplacePoisson.poisson_solution_tendsto_zero_nge3 {n : ℕ} (hn : n ≥ 3) (f : (Fin n → ℝ) → ℝ) (hf_smooth : ContDiff ℝ ⊤ f) (hf_supp : HasCompactSupport f) : Filter.Tendsto (phiConvolutionLP n f) (Filter.cocompact (Fin n → ℝ)) (nhds 0)

Decay at infinity (consequence of the $1/|x|^{n-2}$ bound): for $n \ge 3$, $(\Phi * f)(x) \to 0$ as $|x| \to \infty$.

theorem LaplacePoisson.poisson_solution_unique_nge3 {n : ℕ} (hn : n ≥ 3) (u₁ u₂ f : (Fin n → ℝ) → ℝ) (hu₁_smooth : ContDiff ℝ ⊤ u₁) (hu₂_smooth : ContDiff ℝ ⊤ u₂) (hu₁_pde : ∀ (x : Fin n → ℝ), laplacianLP u₁ x = f x) (hu₂_pde : ∀ (x : Fin n → ℝ), laplacianLP u₂ x = f x) (hu₁_decay : Filter.Tendsto u₁ (Filter.cocompact (Fin n → ℝ)) (nhds 0)) (hu₂_decay : Filter.Tendsto u₂ (Filter.cocompact (Fin n → ℝ)) (nhds 0)) : u₁ = u₂

Uniqueness for Poisson's equation under decay at infinity (Liouville-type argument): two smooth solutions of $\Delta u = f$ that both vanish at infinity must agree, for $n \ge 3$.

theorem LaplacePoisson.poisson_theorem_1_1 {n : ℕ} (hn : n ≥ 3) (f : (Fin n → ℝ) → ℝ) (hf_smooth : ContDiff ℝ ⊤ f) (hf_supp : HasCompactSupport f) : (∀ (x : Fin n → ℝ), laplacianLP (phiConvolutionLP n f) x = f x) ∧ ContDiff ℝ ⊤ (phiConvolutionLP n f) ∧ (∃ C > 0, ∀ (x : Fin n → ℝ), euclidNormLP x ≥ 1 → |phiConvolutionLP n f x| ≤ C / euclidNormLP x ^ (n - 2)) ∧ Filter.Tendsto (phiConvolutionLP n f) (Filter.cocompact (Fin n → ℝ)) (nhds 0) ∧ ∀ (u₁ u₂ : (Fin n → ℝ) → ℝ), ContDiff ℝ ⊤ u₁ → ContDiff ℝ ⊤ u₂ → (∀ (x : Fin n → ℝ), laplacianLP u₁ x = f x) → (∀ (x : Fin n → ℝ), laplacianLP u₂ x = f x) → Filter.Tendsto u₁ (Filter.cocompact (Fin n → ℝ)) (nhds 0) → Filter.Tendsto u₂ (Filter.cocompact (Fin n → ℝ)) (nhds 0) → u₁ = u₂

Theorem 1.1 (CM7). For $n \ge 3$ and $f \in C_c^\infty(\mathbb{R}^n)$, the convolution $u = \Phi * f$ is the unique smooth solution to Poisson's equation $\Delta u = f$ that vanishes at infinity, with the explicit decay rate $|u(x)| \lesssim |x|^{2-n}$.

theorem LaplacePoisson.dirichlet_basic_existence {n : ℕ} (Ω : Set (Fin n → ℝ)) (hΩ : IsOpen Ω) (hΩb : Bornology.IsBounded Ω) (hΩ_lip : IsLipschitzDomain Ω) (f g : (Fin n → ℝ) → ℝ) (hg : ContinuousOn g (frontier Ω)) : ∃ (u : (Fin n → ℝ) → ℝ), ContDiffOn ℝ 2 u Ω ∧ ContinuousOn u (closure Ω) ∧ (∀ x ∈ Ω, laplacianLP u x = f x) ∧ (∀ σ ∈ frontier Ω, u σ = g σ) ∧ ∀ (u' : (Fin n → ℝ) → ℝ), ContDiffOn ℝ 2 u' Ω → ContinuousOn u' (closure Ω) → (∀ x ∈ Ω, laplacianLP u' x = f x) → (∀ σ ∈ frontier Ω, u' σ = g σ) → ∀ x ∈ closure Ω, u' x = u x

Basic existence and uniqueness for the Dirichlet problem on a bounded Lipschitz domain: for given $f$ (interior) and continuous boundary data $g$, there is a unique $C^2$ solution $u$ of $\Delta u = f$ in $\Omega$ with $u = g$ on $\partial\Omega$.

theorem LaplacePoisson.dirichlet_uniqueness {n : ℕ} (hn : 0 < n) (Ω : Set (Fin n → ℝ)) (hΩ : IsOpen Ω) (hΩc : IsConnected Ω) (hΩb : Bornology.IsBounded Ω) (u₁ u₂ f g : (Fin n → ℝ) → ℝ) (hu₁_reg : ContDiffOn ℝ 2 u₁ Ω) (hu₁_cont : ContinuousOn u₁ (closure Ω)) (hu₂_reg : ContDiffOn ℝ 2 u₂ Ω) (hu₂_cont : ContinuousOn u₂ (closure Ω)) (hu₁_pde : ∀ x ∈ Ω, laplacianLP u₁ x = f x) (hu₂_pde : ∀ x ∈ Ω, laplacianLP u₂ x = f x) (hu₁_bdy : ∀ σ ∈ frontier Ω, u₁ σ = g σ) (hu₂_bdy : ∀ σ ∈ frontier Ω, u₂ σ = g σ) (x : Fin n → ℝ) : x ∈ closure Ω → u₁ x = u₂ x

Uniqueness for the Dirichlet problem on a bounded connected Lipschitz domain via the maximum principle: if $u_1, u_2$ both solve $\Delta u = f$ in $\Omega$ with the same boundary data $g$, then $u_1 = u_2$ on $\overline{\Omega}$.

structure LaplacePoisson.GreenFunctionLP (n : ℕ) (Ω : Set (Fin n → ℝ)) : Type

Bundled Green's function for the Dirichlet Laplacian on a domain $\Omega$: $G(x, \cdot)$ vanishes on $\partial\Omega$, satisfies the distributional identity $\Delta_y G(x, y) = -\delta_x$ (here stated against test functions), and comes with the integrability data needed for Green's representation formula.

• G : (Fin n → ℝ) → (Fin n → ℝ) → ℝ
• domain_open : IsOpen Ω
• boundary_zero (x : Fin n → ℝ) : x ∈ Ω → ∀ σ ∈ frontier Ω, self.G x σ = 0
• distributional_pde (x : Fin n → ℝ) : x ∈ Ω → ∀ (φ : (Fin n → ℝ) → ℝ), ContDiff ℝ 2 φ → HasCompactSupport φ → tsupport φ ⊆ Ω → ∫ (y : Fin n → ℝ), self.G x y * laplacianLP φ y = φ x
• G_differentiable (x : Fin n → ℝ) : x ∈ Ω → ∀ (σ : Fin n → ℝ), DifferentiableAt ℝ (self.G x) σ
• Phi_differentiable (x σ : Fin n → ℝ) : DifferentiableAt ℝ (fun (y : Fin n → ℝ) => fundamentalSolution n (x - y)) σ
• G_mul_integrableOn (x : Fin n → ℝ) : x ∈ Ω → ∀ (f : (Fin n → ℝ) → ℝ), Bornology.IsBounded Ω → MeasureTheory.IntegrableOn (fun (y : Fin n → ℝ) => self.G x y * f y) Ω MeasureTheory.volume
• Phi_mul_integrableOn (x : Fin n → ℝ) (f : (Fin n → ℝ) → ℝ) : Bornology.IsBounded Ω → MeasureTheory.IntegrableOn (fun (y : Fin n → ℝ) => fundamentalSolution n (x - y) * f y) Ω MeasureTheory.volume
• G_normalDeriv_integrableOn (x : Fin n → ℝ) : x ∈ Ω → ∀ (g : (Fin n → ℝ) → ℝ), MeasureTheory.IntegrableOn (fun (σ : Fin n → ℝ) => g σ * normalDerivLP Ω (self.G x) σ) (frontier Ω) (surfaceMeasure Ω)
• Phi_normalDeriv_integrableOn (x : Fin n → ℝ) (g : (Fin n → ℝ) → ℝ) : MeasureTheory.IntegrableOn (fun (σ : Fin n → ℝ) => g σ * normalDerivLP Ω (fun (y : Fin n → ℝ) => fundamentalSolution n (x - y)) σ) (frontier Ω) (surfaceMeasure Ω)

theorem LaplacePoisson.weyl_lemma_LP {n : ℕ} (Ω : Set (Fin n → ℝ)) (hΩ : IsOpen Ω) (u : (Fin n → ℝ) → ℝ) (h_dist : ∀ (ψ : (Fin n → ℝ) → ℝ), ContDiff ℝ ⊤ ψ → HasCompactSupport ψ → tsupport ψ ⊆ Ω → ∫ (y : Fin n → ℝ), u y * laplacianLP ψ y = 0) : IsHarmonicLP u Ω

Weyl's lemma: a function whose integral against $\Delta\psi$ vanishes for every test function $\psi$ supported in $\Omega$ is necessarily smooth and harmonic on $\Omega$.

theorem LaplacePoisson.fundamental_solution_distributional_delta_LP {n : ℕ} (hn : n ≥ 2) (x : Fin n → ℝ) (ψ : (Fin n → ℝ) → ℝ) (hψ : ContDiff ℝ ⊤ ψ) (hψs : HasCompactSupport ψ) : ∫ (y : Fin n → ℝ), fundamentalSolution n (x - y) * laplacianLP ψ y = ψ x

Distributional identity $\Delta \Phi = \delta_0$: for any test function $\psi$, $\int \Phi(x - y)\,\Delta\psi(y)\,dy = \psi(x)$.

theorem LaplacePoisson.fundamentalSolution_laplacian_integrable {n : ℕ} (x : Fin n → ℝ) (ψ : (Fin n → ℝ) → ℝ) (hψ : ContDiff ℝ 2 ψ) (hψs : HasCompactSupport ψ) : MeasureTheory.Integrable (fun (y : Fin n → ℝ) => fundamentalSolution n (x - y) * laplacianLP ψ y) MeasureTheory.volume

Global integrability of $y \mapsto \Phi(x - y)\,\Delta\psi(y)$ when $\psi$ is $C^2$ with compact support.

theorem LaplacePoisson.green_function_laplacian_integrable {n : ℕ} {Ω : Set (Fin n → ℝ)} (gf : GreenFunctionLP n Ω) (x : Fin n → ℝ) (ψ : (Fin n → ℝ) → ℝ) (hψ : ContDiff ℝ 2 ψ) (hψs : HasCompactSupport ψ) : MeasureTheory.Integrable (fun (y : Fin n → ℝ) => gf.G x y * laplacianLP ψ y) MeasureTheory.volume

Global integrability of $y \mapsto G(x, y)\,\Delta\psi(y)$, where $G$ is a Green function and $\psi$ is a $C^2$ compactly supported test function.

theorem LaplacePoisson.corrector_integrand_integrable_LP {n : ℕ} {Ω : Set (Fin n → ℝ)} (gf : GreenFunctionLP n Ω) (x : Fin n → ℝ) (ψ : (Fin n → ℝ) → ℝ) (hψ : ContDiff ℝ 2 ψ) (hψs : HasCompactSupport ψ) : MeasureTheory.Integrable (fun (y : Fin n → ℝ) => fundamentalSolution n (x - y) * laplacianLP ψ y) MeasureTheory.volume ∧ MeasureTheory.Integrable (fun (y : Fin n → ℝ) => gf.G x y * laplacianLP ψ y) MeasureTheory.volume

Joint integrability used when subtracting $\Phi$ and $G$ to obtain the corrector.

theorem LaplacePoisson.green_corrector_harmonic {n : ℕ} {Ω : Set (Fin n → ℝ)} (hn : n ≥ 2) (gf : GreenFunctionLP n Ω) (x : Fin n → ℝ) (hx : x ∈ Ω) : IsHarmonicLP (fun (y : Fin n → ℝ) => fundamentalSolution n (x - y) - gf.G x y) Ω

The Green corrector $h(y) = \Phi(x - y) - G(x, y)$ is harmonic on $\Omega$: this follows from Weyl's lemma since $\Delta_y(\Phi(x - y) - G(x, y)) = \delta_x - \delta_x = 0$ distributionally on $\Omega$.

theorem LaplacePoisson.green_function_decomposition {n : ℕ} {Ω : Set (Fin n → ℝ)} (hn : n ≥ 2) (gf : GreenFunctionLP n Ω) : ∃ (corrector : (Fin n → ℝ) → (Fin n → ℝ) → ℝ), (∀ x ∈ Ω, ∀ σ ∈ frontier Ω, corrector x σ = fundamentalSolution n (x - σ)) ∧ (∀ x ∈ Ω, IsHarmonicLP (corrector x) Ω) ∧ ∀ (x y : Fin n → ℝ), gf.G x y = fundamentalSolution n (x - y) - corrector x y

Classical Green-function decomposition: $G(x, y) = \Phi(x - y) - h(x, y)$, where $h(x, \cdot)$ is harmonic on $\Omega$ and matches $\Phi(x - \cdot)$ on the boundary $\partial\Omega$.

theorem LaplacePoisson.surfaceMeasure_ball_sphere_finite {n : ℕ} (x : Fin n → ℝ) (ε : ℝ) (hε : 0 < ε) : (surfaceMeasure (Metric.ball x ε)) (Metric.sphere x ε) < ⊤

Finiteness of the surface measure of the sphere $\partial B(x, \varepsilon)$.

theorem LaplacePoisson.surfaceMeasure_ball_sphere_real_le {n : ℕ} (x : Fin n → ℝ) (ε : ℝ) (hε : 0 < ε) : (surfaceMeasure (Metric.ball x ε)).real (Metric.sphere x ε) ≤ ↑n * unitSphereArea n * ε ^ (n - 1)

Upper bound on the surface measure of $\partial B(x, \varepsilon)$: $\le n\,\omega_n\,\varepsilon^{n-1}$.

theorem LaplacePoisson.euclidNormLP_eq_dist_LP {n : ℕ} (x σ : Fin n → ℝ) : euclidNormLP (x - σ) = dist x σ

The Euclidean L² norm of $x - \sigma$ coincides with the metric distance $\operatorname{dist}(x, \sigma)$.

theorem LaplacePoisson.fundamentalSolution_abs_le_on_sphere (n : ℕ) (v : Fin n → ℝ) (ε : ℝ) (hε : 0 < ε) (hv : euclidNormLP v = ε) : |fundamentalSolution n v| ≤ 1 / (unitSphereArea n * ε ^ (n - 2))

On the sphere $\{|v| = \varepsilon\}$, the fundamental solution is bounded by $1 / (\omega_n \varepsilon^{n-2})$ in absolute value.

noncomputable def LaplacePoisson.sphereIntegralLP {n : ℕ} (x : Fin n → ℝ) (ε : ℝ) (f : (Fin n → ℝ) → ℝ) : ℝ

The surface integral of $f$ over the sphere $\partial B(x, \varepsilon)$.

theorem LaplacePoisson.surfaceIntegral_integrable_LP {n : ℕ} (Ω : Set (Fin n → ℝ)) (f : (Fin n → ℝ) → ℝ) : MeasureTheory.IntegrableOn f (frontier Ω) (surfaceMeasure Ω)

Integrability axiom (used as glue): all functions are integrable against the auxiliary surface measure on $\partial \Omega$ for this development.

theorem LaplacePoisson.surfaceIntegralLP_sub {n : ℕ} (Ω : Set (Fin n → ℝ)) (f g : (Fin n → ℝ) → ℝ) : (surfaceIntegralLP Ω fun (σ : Fin n → ℝ) => f σ - g σ) = surfaceIntegralLP Ω f - surfaceIntegralLP Ω g

Linearity (subtraction) of the surface integral on $\partial\Omega$.

theorem LaplacePoisson.sphereIntegralLP_sub {n : ℕ} (x : Fin n → ℝ) (ε : ℝ) (f g : (Fin n → ℝ) → ℝ) : (sphereIntegralLP x ε fun (σ : Fin n → ℝ) => f σ - g σ) = sphereIntegralLP x ε f - sphereIntegralLP x ε g

Linearity (subtraction) of the sphere integral over $\partial B(x, \varepsilon)$.

theorem LaplacePoisson.greens_identity_on_omega_eps_combined {n : ℕ} (u : (Fin n → ℝ) → ℝ) (Ω : Set (Fin n → ℝ)) (hu : ContDiffOn ℝ 2 u (closure Ω)) (hΩ : IsOpen Ω) (hΩb : Bornology.IsBounded Ω) (x : Fin n → ℝ) (hx : x ∈ Ω) (ε : ℝ) (hε : 0 < ε) : ∫ (y : Fin n → ℝ) in Ω \ Metric.ball x ε, fundamentalSolution n (x - y) * laplacianLP u y = (surfaceIntegralLP Ω fun (σ : Fin n → ℝ) => fundamentalSolution n (x - σ) * normalDerivLP Ω u σ - u σ * normalDerivLP Ω (fun (z : Fin n → ℝ) => fundamentalSolution n (x - z)) σ) - sphereIntegralLP x ε fun (σ : Fin n → ℝ) => fundamentalSolution n (x - σ) * normalDerivLP Ω u σ - u σ * normalDerivLP Ω (fun (z : Fin n → ℝ) => fundamentalSolution n (x - z)) σ

Combined Green's identity on $\Omega \setminus B(x, \varepsilon)$: the volume integral on the punctured domain equals the surface integral over $\partial\Omega$ minus the one over the small sphere $\partial B(x, \varepsilon)$.

theorem LaplacePoisson.sphere_area_cancellation (n : ℕ) (ε : ℝ) (hε : 0 < ε) : 1 / (unitSphereArea n * ε ^ (n - 2)) * (↑n * unitSphereArea n * ε ^ (n - 1)) = ↑n * ε

Algebraic cancellation $\frac{1}{\omega_n \varepsilon^{n-2}} \cdot (n \omega_n \varepsilon^{n-1}) = n \varepsilon$.

theorem LaplacePoisson.sphereIntegralLP_phi_bound {n : ℕ} (x : Fin n → ℝ) (ε : ℝ) (hε : 0 < ε) (g : (Fin n → ℝ) → ℝ) (M : ℝ) (hM : 0 ≤ M) (hg_bound : ∀ (σ : Fin n → ℝ), euclidNormLP (x - σ) = ε → |g σ| ≤ M) : ‖sphereIntegralLP x ε fun (σ : Fin n → ℝ) => fundamentalSolution n (x - σ) * g σ‖ ≤ ↑n * M * ε

Bound on the sphere integral of $\Phi(x - \sigma)\,g(\sigma)$: $\le n\,M\,\varepsilon$ when $|g| \le M$ on the sphere.

theorem LaplacePoisson.normalDerivLP_globally_bounded {n : ℕ} (u : (Fin n → ℝ) → ℝ) (Ω : Set (Fin n → ℝ)) (hu : ContDiffOn ℝ 2 u (closure Ω)) (hΩb : Bornology.IsBounded Ω) (x : Fin n → ℝ) (hx : x ∈ Ω) : ∃ (M : ℝ), 0 ≤ M ∧ ∀ (σ : Fin n → ℝ), |normalDerivLP Ω u σ| ≤ M

Uniform bound on the normal derivative $\partial_\nu u$ over all of $\mathbb{R}^n$: $|\partial_\nu u| \le n \cdot C$ where $C$ bounds $\|\nabla u\|$ on $\overline{\Omega}$.

theorem LaplacePoisson.greens_identity_on_omega_eps_LP {n : ℕ} (u : (Fin n → ℝ) → ℝ) (Ω : Set (Fin n → ℝ)) (hu : ContDiffOn ℝ 2 u (closure Ω)) (hΩ : IsOpen Ω) (hΩb : Bornology.IsBounded Ω) (x : Fin n → ℝ) (hx : x ∈ Ω) (ε : ℝ) (hε : 0 < ε) : ∫ (y : Fin n → ℝ) in Ω \ Metric.ball x ε, fundamentalSolution n (x - y) * laplacianLP u y = (((surfaceIntegralLP Ω fun (σ : Fin n → ℝ) => fundamentalSolution n (x - σ) * normalDerivLP Ω u σ) - surfaceIntegralLP Ω fun (σ : Fin n → ℝ) => u σ * normalDerivLP Ω (fun (z : Fin n → ℝ) => fundamentalSolution n (x - z)) σ) - sphereIntegralLP x ε fun (σ : Fin n → ℝ) => fundamentalSolution n (x - σ) * normalDerivLP Ω u σ) + sphereIntegralLP x ε fun (σ : Fin n → ℝ) => u σ * normalDerivLP Ω (fun (z : Fin n → ℝ) => fundamentalSolution n (x - z)) σ

Expanded form of Green's identity on $\Omega \setminus B(x, \varepsilon)$, splitting each surface integral into its $\Phi \partial_\nu u$ and $u \partial_\nu \Phi$ pieces.

theorem LaplacePoisson.volume_integral_limit_LP {n : ℕ} (u : (Fin n → ℝ) → ℝ) (Ω : Set (Fin n → ℝ)) (hu : ContDiffOn ℝ 2 u (closure Ω)) (hΩ : IsOpen Ω) (x : Fin n → ℝ) (hx : x ∈ Ω) : Filter.Tendsto (fun (ε : ℝ) => ∫ (y : Fin n → ℝ) in Ω \ Metric.ball x ε, fundamentalSolution n (x - y) * laplacianLP u y) (nhdsWithin 0 (Set.Ioi 0)) (nhds (∫ (y : Fin n → ℝ) in Ω, fundamentalSolution n (x - y) * laplacianLP u y))

Convergence of the volume integral over $\Omega \setminus B(x, \varepsilon)$ to the integral over $\Omega$ as $\varepsilon \to 0^+$ (since $B(x, \varepsilon)$ has vanishing volume).

theorem LaplacePoisson.sphere_integral_R3_bound_LP {n : ℕ} (u : (Fin n → ℝ) → ℝ) (Ω : Set (Fin n → ℝ)) (hu : ContDiffOn ℝ 2 u (closure Ω)) (hΩb : Bornology.IsBounded Ω) (x : Fin n → ℝ) (hx : x ∈ Ω) : ∃ (C : ℝ), ∀ (ε : ℝ), 0 < ε → ‖sphereIntegralLP x ε fun (σ : Fin n → ℝ) => fundamentalSolution n (x - σ) * normalDerivLP Ω u σ‖ ≤ C * ε

Bound on the "$R_3$" sphere integral $\int_{\partial B(x,\varepsilon)} \Phi(x - \sigma)\,\partial_\nu u(\sigma)\,dS \le C\,\varepsilon$.

theorem LaplacePoisson.sphereIntegralLP_add {n : ℕ} (x : Fin n → ℝ) (ε : ℝ) (f g : (Fin n → ℝ) → ℝ) : (sphereIntegralLP x ε fun (σ : Fin n → ℝ) => f σ + g σ) = sphereIntegralLP x ε f + sphereIntegralLP x ε g

Linearity (addition) of the sphere integral.

theorem LaplacePoisson.sphereIntegralLP_const_mul {n : ℕ} (x : Fin n → ℝ) (ε c : ℝ) (f : (Fin n → ℝ) → ℝ) : (sphereIntegralLP x ε fun (σ : Fin n → ℝ) => c * f σ) = c * sphereIntegralLP x ε f

Scalar homogeneity of the sphere integral.

theorem LaplacePoisson.sphereIntegralLP_congr_on_sphere {n : ℕ} (x : Fin n → ℝ) (ε : ℝ) (f g : (Fin n → ℝ) → ℝ) (h : ∀ σ ∈ Metric.sphere x ε, f σ = g σ) : sphereIntegralLP x ε f = sphereIntegralLP x ε g

Pointwise congruence: if $f = g$ on the sphere $\partial B(x, \varepsilon)$, then their sphere integrals agree.

theorem LaplacePoisson.normalDerivLP_Phi_on_sphere_eq {n : ℕ} (Ω : Set (Fin n → ℝ)) (x σ : Fin n → ℝ) (ε : ℝ) (hε : 0 < ε) (hσ : σ ∈ Metric.sphere x ε) : normalDerivLP Ω (fun (z : Fin n → ℝ) => fundamentalSolution n (x - z)) σ = 1 / (unitSphereArea n * ε ^ (n - 1))

Explicit pointwise value of the normal derivative of $\Phi(x - \cdot)$ on the sphere $\partial B(x, \varepsilon)$: $\partial_\nu \Phi = 1/(\omega_n \varepsilon^{n-1})$.

theorem LaplacePoisson.sphereIntegralLP_one_eq {n : ℕ} (x : Fin n → ℝ) (ε : ℝ) (hε : 0 < ε) : (sphereIntegralLP x ε fun (x : Fin n → ℝ) => 1) = unitSphereArea n * ε ^ (n - 1)

The total surface area of the sphere $\partial B(x, \varepsilon)$ is $\omega_n \varepsilon^{n-1}$.

theorem LaplacePoisson.normalDerivLP_Phi_const_on_sphere {n : ℕ} (Ω : Set (Fin n → ℝ)) (x : Fin n → ℝ) (ε : ℝ) (hε : 0 < ε) : ∃ (c : ℝ), 0 < c ∧ (∀ σ ∈ Metric.sphere x ε, normalDerivLP Ω (fun (z : Fin n → ℝ) => fundamentalSolution n (x - z)) σ = c) ∧ (c * sphereIntegralLP x ε fun (x : Fin n → ℝ) => 1) = 1

Packaged form: the normal derivative of $\Phi(x - \cdot)$ takes a constant value $c = 1/(\omega_n \varepsilon^{n-1}) > 0$ on the sphere $\partial B(x, \varepsilon)$, and $c$ times the area of the sphere equals $1$.

theorem LaplacePoisson.sphereIntegralLP_weighted_bound {n : ℕ} (x : Fin n → ℝ) (ε : ℝ) (hε : 0 < ε) (f g : (Fin n → ℝ) → ℝ) (hg_nn : ∀ σ ∈ Metric.sphere x ε, 0 ≤ g σ) (A : ℝ) (hA : sphereIntegralLP x ε g = A) : ‖sphereIntegralLP x ε fun (σ : Fin n → ℝ) => f σ * g σ‖ ≤ (⨆ σ ∈ Metric.sphere x ε, |f σ|) * A

Weighted bound: if $g \ge 0$ on the sphere and $\int g\,dS = A$, then $\bigl|\int f g\,dS\bigr| \le (\sup |f|) \cdot A$.

theorem LaplacePoisson.sphereIntegralLP_normalDeriv_Phi_eq_one {n : ℕ} (Ω : Set (Fin n → ℝ)) (x : Fin n → ℝ) (ε : ℝ) (hε : 0 < ε) : (sphereIntegralLP x ε fun (σ : Fin n → ℝ) => normalDerivLP Ω (fun (z : Fin n → ℝ) => fundamentalSolution n (x - z)) σ) = 1

Normalisation: $\int_{\partial B(x, \varepsilon)} \partial_\nu \Phi(x-\sigma)\, dS = 1$. This is the analogue of the $-1$ normalisation at the origin, used in the sphere version of the representation formula.

theorem LaplacePoisson.sphereIntegralLP_error_bound {n : ℕ} (u : (Fin n → ℝ) → ℝ) (Ω : Set (Fin n → ℝ)) (x : Fin n → ℝ) (ε : ℝ) (hε : 0 < ε) : ‖sphereIntegralLP x ε fun (σ : Fin n → ℝ) => (u σ - u x) * normalDerivLP Ω (fun (z : Fin n → ℝ) => fundamentalSolution n (x - z)) σ‖ ≤ ⨆ σ ∈ Metric.sphere x ε, |u σ - u x|

Error bound: the sphere integral of $(u - u(x))\,\partial_\nu \Phi$ is bounded by the oscillation $\sup |u - u(x)|$ on the sphere.

theorem LaplacePoisson.oscillation_sphere_tendsto_zero {n : ℕ} (u : (Fin n → ℝ) → ℝ) (Ω : Set (Fin n → ℝ)) (hu : ContDiffOn ℝ 2 u (closure Ω)) (hΩ : IsOpen Ω) (x : Fin n → ℝ) (hx : x ∈ Ω) : Filter.Tendsto (fun (ε : ℝ) => ⨆ σ ∈ Metric.sphere x ε, |u σ - u x|) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

Continuity at $x$ implies that $\sup_{\sigma \in \partial B(x,\varepsilon)} |u(\sigma) - u(x)| \to 0$ as $\varepsilon \to 0^+$.

theorem LaplacePoisson.sphere_integral_R4_decomposition_LP {n : ℕ} (u : (Fin n → ℝ) → ℝ) (Ω : Set (Fin n → ℝ)) (hu : ContDiffOn ℝ 2 u (closure Ω)) (hΩ : IsOpen Ω) (x : Fin n → ℝ) (hx : x ∈ Ω) : ∃ (error : ℝ → ℝ), (∀ ε > 0, (sphereIntegralLP x ε fun (σ : Fin n → ℝ) => u σ * normalDerivLP Ω (fun (z : Fin n → ℝ) => fundamentalSolution n (x - z)) σ) = u x + error ε) ∧ Filter.Tendsto error (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

Decomposition of the "$R_4$" sphere integral: $\int_{\partial B(x,\varepsilon)} u\,\partial_\nu \Phi\,dS = u(x) + \text{error}(\varepsilon)$, with $\text{error}(\varepsilon) \to 0$ as $\varepsilon \to 0^+$.

theorem LaplacePoisson.sphere_integral_R3_vanishes_LP {n : ℕ} (u : (Fin n → ℝ) → ℝ) (Ω : Set (Fin n → ℝ)) (hu : ContDiffOn ℝ 2 u (closure Ω)) (hΩb : Bornology.IsBounded Ω) (x : Fin n → ℝ) (hx : x ∈ Ω) : Filter.Tendsto (fun (ε : ℝ) => sphereIntegralLP x ε fun (σ : Fin n → ℝ) => fundamentalSolution n (x - σ) * normalDerivLP Ω u σ) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

The "$R_3$" sphere integral $\int_{\partial B(x,\varepsilon)} \Phi(x-\sigma)\, \partial_\nu u\,dS$ vanishes as $\varepsilon \to 0^+$.

theorem LaplacePoisson.sphere_integral_R4_limit_LP {n : ℕ} (u : (Fin n → ℝ) → ℝ) (Ω : Set (Fin n → ℝ)) (hu : ContDiffOn ℝ 2 u (closure Ω)) (hΩ : IsOpen Ω) (x : Fin n → ℝ) (hx : x ∈ Ω) : Filter.Tendsto (fun (ε : ℝ) => sphereIntegralLP x ε fun (σ : Fin n → ℝ) => u σ * normalDerivLP Ω (fun (z : Fin n → ℝ) => fundamentalSolution n (x - z)) σ) (nhdsWithin 0 (Set.Ioi 0)) (nhds (u x))

The "$R_4$" sphere integral $\int_{\partial B(x,\varepsilon)} u\,\partial_\nu \Phi(x-\cdot)\,dS$ converges to $u(x)$ as $\varepsilon \to 0^+$.

theorem LaplacePoisson.representation_formula_u_aux {n : ℕ} (u : (Fin n → ℝ) → ℝ) (Ω : Set (Fin n → ℝ)) (hu : ContDiffOn ℝ 2 u (closure Ω)) (hΩ : IsOpen Ω) (hΩb : Bornology.IsBounded Ω) (x : Fin n → ℝ) (hx : x ∈ Ω) : u x = ((∫ (y : Fin n → ℝ) in Ω, fundamentalSolution n (x - y) * laplacianLP u y) - surfaceIntegralLP Ω fun (σ : Fin n → ℝ) => fundamentalSolution n (x - σ) * normalDerivLP Ω u σ) + surfaceIntegralLP Ω fun (σ : Fin n → ℝ) => u σ * normalDerivLP Ω (fun (z : Fin n → ℝ) => fundamentalSolution n (x - z)) σ

Auxiliary form of the Green-Phi representation formula: $u(x) = (\Phi * \Delta u) - \int_{\partial\Omega} \Phi\,\partial_\nu u + \int_{\partial\Omega} u\,\partial_\nu \Phi$. Proved by passing to the limit in Green's identity on $\Omega \setminus B(x, \varepsilon)$.

theorem LaplacePoisson.representation_formula_u {n : ℕ} (u : (Fin n → ℝ) → ℝ) (Ω : Set (Fin n → ℝ)) (hu : ContDiffOn ℝ 2 u (closure Ω)) (hΩ : IsOpen Ω) (hΩb : Bornology.IsBounded Ω) (x : Fin n → ℝ) (hx : x ∈ Ω) : u x = ((∫ (y : Fin n → ℝ) in Ω, fundamentalSolution n (x - y) * laplacianLP u y) - surfaceIntegralLP Ω fun (σ : Fin n → ℝ) => fundamentalSolution n (x - σ) * normalDerivLP Ω u σ) + surfaceIntegralLP Ω fun (σ : Fin n → ℝ) => u σ * normalDerivLP Ω (fun (z : Fin n → ℝ) => fundamentalSolution n (x - z)) σ

Green's representation formula (with $\Phi$): for any $C^2$ function $u$ on $\overline{\Omega}$ and $x \in \Omega$, $u(x) = \int_\Omega \Phi(x - y),\Delta u(y),dy

• \int_{\partial\Omega} \Phi(x - \sigma),\partial_\nu u(\sigma),dS

• \int_{\partial\Omega} u(\sigma),\partial_\nu \Phi(x - \sigma),dS$.

theorem LaplacePoisson.pde_solution_smooth {n : ℕ} (Ω : Set (Fin n → ℝ)) (u f : (Fin n → ℝ) → ℝ) (hΩ : IsOpen Ω) (hΩb : Bornology.IsBounded Ω) (hu_pde : ∀ x ∈ Ω, laplacianLP u x = f x) : ContDiffOn ℝ 2 u (closure Ω)

A solution of $\Delta u = f$ on $\Omega$ is automatically $C^2$ up to the boundary, given enough regularity of $f$ and $\partial\Omega$ (axiom).

theorem LaplacePoisson.corrector_smooth {n : ℕ} (Ω : Set (Fin n → ℝ)) (gf : GreenFunctionLP n Ω) (hΩ : IsOpen Ω) (hΩb : Bornology.IsBounded Ω) (x : Fin n → ℝ) (hx : x ∈ Ω) : ContDiffOn ℝ 2 (fun (y : Fin n → ℝ) => fundamentalSolution n (x - y) - gf.G x y) (closure Ω)

Smoothness of the Green corrector $h(y) = \Phi(x - y) - G(x, y)$ up to $\overline{\Omega}$.

theorem LaplacePoisson.surface_integrand_integrableOn {n : ℕ} (Ω : Set (Fin n → ℝ)) (h₁ h₂ : (Fin n → ℝ) → ℝ) (hΩ : IsOpen Ω) (hΩb : Bornology.IsBounded Ω) : MeasureTheory.IntegrableOn (fun (σ : Fin n → ℝ) => h₁ σ * h₂ σ) (frontier Ω) (surfaceMeasure Ω)

Products of bounded measurable functions are integrable on $\partial\Omega$ (axiom used as glue).

theorem LaplacePoisson.green_identity_corrector {n : ℕ} (hn : n ≥ 2) (Ω : Set (Fin n → ℝ)) (gf : GreenFunctionLP n Ω) (u f g : (Fin n → ℝ) → ℝ) (hΩ : IsOpen Ω) (hΩb : Bornology.IsBounded Ω) (hu_pde : ∀ x ∈ Ω, laplacianLP u x = f x) (hu_bdy : ∀ σ ∈ frontier Ω, u σ = g σ) (x : Fin n → ℝ) (hx : x ∈ Ω) : have Φ := fun (y : Fin n → ℝ) => fundamentalSolution n (x - y); have φ := fun (y : Fin n → ℝ) => Φ y - gf.G x y; 0 = ((∫ (y : Fin n → ℝ) in Ω, φ y * f y) - surfaceIntegralLP Ω fun (σ : Fin n → ℝ) => Φ σ * normalDerivLP Ω u σ) + surfaceIntegralLP Ω fun (σ : Fin n → ℝ) => g σ * normalDerivLP Ω φ σ

Apply Green's second identity to the harmonic corrector $\varphi = \Phi - G$: the resulting identity expresses how the corrector "absorbs" the singular part of $\Phi$, leaving a clean integral identity used to derive Green's representation formula in terms of $G$.

theorem LaplacePoisson.adapted_representation_formula {n : ℕ} (Ω : Set (Fin n → ℝ)) (gf : GreenFunctionLP n Ω) (u f g : (Fin n → ℝ) → ℝ) (hΩ : IsOpen Ω) (hΩb : Bornology.IsBounded Ω) (hu_pde : ∀ x ∈ Ω, laplacianLP u x = f x) (hu_bdy : ∀ σ ∈ frontier Ω, u σ = g σ) (x : Fin n → ℝ) (hx : x ∈ Ω) : have Φ := fun (y : Fin n → ℝ) => fundamentalSolution n (x - y); u x = ((∫ (y : Fin n → ℝ) in Ω, Φ y * f y) - surfaceIntegralLP Ω fun (σ : Fin n → ℝ) => Φ σ * normalDerivLP Ω u σ) + surfaceIntegralLP Ω fun (σ : Fin n → ℝ) => g σ * normalDerivLP Ω Φ σ

Adapted form of the representation formula in which the volume integral uses $f = \Delta u$ and the boundary value uses $g = u|_{\partial \Omega}$.

theorem LaplacePoisson.volume_integral_combination {n : ℕ} (Ω : Set (Fin n → ℝ)) (gf : GreenFunctionLP n Ω) (f : (Fin n → ℝ) → ℝ) (x : Fin n → ℝ) (hΦf : MeasureTheory.IntegrableOn (fun (y : Fin n → ℝ) => fundamentalSolution n (x - y) * f y) Ω MeasureTheory.volume) (hGf : MeasureTheory.IntegrableOn (fun (y : Fin n → ℝ) => gf.G x y * f y) Ω MeasureTheory.volume) : have Φ := fun (y : Fin n → ℝ) => fundamentalSolution n (x - y); have φ := fun (y : Fin n → ℝ) => Φ y - gf.G x y; (-∫ (y : Fin n → ℝ) in Ω, Φ y * f y) + ∫ (y : Fin n → ℝ) in Ω, φ y * f y = -∫ (y : Fin n → ℝ) in Ω, f y * gf.G x y

Volume integral combination: $-\int \Phi f + \int (\Phi - G) f = -\int f G$, by linearity.

theorem LaplacePoisson.surface_integral_combination {n : ℕ} (Ω : Set (Fin n → ℝ)) (gf : GreenFunctionLP n Ω) (g : (Fin n → ℝ) → ℝ) (x : Fin n → ℝ) (hΦ_diff : ∀ (σ : Fin n → ℝ), DifferentiableAt ℝ (fun (y : Fin n → ℝ) => fundamentalSolution n (x - y)) σ) (hG_diff : ∀ (σ : Fin n → ℝ), DifferentiableAt ℝ (fun (z : Fin n → ℝ) => gf.G x z) σ) (h1_int : MeasureTheory.IntegrableOn (fun (σ : Fin n → ℝ) => g σ * normalDerivLP Ω (fun (y : Fin n → ℝ) => fundamentalSolution n (x - y)) σ) (frontier Ω) (surfaceMeasure Ω)) (h2_int : MeasureTheory.IntegrableOn (fun (σ : Fin n → ℝ) => g σ * normalDerivLP Ω (fun (z : Fin n → ℝ) => gf.G x z) σ) (frontier Ω) (surfaceMeasure Ω)) : have Φ := fun (y : Fin n → ℝ) => fundamentalSolution n (x - y); have φ := fun (y : Fin n → ℝ) => Φ y - gf.G x y; ((-surfaceIntegralLP Ω fun (σ : Fin n → ℝ) => g σ * normalDerivLP Ω Φ σ) + surfaceIntegralLP Ω fun (σ : Fin n → ℝ) => g σ * normalDerivLP Ω φ σ) = -surfaceIntegralLP Ω fun (σ : Fin n → ℝ) => g σ * normalDerivLP Ω (fun (z : Fin n → ℝ) => gf.G x z) σ

Surface integral combination: the analogue of volume_integral_combination but for boundary integrals of $g\,\partial_\nu \cdot$, using linearity of the normal derivative on $\Phi - G$.

theorem LaplacePoisson.green_representation_from_corrector {n : ℕ} (hn : n ≥ 2) (Ω : Set (Fin n → ℝ)) (gf : GreenFunctionLP n Ω) (u f g : (Fin n → ℝ) → ℝ) (hΩ : IsOpen Ω) (hΩb : Bornology.IsBounded Ω) (hu_pde : ∀ x ∈ Ω, laplacianLP u x = f x) (hu_bdy : ∀ σ ∈ frontier Ω, u σ = g σ) (x : Fin n → ℝ) (hx : x ∈ Ω) (hΦ_diff : ∀ (σ : Fin n → ℝ), DifferentiableAt ℝ (fun (y : Fin n → ℝ) => fundamentalSolution n (x - y)) σ) (hG_diff : ∀ (σ : Fin n → ℝ), DifferentiableAt ℝ (fun (z : Fin n → ℝ) => gf.G x z) σ) (h1_int : MeasureTheory.IntegrableOn (fun (σ : Fin n → ℝ) => g σ * normalDerivLP Ω (fun (y : Fin n → ℝ) => fundamentalSolution n (x - y)) σ) (frontier Ω) (surfaceMeasure Ω)) (h2_int : MeasureTheory.IntegrableOn (fun (σ : Fin n → ℝ) => g σ * normalDerivLP Ω (fun (z : Fin n → ℝ) => gf.G x z) σ) (frontier Ω) (surfaceMeasure Ω)) (hΦf_int : MeasureTheory.IntegrableOn (fun (y : Fin n → ℝ) => fundamentalSolution n (x - y) * f y) Ω MeasureTheory.volume) (hGf_int : MeasureTheory.IntegrableOn (fun (y : Fin n → ℝ) => gf.G x y * f y) Ω MeasureTheory.volume) : u x = (∫ (y : Fin n → ℝ) in Ω, f y * gf.G x y) + surfaceIntegralLP Ω fun (σ : Fin n → ℝ) => g σ * normalDerivLP Ω (fun (z : Fin n → ℝ) => gf.G x z) σ

Green's representation formula derived from the corrector identity: combining the $\Phi$-version of the representation formula with the harmonic-corrector identity $\varphi = \Phi - G$ yields the clean Green-function formula $u(x) = \int_\Omega f \cdot G(x, \cdot) + \int_{\partial \Omega} g \cdot \partial_\nu G(x, \cdot)$.

theorem LaplacePoisson.green_representation_formula {n : ℕ} (hn : n ≥ 2) (Ω : Set (Fin n → ℝ)) (gf : GreenFunctionLP n Ω) (u f g : (Fin n → ℝ) → ℝ) (hΩ : IsOpen Ω) (hΩb : Bornology.IsBounded Ω) (hu_pde : ∀ x ∈ Ω, laplacianLP u x = f x) (hu_bdy : ∀ σ ∈ frontier Ω, u σ = g σ) (x : Fin n → ℝ) (hx : x ∈ Ω) : u x = (∫ (y : Fin n → ℝ) in Ω, f y * gf.G x y) + surfaceIntegralLP Ω fun (σ : Fin n → ℝ) => g σ * normalDerivLP Ω (fun (z : Fin n → ℝ) => gf.G x z) σ

Green's representation formula for the Dirichlet problem $\Delta u = f$ in $\Omega$ with $u = g$ on $\partial\Omega$: $u(x) = \int_\Omega f(y)\,G(x, y)\,dy + \int_{\partial\Omega} g(\sigma)\, \partial_\nu G(x, \sigma)\,dS$.

noncomputable def LaplacePoisson.laplacianE {n : ℕ} (f : EuclideanSpace ℝ (Fin n) → ℝ) (x : EuclideanSpace ℝ (Fin n)) : ℝ

Laplacian on EuclideanSpace ℝ (Fin n) (i.e.\ Mathlib's L²-normed $\mathbb{R}^n$). Defined as $\Delta f(x) = \sum_i \partial_{x_i}^2 f(x)$ using standard basis vectors.

def LaplacePoisson.IsHarmonicE {n : ℕ} (u : EuclideanSpace ℝ (Fin n) → ℝ) (Ω : Set (EuclideanSpace ℝ (Fin n))) : Prop

A function $u$ on EuclideanSpace ℝ (Fin n) is harmonic on $\Omega$ iff $\Delta u = 0$ on $\Omega$.

opaque LaplacePoisson.outwardUnitNormalE {n : ℕ} (Ω : Set (EuclideanSpace ℝ (Fin n))) : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n)

Opaque outward unit normal on $\partial\Omega$, valued in EuclideanSpace ℝ (Fin n).

theorem LaplacePoisson.outwardUnitNormalE_ball_spec (R : ℝ) (hR : 0 < R) (p σ : EuclideanSpace ℝ (Fin 3)) (hσ : σ ∈ Metric.sphere p R) : (outwardUnitNormalE (Metric.ball p R) σ).ofLp = fun (i : Fin 3) => (σ.ofLp i - p.ofLp i) / R

Explicit form of the outward unit normal on a ball in $\mathbb{R}^3$: $\nu(\sigma) = (\sigma - p)/R$ for $\sigma$ on the sphere of radius $R$ about $p$.

opaque LaplacePoisson.surfaceMeasureE {n : ℕ} (Ω : Set (EuclideanSpace ℝ (Fin n))) : MeasureTheory.Measure (EuclideanSpace ℝ (Fin n))

Opaque surface (Hausdorff) measure on $\partial\Omega \subseteq$ EuclideanSpace ℝ (Fin n).

noncomputable def LaplacePoisson.normalDerivE {n : ℕ} (Ω : Set (EuclideanSpace ℝ (Fin n))) (f : EuclideanSpace ℝ (Fin n) → ℝ) (σ : EuclideanSpace ℝ (Fin n)) : ℝ

Normal derivative $\partial_\nu f$ at $\sigma \in \partial\Omega$ on EuclideanSpace, defined as $\sum_i (\partial_i f)(\sigma) \cdot \nu_i(\sigma)$.

noncomputable def LaplacePoisson.surfaceIntegralE {n : ℕ} (Ω : Set (EuclideanSpace ℝ (Fin n))) (f : EuclideanSpace ℝ (Fin n) → ℝ) : ℝ

Surface integral $\int_{\partial \Omega} f\,dS$ on EuclideanSpace.

structure LaplacePoisson.GreenFunctionE (n : ℕ) (Ω : Set (EuclideanSpace ℝ (Fin n))) : Type

Bundled Green's function for the Dirichlet Laplacian on $\Omega \subseteq$ EuclideanSpace ℝ (Fin n). Same defining properties as GreenFunctionLP but on the Euclidean (rather than $L^p$) model of $\mathbb{R}^n$.

• G : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n) → ℝ
• domain_open : IsOpen Ω
• boundary_zero (x : EuclideanSpace ℝ (Fin n)) : x ∈ Ω → ∀ σ ∈ frontier Ω, self.G x σ = 0
• distributional_pde (x : EuclideanSpace ℝ (Fin n)) : x ∈ Ω → ∀ (φ : EuclideanSpace ℝ (Fin n) → ℝ), ContDiff ℝ 2 φ → HasCompactSupport φ → tsupport φ ⊆ Ω → ∫ (y : EuclideanSpace ℝ (Fin n)), self.G x y * laplacianE φ y = φ x

theorem LaplacePoisson.euclideanSpace_norm_sq (v : EuclideanSpace ℝ (Fin 3)) : ‖v‖ ^ 2 = ∑ i : Fin 3, v.ofLp i ^ 2

Squared EuclideanSpace norm: $\|v\|^2 = \sum_i v_i^2$ in dimension $3$.

theorem LaplacePoisson.outwardUnitNormalE_ball_eq (R : ℝ) (hR : 0 < R) (p σ : EuclideanSpace ℝ (Fin 3)) (hσ : σ ∈ Metric.sphere p R) (i : Fin 3) : (outwardUnitNormalE (Metric.ball p R) σ).ofLp i = (σ.ofLp i - p.ofLp i) / R

Componentwise restatement of outwardUnitNormalE_ball_spec: $\nu_i(\sigma) = (\sigma_i - p_i)/R$.

theorem LaplacePoisson.greenFunctionE_ball_unique (p : EuclideanSpace ℝ (Fin 3)) (R : ℝ) (hR : 0 < R) (gf₁ gf₂ : GreenFunctionE 3 (Metric.ball p R)) (x : EuclideanSpace ℝ (Fin 3)) (hx : x ∈ Metric.ball p R) (y : EuclideanSpace ℝ (Fin 3)) : gf₁.G x y = gf₂.G x y

Uniqueness of the Green's function on a ball in $\mathbb{R}^3$: any two $\mathtt{GreenFunctionE\ 3}$ structures on $B(p, R)$ coincide pointwise.

noncomputable def LaplacePoisson.greenBallExplicit_exists (p : EuclideanSpace ℝ (Fin 3)) (R : ℝ) (hR : 0 < R) : GreenFunctionE 3 (Metric.ball p R)

An explicit Green's function on the ball $B(p, R) \subseteq \mathbb{R}^3$, built from the classical Kelvin image construction.

theorem LaplacePoisson.fderiv_greenBallExplicit_eq (p : EuclideanSpace ℝ (Fin 3)) (R : ℝ) (hR : 0 < R) (x : EuclideanSpace ℝ (Fin 3)) (hx : x ∈ Metric.ball p R) (σ : EuclideanSpace ℝ (Fin 3)) (hσ : σ ∈ Metric.sphere p R) (i : Fin 3) : (fderiv ℝ (fun (z : EuclideanSpace ℝ (Fin 3)) => (greenBallExplicit_exists p R hR).G x z) σ) (EuclideanSpace.single i 1) = -(1 - ‖x - p‖ ^ 2 / R ^ 2) / (4 * Real.pi * ‖x - σ‖ ^ 3) * (σ.ofLp i - p.ofLp i)

Explicit componentwise formula for the boundary derivative of the explicit ball Green's function in $\mathbb{R}^3$: this is the classical Poisson-kernel weight.

theorem LaplacePoisson.fderiv_greenFunctionE_ball_spec (p : EuclideanSpace ℝ (Fin 3)) (R : ℝ) (hR : 0 < R) (gf : GreenFunctionE 3 (Metric.ball p R)) (x : EuclideanSpace ℝ (Fin 3)) (hx : x ∈ Metric.ball p R) (σ : EuclideanSpace ℝ (Fin 3)) (hσ : σ ∈ Metric.sphere p R) (i : Fin 3) : (fderiv ℝ (fun (z : EuclideanSpace ℝ (Fin 3)) => gf.G x z) σ) (EuclideanSpace.single i 1) = -(1 - ‖x - p‖ ^ 2 / R ^ 2) / (4 * Real.pi * ‖x - σ‖ ^ 3) * (σ.ofLp i - p.ofLp i)

By uniqueness, the derivative formula fderiv_greenBallExplicit_eq applies to every GreenFunctionE 3 (Metric.ball p R).

theorem LaplacePoisson.fderiv_greenFunctionE_ball_eq (p : EuclideanSpace ℝ (Fin 3)) (R : ℝ) (hR : 0 < R) (gf : GreenFunctionE 3 (Metric.ball p R)) (x : EuclideanSpace ℝ (Fin 3)) (hx : x ∈ Metric.ball p R) (σ : EuclideanSpace ℝ (Fin 3)) (hσ : σ ∈ Metric.sphere p R) (i : Fin 3) : (fderiv ℝ (fun (z : EuclideanSpace ℝ (Fin 3)) => gf.G x z) σ) (EuclideanSpace.single i 1) = -(1 - ‖x - p‖ ^ 2 / R ^ 2) / (4 * Real.pi * ‖x - σ‖ ^ 3) * (σ.ofLp i - p.ofLp i)

Equational form of fderiv_greenFunctionE_ball_spec.

theorem LaplacePoisson.dirichlet_uniquenessE {n : ℕ} (hn : 0 < n) (Ω : Set (EuclideanSpace ℝ (Fin n))) (hΩ : IsOpen Ω) (hΩc : IsConnected Ω) (hΩb : Bornology.IsBounded Ω) (u₁ u₂ f g : EuclideanSpace ℝ (Fin n) → ℝ) (hu₁_reg : ContDiffOn ℝ 2 u₁ Ω) (hu₁_cont : ContinuousOn u₁ (closure Ω)) (hu₂_reg : ContDiffOn ℝ 2 u₂ Ω) (hu₂_cont : ContinuousOn u₂ (closure Ω)) (hu₁_pde : ∀ x ∈ Ω, laplacianE u₁ x = f x) (hu₂_pde : ∀ x ∈ Ω, laplacianE u₂ x = f x) (hu₁_bdy : ∀ σ ∈ frontier Ω, u₁ σ = g σ) (hu₂_bdy : ∀ σ ∈ frontier Ω, u₂ σ = g σ) (x : EuclideanSpace ℝ (Fin n)) : x ∈ closure Ω → u₁ x = u₂ x

Dirichlet uniqueness on EuclideanSpace: transferred from the $L^p$ formulation dirichlet_uniqueness via the EuclideanSpace.equiv linear isometry.

theorem LaplacePoisson.fundamental_solution_distributional_delta_E (x : EuclideanSpace ℝ (Fin 3)) (φ : EuclideanSpace ℝ (Fin 3) → ℝ) (hφ : ContDiff ℝ 2 φ) (hφs : HasCompactSupport φ) : ∫ (y : EuclideanSpace ℝ (Fin 3)), -1 / (4 * Real.pi * ‖y - x‖) * laplacianE φ y = φ x

$\Delta \Phi = \delta_x$ distributionally on EuclideanSpace ℝ (Fin 3): for any $C^2$ test function $\varphi$ with compact support, $\int -1/(4\pi |y - x|)\,\Delta \varphi(y)\,dy = \varphi(x)$.

noncomputable def LaplacePoisson.kelvinImageE (p : EuclideanSpace ℝ (Fin 3)) (R : ℝ) (x : EuclideanSpace ℝ (Fin 3)) : EuclideanSpace ℝ (Fin 3)

Kelvin image of $x$ with respect to the sphere $\partial B(p, R)$ in $\mathbb{R}^3$: $x^* = p + (R/\|x - p\|)^2 (x - p)$.

theorem LaplacePoisson.kelvinImageE_not_in_ball (p : EuclideanSpace ℝ (Fin 3)) (R : ℝ) (hR : 0 < R) (x : EuclideanSpace ℝ (Fin 3)) (hx : x ∈ Metric.ball p R) (hxp : x ≠ p) : kelvinImageE p R x ∉ Metric.ball p R

The Kelvin image of an interior point $x \ne p$ of $B(p, R)$ lies outside the ball, which is the property that makes the Kelvin image useful for constructing Green's functions on the ball.

theorem LaplacePoisson.kelvinImageE_norm_identity (p : EuclideanSpace ℝ (Fin 3)) (R : ℝ) (hR : 0 < R) (x : EuclideanSpace ℝ (Fin 3)) (hx : x ∈ Metric.ball p R) (hxp : x ≠ p) (σ : EuclideanSpace ℝ (Fin 3)) (hσ : σ ∈ Metric.sphere p R) : ‖kelvinImageE p R x - σ‖ = R / ‖x - p‖ * ‖x - σ‖

Key Kelvin-image identity: for $\sigma$ on the sphere $\partial B(p, R)$, $\|x^* - \sigma\| = (R/\|x - p\|)\,\|x - \sigma\|$. This produces the boundary cancellation of $G$ on $\partial B(p, R)$.

noncomputable def LaplacePoisson.greenBallFunctionE (p : EuclideanSpace ℝ (Fin 3)) (R : ℝ) (x y : EuclideanSpace ℝ (Fin 3)) : ℝ

Explicit Green's function on the ball $B(p, R) \subseteq \mathbb{R}^3$ constructed by the Kelvin-image method: $G(x, y) = -\frac{1}{4\pi|y-x|}

• \frac{R/|x-p|}{4\pi|y - x^|}$, where $x^$ is the Kelvin image of $x$. The center case $x = p$ is handled separately.

theorem LaplacePoisson.greenBallFunctionE_boundary_zero (p : EuclideanSpace ℝ (Fin 3)) (R : ℝ) (hR : 0 < R) (x : EuclideanSpace ℝ (Fin 3)) (hx : x ∈ Metric.ball p R) (σ : EuclideanSpace ℝ (Fin 3)) (hσ : σ ∈ frontier (Metric.ball p R)) : greenBallFunctionE p R x σ = 0

Boundary vanishing of the explicit Green's function on the ball: for every $x \in B(p, R)$ and every $\sigma \in \partial B(p, R)$, $G(x, \sigma) = 0$. This relies on the Kelvin-image norm identity to balance the two terms.

theorem LaplacePoisson.integral_laplacianE_compactSupport_eq_zero (φ : EuclideanSpace ℝ (Fin 3) → ℝ) (hφ : ContDiff ℝ 2 φ) (hφs : HasCompactSupport φ) : ∫ (y : EuclideanSpace ℝ (Fin 3)), laplacianE φ y = 0

The integral of the Laplacian of any compactly supported $C^2$ function on $\mathbb{R}^3$ vanishes: $\int_{\mathbb{R}^3} \Delta \varphi = 0$. This follows from the divergence theorem applied to a large ball containing $\operatorname{supp} \varphi$.

theorem LaplacePoisson.integrable_fundamentalSol_mul_laplacianE (x : EuclideanSpace ℝ (Fin 3)) (φ : EuclideanSpace ℝ (Fin 3) → ℝ) (hφ : ContDiff ℝ 2 φ) (hφs : HasCompactSupport φ) : MeasureTheory.Integrable (fun (y : EuclideanSpace ℝ (Fin 3)) => -1 / (4 * Real.pi * ‖y - x‖) * laplacianE φ y) MeasureTheory.volume

Integrability of $\Phi(y - x) \, \Delta \varphi(y)$ on $\mathbb{R}^3$ when $\varphi \in C^2_c$. The product is locally integrable because $\Phi$ has only a weak $1/r$ singularity in three dimensions and $\Delta \varphi$ has compact support.

theorem LaplacePoisson.integrable_const_mul_laplacianE (c : ℝ) (φ : EuclideanSpace ℝ (Fin 3) → ℝ) (hφ : ContDiff ℝ 2 φ) (hφs : HasCompactSupport φ) : MeasureTheory.Integrable (fun (y : EuclideanSpace ℝ (Fin 3)) => c * laplacianE φ y) MeasureTheory.volume

Integrability of $c \cdot \Delta \varphi$ for any constant $c$ when $\varphi \in C^2_c$. Used to handle the constant correction term in the ball Green's function.

theorem LaplacePoisson.integrable_corrector_mul_laplacianE (p : EuclideanSpace ℝ (Fin 3)) (R : ℝ) (x : EuclideanSpace ℝ (Fin 3)) (hxp : x ≠ p) (φ : EuclideanSpace ℝ (Fin 3) → ℝ) (hφ : ContDiff ℝ 2 φ) (hφs : HasCompactSupport φ) : MeasureTheory.Integrable (fun (y : EuclideanSpace ℝ (Fin 3)) => R / ‖x - p‖ * (1 / (4 * Real.pi * ‖y - kelvinImageE p R x‖)) * laplacianE φ y) MeasureTheory.volume

Integrability of the Kelvin-image corrector term $\frac{R}{\|x-p\|} \cdot \frac{1}{4\pi \|y - x^*\|} \cdot \Delta \varphi(y)$ against a $C^2_c$ test function, used in proving the distributional PDE for the ball Green's function.

theorem LaplacePoisson.greenBallFunctionE_distributional_pde (p : EuclideanSpace ℝ (Fin 3)) (R : ℝ) (hR : 0 < R) (x : EuclideanSpace ℝ (Fin 3)) (hx : x ∈ Metric.ball p R) (φ : EuclideanSpace ℝ (Fin 3) → ℝ) (hφ : ContDiff ℝ 2 φ) (hφs : HasCompactSupport φ) (hφsupp : tsupport φ ⊆ Metric.ball p R) : ∫ (y : EuclideanSpace ℝ (Fin 3)), greenBallFunctionE p R x y * laplacianE φ y = φ x

Distributional Green's identity for the explicit ball Green's function: for any $\varphi \in C^2_c$ with $\operatorname{supp} \varphi \subseteq B(p, R)$ and $x \in B(p, R)$, $$\int_{\mathbb{R}^3} G(x, y) \, \Delta \varphi(y) \, dy = \varphi(x).$$ This expresses $\Delta_y G(x, \cdot) = \delta_x$ in the sense of distributions and uses that the Kelvin image $x^*$ lies outside $B(p, R)$.

noncomputable def LaplacePoisson.green_ball_existsE_spec (p : EuclideanSpace ℝ (Fin 3)) (R : ℝ) (hR : 0 < R) : GreenFunctionE 3 (Metric.ball p R)

Existence of the Green's function on the ball $B(p, R) \subseteq \mathbb{R}^3$, packaged as a GreenFunctionE structure built from greenBallFunctionE, greenBallFunctionE_boundary_zero, and greenBallFunctionE_distributional_pde.

noncomputable def LaplacePoisson.green_ball_existsE (p : EuclideanSpace ℝ (Fin 3)) (R : ℝ) (hR : 0 < R) : GreenFunctionE 3 (Metric.ball p R)

The Green's function on the ball $B(p, R)$, exposed as a GreenFunctionE term. This is the abstract witness consumed by the Poisson-formula proof.

theorem LaplacePoisson.greens_second_identity_representation_E {n : ℕ} (Ω : Set (EuclideanSpace ℝ (Fin n))) (gf : GreenFunctionE n Ω) (u h g : EuclideanSpace ℝ (Fin n) → ℝ) (hΩ : IsOpen Ω) (hΩb : Bornology.IsBounded Ω) (hu_pde : ∀ x ∈ Ω, laplacianE u x = h x) (hu_bdy : ∀ σ ∈ frontier Ω, u σ = g σ) (x : EuclideanSpace ℝ (Fin n)) (hx : x ∈ Ω) : ((u x + ∫ (y : EuclideanSpace ℝ (Fin n)) in Ω, h y * gf.G x y) + surfaceIntegralE Ω fun (σ : EuclideanSpace ℝ (Fin n)) => g σ * normalDerivE Ω (fun (z : EuclideanSpace ℝ (Fin n)) => gf.G x z) σ) = 0

Green's second identity applied to a Green's function gf for the bounded open domain $\Omega$: if $\Delta u = h$ in $\Omega$ and $u = g$ on $\partial \Omega$, then $$u(x) + \int_{\Omega} h(y) , G(x, y) , dy

• \int_{\partial \Omega} g(\sigma) , \partial_\nu G(x, \sigma) , dS(\sigma) = 0.$$ This is the integration-by-parts cornerstone of the representation formula.

theorem LaplacePoisson.green_representation_formulaE {n : ℕ} (Ω : Set (EuclideanSpace ℝ (Fin n))) (gf : GreenFunctionE n Ω) (u h g : EuclideanSpace ℝ (Fin n) → ℝ) (hΩ : IsOpen Ω) (hΩb : Bornology.IsBounded Ω) (hu_pde : ∀ x ∈ Ω, laplacianE u x = h x) (hu_bdy : ∀ σ ∈ frontier Ω, u σ = g σ) (x : EuclideanSpace ℝ (Fin n)) (hx : x ∈ Ω) : u x = (-∫ (y : EuclideanSpace ℝ (Fin n)) in Ω, h y * gf.G x y) - surfaceIntegralE Ω fun (σ : EuclideanSpace ℝ (Fin n)) => g σ * normalDerivE Ω (fun (z : EuclideanSpace ℝ (Fin n)) => gf.G x z) σ

Green's representation formula: a solution of the Dirichlet problem $\Delta u = h$ in $\Omega$ with $u = g$ on $\partial \Omega$ admits the explicit representation $$u(x) = -\int_{\Omega} h(y) , G(x, y) , dy

• \int_{\partial \Omega} g(\sigma) , \partial_\nu G(x, \sigma) , dS(\sigma).$$ Obtained immediately by rearranging Green's second identity.

theorem LaplacePoisson.normal_deriv_green_ball (p : EuclideanSpace ℝ (Fin 3)) (R : ℝ) (hR : 0 < R) (gf : GreenFunctionE 3 (Metric.ball p R)) (x : EuclideanSpace ℝ (Fin 3)) (hx : x ∈ Metric.ball p R) (σ : EuclideanSpace ℝ (Fin 3)) (hσ : σ ∈ Metric.sphere p R) : normalDerivE (Metric.ball p R) (fun (z : EuclideanSpace ℝ (Fin 3)) => gf.G x z) σ = -(R ^ 2 - ‖x - p‖ ^ 2) / (4 * Real.pi * R * ‖x - σ‖ ^ 3)

Explicit normal derivative of the ball Green's function on the sphere $\partial B(p, R) \subseteq \mathbb{R}^3$: $$\partial_\nu G(x, \sigma) = -\frac{R^2 - \|x - p\|^2}{4 \pi R \, \|x - \sigma\|^3}.$$ This is the Poisson kernel (up to sign) that appears in the Poisson integral formula.

theorem LaplacePoisson.poisson_formula (p : EuclideanSpace ℝ (Fin 3)) (R : ℝ) (hR : 0 < R) (f : EuclideanSpace ℝ (Fin 3) → ℝ) (_hf : ContinuousOn f (Metric.sphere p R)) (u : EuclideanSpace ℝ (Fin 3) → ℝ) (hu_reg : ContDiffOn ℝ 2 u (Metric.ball p R)) (hu_cont : ContinuousOn u (Metric.closedBall p R)) (hu_harm : IsHarmonicE u (Metric.ball p R)) (hu_bdy : ∀ σ ∈ Metric.sphere p R, u σ = f σ) (x : EuclideanSpace ℝ (Fin 3)) (hx : x ∈ Metric.ball p R) : (u x = (R ^ 2 - ‖x - p‖ ^ 2) / (4 * Real.pi * R) * surfaceIntegralE (Metric.ball p R) fun (σ : EuclideanSpace ℝ (Fin 3)) => f σ / ‖x - σ‖ ^ 3) ∧ ∀ (v : EuclideanSpace ℝ (Fin 3) → ℝ), ContDiffOn ℝ 2 v (Metric.ball p R) → ContinuousOn v (Metric.closedBall p R) → IsHarmonicE v (Metric.ball p R) → (∀ σ ∈ Metric.sphere p R, v σ = f σ) → ∀ y ∈ Metric.closedBall p R, v y = u y

Poisson integral formula on the ball $B(p, R) \subseteq \mathbb{R}^3$. If $u \in C^2(B(p, R)) \cap C(\overline{B(p, R)})$ is harmonic in $B(p, R)$ and $u = f$ on $\partial B(p, R)$, then for every $x \in B(p, R)$ $$u(x) = \frac{R^2 - \|x - p\|^2}{4 \pi R} \int_{\partial B(p, R)} \frac{f(\sigma)}{\|x - \sigma\|^3} \, dS(\sigma),$$ and $u$ is the unique such function (uniqueness from the maximum principle via dirichlet_uniquenessE). This is the explicit solution of the Dirichlet problem on the ball.