opaque CM8.IsLipschitzDomain {n : ℕ} : Set (Fin n → ℝ) → Prop

Opaque predicate: $\Omega \subset \mathbb{R}^n$ is a (bounded) Lipschitz domain. Left abstract here since regularity details of the boundary are not used in these formal statements.

noncomputable def CM8.euclidNorm {n : ℕ} (x : Fin n → ℝ) : ℝ

The Euclidean norm on $\mathbb{R}^n$ written as $\|x\| = \sqrt{\sum_i x_i^2}$.

noncomputable def CM8.Phi3 (x : Fin 3 → ℝ) : ℝ

The fundamental solution of the Laplacian in $\mathbb{R}^3$: $\Phi(x) = -\dfrac{1}{4 \pi |x|}$, away from the origin.

noncomputable def CM8.laplacian {n : ℕ} (f : (Fin n → ℝ) → ℝ) (x : Fin n → ℝ) : ℝ

The Laplacian of $f : \mathbb{R}^n \to \mathbb{R}$ at $x$, defined in terms of Fréchet derivatives applied to coordinate unit vectors: $\Delta f(x) = \sum_{i = 1}^{n} \partial_i (\partial_i f)(x)$.

noncomputable def CM8.normSq_CLM (x : Fin 3 → ℝ) : (Fin 3 → ℝ) →L[ℝ] ℝ

The continuous linear map representing the Fréchet derivative of $y \mapsto \sum_j y_j^2$ at $x$: it acts as $v \mapsto 2 \sum_j x_j v_j$.

theorem CM8.normSq_pos (x : Fin 3 → ℝ) (hx : euclidNorm x ≠ 0) : 0 < CM8.normSq✝ x

If $\|x\| \ne 0$ then $\sum_j x_j^2 > 0$.

theorem CM8.euclidNorm_pos (x : Fin 3 → ℝ) (hx : euclidNorm x ≠ 0) : 0 < euclidNorm x

If $\|x\| \ne 0$ then $\|x\| > 0$.

theorem CM8.continuous_euclidNorm3 : Continuous euclidNorm

The Euclidean norm on $\mathbb{R}^3$ is continuous.

theorem CM8.isOpen_euclidNorm_ne : IsOpen {y : Fin 3 → ℝ | euclidNorm y ≠ 0}

The complement of the origin (where $\|y\| \ne 0$) is open in $\mathbb{R}^3$.

theorem CM8.hasFDerivAt_normSq (x : Fin 3 → ℝ) : HasFDerivAt CM8.normSq✝ (normSq_CLM x) x

The map $y \mapsto \sum_j y_j^2$ has Fréchet derivative normSq_CLM x at $x$.

theorem CM8.normSq_CLM_apply (x : Fin 3 → ℝ) (i : Fin 3) : (normSq_CLM x) (Pi.single i 1) = 2 * x i

Evaluation of normSq_CLM x on the $i$-th coordinate basis vector gives $2 x_i$.

theorem CM8.hasDerivAt_g (s : ℝ) (hs : 0 < s) : HasDerivAt (fun (s : ℝ) => -1 / (4 * Real.pi * √s)) (1 / (8 * Real.pi * √s ^ 3)) s

The scalar function $g(s) = -1 / (4 \pi \sqrt{s})$ has derivative $g'(s) = 1 / (8 \pi (\sqrt{s})^3)$ for $s > 0$.

theorem CM8.hasFDerivAt_Phi3 (y : Fin 3 → ℝ) (hy : euclidNorm y ≠ 0) : HasFDerivAt Phi3 ((1 / (8 * Real.pi * euclidNorm y ^ 3)) • normSq_CLM y) y

Fréchet derivative of $\Phi_3$ on $\mathbb{R}^3 \setminus \{0\}$, obtained by the chain rule $\Phi_3(y) = g(\|y\|^2)$.

theorem CM8.fderiv_Phi3_apply (y : Fin 3 → ℝ) (hy : euclidNorm y ≠ 0) (i : Fin 3) : (fderiv ℝ Phi3 y) (Pi.single i 1) = y i / (4 * Real.pi * euclidNorm y ^ 3)

The $i$-th partial derivative of $\Phi_3$ at $y$ (with $y \ne 0$) is $\partial_i \Phi_3(y) = y_i / (4 \pi \|y\|^3)$.

theorem CM8.hasDerivAt_sqrt_cube (s : ℝ) (hs : 0 < s) : HasDerivAt (fun (s : ℝ) => √s ^ 3) (3 / 2 * √s) s

$\frac{d}{ds} (\sqrt{s})^3 = \frac{3}{2} \sqrt{s}$ for $s > 0$.

theorem CM8.hasDerivAt_inv_4pi_R3 (s : ℝ) (hs : 0 < s) : HasDerivAt (fun (s : ℝ) => (4 * Real.pi * √s ^ 3)⁻¹) (-(4 * Real.pi * (3 / 2 * √s)) / (4 * Real.pi * √s ^ 3) ^ 2) s

The derivative of $s \mapsto (4 \pi (\sqrt{s})^3)^{-1}$ at $s > 0$, computed via the chain and quotient rules.

theorem CM8.hasFDerivAt_h (y : Fin 3 → ℝ) (hy : euclidNorm y ≠ 0) : HasFDerivAt (fun (y : Fin 3 → ℝ) => (4 * Real.pi * euclidNorm y ^ 3)⁻¹) ((-(4 * Real.pi * (3 / 2 * euclidNorm y)) / (4 * Real.pi * euclidNorm y ^ 3) ^ 2) • normSq_CLM y) y

Fréchet derivative of $y \mapsto (4 \pi \|y\|^3)^{-1}$ on $\mathbb{R}^3 \setminus \{0\}$, used as a building block for partial derivatives of $\Phi_3$ itself.

theorem CM8.differentiableAt_F (x : Fin 3 → ℝ) (hx : euclidNorm x ≠ 0) (i : Fin 3) : DifferentiableAt ℝ (fun (y : Fin 3 → ℝ) => y i / (4 * Real.pi * euclidNorm y ^ 3)) x

The map $y \mapsto y_i / (4 \pi \|y\|^3)$ is differentiable at every $x \in \mathbb{R}^3$ with $\|x\| \ne 0$.

def CM8.restSq (x : Fin 3 → ℝ) (i : Fin 3) : ℝ

The sum of squares of the coordinates of $x$ other than the $i$-th: $\sum_{j \ne i} x_j^2$. Used to reduce a multivariable derivative to a one-dimensional computation.

theorem CM8.euclidNorm_update_sq (x : Fin 3 → ℝ) (i : Fin 3) (t : ℝ) : ∑ j : Fin 3, Function.update x i t j ^ 2 = t ^ 2 + restSq x i

Updating the $i$-th coordinate of $x$ to $t$ changes the squared Euclidean norm to $t^2 + \sum_{j \ne i} x_j^2$.

theorem CM8.hasDerivAt_phi_2d (t C : ℝ) (hpos : 0 < t ^ 2 + C) : HasDerivAt (fun (t : ℝ) => t / (4 * Real.pi * √(t ^ 2 + C) ^ 3)) ((C - 2 * t ^ 2) / (4 * Real.pi * √(t ^ 2 + C) ^ 5)) t

Derivative of the one-variable section $t \mapsto t / (4 \pi (\sqrt{t^2 + C})^3)$ at a point where $t^2 + C > 0$. This is the diagonal contribution to $\partial_i \partial_i \Phi_3$.

theorem CM8.Phi3_harmonic_away (x : Fin 3 → ℝ) (hx : euclidNorm x ≠ 0) : laplacian Phi3 x = 0

The fundamental solution $\Phi_3(x) = -1 / (4 \pi |x|)$ is harmonic on $\mathbb{R}^3 \setminus \{0\}$: $\Delta \Phi_3(x) = 0$ for all $x$ with $\|x\| \ne 0$.

structure CM8.GreenFunction (Ω : Set (Fin 3 → ℝ)) : Type

Definition 2.0.2 (Green function for a domain). Data of a Green function for a domain $\Omega \subset \mathbb{R}^3$: a corrector $\phi(x, y)$ which matches the fundamental solution on the boundary, i.e. $\phi(x, \sigma) = \Phi_3(x - \sigma)$ for $x \in \Omega$ and $\sigma \in \partial \Omega$.

• corrector : (Fin 3 → ℝ) → (Fin 3 → ℝ) → ℝ
• corrector_boundary (x : Fin 3 → ℝ) : x ∈ Ω → ∀ σ ∈ frontier Ω, self.corrector x σ = Phi3 (x - σ)

noncomputable def CM8.GreenFunction.G {Ω : Set (Fin 3 → ℝ)} (gf : GreenFunction Ω) (x y : Fin 3 → ℝ) : ℝ

The Green function $G(x, y) = \Phi_3(x - y) - \phi(x, y)$ assembled from a fundamental solution and its corrector.

opaque CM8.normalDerivGF (Ω : Set (Fin 3 → ℝ)) (f : (Fin 3 → ℝ) → ℝ) (σ : Fin 3 → ℝ) : ℝ

Abstract placeholder for the outward normal derivative $\nabla_{\hat{N}(\sigma)} f$ of a function $f$ at a boundary point $\sigma$ of $\Omega$.

opaque CM8.surfaceIntegralGF (Ω : Set (Fin 3 → ℝ)) (f : (Fin 3 → ℝ) → ℝ) : ℝ

Abstract placeholder for the boundary surface integral $\int_{\partial \Omega} f(\sigma) \, d\sigma$.

opaque CM8.sphereIntegralGF (x : Fin 3 → ℝ) (ε : ℝ) (f : (Fin 3 → ℝ) → ℝ) : ℝ

Abstract placeholder for the integral of $f$ over the sphere of radius $\varepsilon$ centred at $x$: $\int_{\partial B_\varepsilon(x)} f \, d\sigma$.

theorem CM8.greens_identity_on_omega_eps_GF (u : (Fin 3 → ℝ) → ℝ) (Ω : Set (Fin 3 → ℝ)) (hu : ContDiff ℝ 2 u) (hΩ : IsOpen Ω) (x : Fin 3 → ℝ) (hx : x ∈ Ω) (ε : ℝ) (hε : ε > 0) : ∫ (y : Fin 3 → ℝ) in Ω \ Metric.ball x ε, Phi3 (x - y) * laplacian u y = (((surfaceIntegralGF Ω fun (σ : Fin 3 → ℝ) => Phi3 (x - σ) * normalDerivGF Ω u σ) - surfaceIntegralGF Ω fun (σ : Fin 3 → ℝ) => u σ * normalDerivGF Ω (fun (z : Fin 3 → ℝ) => Phi3 (x - z)) σ) - sphereIntegralGF x ε fun (σ : Fin 3 → ℝ) => Phi3 (x - σ) * normalDerivGF Ω u σ) + sphereIntegralGF x ε fun (σ : Fin 3 → ℝ) => u σ * normalDerivGF Ω (fun (z : Fin 3 → ℝ) => Phi3 (x - z)) σ

Green's identity on the punctured domain $\Omega \setminus B_\varepsilon(x)$: the volume integral of $\Phi_3(x - y) \Delta u(y)$ equals a difference of boundary surface integrals minus a sphere integral around the singularity.

theorem CM8.volume_integral_limit_GF (u : (Fin 3 → ℝ) → ℝ) (Ω : Set (Fin 3 → ℝ)) (hu : ContDiff ℝ 2 u) (hΩ : IsOpen Ω) (x : Fin 3 → ℝ) (hx : x ∈ Ω) : Filter.Tendsto (fun (ε : ℝ) => ∫ (y : Fin 3 → ℝ) in Ω \ Metric.ball x ε, Phi3 (x - y) * laplacian u y) (nhdsWithin 0 (Set.Ioi 0)) (nhds (∫ (y : Fin 3 → ℝ) in Ω, Phi3 (x - y) * laplacian u y))

As $\varepsilon \to 0^+$, the volume integral $\int_{\Omega \setminus B_\varepsilon(x)} \Phi_3(x - y) \Delta u(y) \, dy$ converges to $\int_{\Omega} \Phi_3(x - y) \Delta u(y) \, dy$.

theorem CM8.sphere_integral_R3_vanishes_GF (u : (Fin 3 → ℝ) → ℝ) (Ω : Set (Fin 3 → ℝ)) (hu : ContDiff ℝ 2 u) (x : Fin 3 → ℝ) (hx : x ∈ Ω) : Filter.Tendsto (fun (ε : ℝ) => sphereIntegralGF x ε fun (σ : Fin 3 → ℝ) => Phi3 (x - σ) * normalDerivGF Ω u σ) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

The sphere integral of $\Phi_3(x - \sigma) \cdot \nabla_{\hat N} u(\sigma)$ over $\partial B_\varepsilon(x)$ vanishes in the limit $\varepsilon \to 0^+$.

theorem CM8.sphere_integral_R4_limit_GF (u : (Fin 3 → ℝ) → ℝ) (Ω : Set (Fin 3 → ℝ)) (hu : ContDiff ℝ 2 u) (x : Fin 3 → ℝ) (hx : x ∈ Ω) : Filter.Tendsto (fun (ε : ℝ) => sphereIntegralGF x ε fun (σ : Fin 3 → ℝ) => u σ * normalDerivGF Ω (fun (z : Fin 3 → ℝ) => Phi3 (x - z)) σ) (nhdsWithin 0 (Set.Ioi 0)) (nhds (u x))

The sphere integral of $u(\sigma) \cdot \nabla_{\hat N} \Phi_3(x - \sigma)$ over $\partial B_\varepsilon(x)$ converges to $u(x)$ as $\varepsilon \to 0^+$. This is where the delta-function behaviour of $\Delta \Phi_3$ contributes.

theorem CM8.representation_formula_u (u : (Fin 3 → ℝ) → ℝ) (Ω : Set (Fin 3 → ℝ)) (hu : ContDiff ℝ 2 u) (hΩ : IsOpen Ω) (x : Fin 3 → ℝ) (hx : x ∈ Ω) : u x = ((∫ (y : Fin 3 → ℝ) in Ω, Phi3 (x - y) * laplacian u y) - surfaceIntegralGF Ω fun (σ : Fin 3 → ℝ) => Phi3 (x - σ) * normalDerivGF Ω u σ) + surfaceIntegralGF Ω fun (σ : Fin 3 → ℝ) => u σ * normalDerivGF Ω (fun (z : Fin 3 → ℝ) => Phi3 (x - z)) σ

Proposition 2.0.3 (Representation formula for $u$). For any $C^2$ function $u$ on an open domain $\Omega \subset \mathbb{R}^3$ and any $x \in \Omega$, $$u(x) = \int_{\Omega} \Phi_3(x - y) \Delta u(y) , dy

• \int_{\partial \Omega} \Phi_3(x - \sigma) \nabla_{\hat N} u(\sigma) , d\sigma

• \int_{\partial \Omega} u(\sigma) \nabla_{\hat N} \Phi_3(x - \sigma) , d\sigma.$$ Proved by taking $\varepsilon \to 0$ in Green's identity.

structure CM8.IsGreenDecomposition {n : ℕ} (Ω : Set (Fin n → ℝ)) (Φ : (Fin n → ℝ) → ℝ) (G φ : (Fin n → ℝ) → (Fin n → ℝ) → ℝ) : Prop

Proposition 2.0.2 (Green decomposition). Predicate asserting that $G(x, y) = \Phi(x - y) - \phi(x, y)$ where, for each $x \in \Omega$, the corrector $\phi(x, \cdot)$ is harmonic in $\Omega$ and equals $\Phi(x - \sigma)$ on $\partial \Omega$.

• decomposition (x y : Fin n → ℝ) : G x y = Φ (x - y) - φ x y
• corrector_harmonic (x : Fin n → ℝ) : x ∈ Ω → ∀ y ∈ Ω, laplacian (φ x) y = 0
• corrector_boundary (x : Fin n → ℝ) : x ∈ Ω → ∀ σ ∈ frontier Ω, φ x σ = Φ (x - σ)

theorem CM8.laplacian_sub {n : ℕ} (f g : (Fin n → ℝ) → ℝ) (x : Fin n → ℝ) (hf : ∀ (y : Fin n → ℝ), DifferentiableAt ℝ f y) (hg : ∀ (y : Fin n → ℝ), DifferentiableAt ℝ g y) (hf2 : ∀ (i : Fin n), DifferentiableAt ℝ (fun (y : Fin n → ℝ) => (fderiv ℝ f y) (Pi.single i 1)) x) (hg2 : ∀ (i : Fin n), DifferentiableAt ℝ (fun (y : Fin n → ℝ) => (fderiv ℝ g y) (Pi.single i 1)) x) : laplacian (f - g) x = laplacian f x - laplacian g x

Linearity of the Laplacian under subtraction: $\Delta(f - g) = \Delta f - \Delta g$, provided $f, g$ are differentiable on $\mathbb{R}^n$ and each partial $\partial_i f$, $\partial_i g$ is differentiable at $x$.