structure CM7.PDEDomain (n : ℕ) : Type

A PDEDomain in $\mathbb{R}^n$ is a connected open subset, the natural setting in which to pose boundary-value problems for PDEs.

• carrier : Set (Fin n → ℝ)
• isOpen : IsOpen self.carrier
• isConnected : IsConnected self.carrier

noncomputable def CM7.Laplacian (n : ℕ) (u : (Fin n → ℝ) → ℝ) : (Fin n → ℝ) → ℝ

The Laplacian $\Delta u(x) = \sum_{i=1}^n \partial_i^2 u(x)$ of a function $u : \mathbb{R}^n \to \mathbb{R}$, defined using iterated Fréchet derivatives applied to the standard basis vectors $e_i$.

theorem CM7.laplacian_sub {n : ℕ} {u v : (Fin n → ℝ) → ℝ} {Ω : Set (Fin n → ℝ)} (hΩ : IsOpen Ω) (hu : ContDiffOn ℝ 2 u Ω) (hv : ContDiffOn ℝ 2 v Ω) {x : Fin n → ℝ} (hx : x ∈ Ω) : Laplacian n (fun (x : Fin n → ℝ) => u x - v x) x = Laplacian n u x - Laplacian n v x

Linearity of the Laplacian under subtraction: for $C^2$ functions $u, v$ on an open set $\Omega$, we have $\Delta(u - v)(x) = \Delta u(x) - \Delta v(x)$ at every $x \in \Omega$.

theorem CM7.laplacian_neg {n : ℕ} (u : (Fin n → ℝ) → ℝ) : (Laplacian n fun (x : Fin n → ℝ) => -u x) = fun (x : Fin n → ℝ) => -Laplacian n u x

The Laplacian commutes with negation: $\Delta(-u) = -\Delta u$.

theorem CM7.laplacian_const {n : ℕ} (c : ℝ) : (Laplacian n fun (x : Fin n → ℝ) => c) = fun (x : Fin n → ℝ) => 0

The Laplacian of a constant function is identically zero: $\Delta c = 0$.

structure CM7.IsHarmonic {n : ℕ} (u : (Fin n → ℝ) → ℝ) (Ω : Set (Fin n → ℝ)) : Prop

A function $u : \mathbb{R}^n \to \mathbb{R}$ is harmonic on an open set $\Omega$ if it is $C^2$ on $\Omega$ and satisfies Laplace's equation $\Delta u(x) = 0$ for all $x \in \Omega$.

• contDiffOn : ContDiffOn ℝ 2 u Ω
• laplacian_eq_zero (x : Fin n → ℝ) : x ∈ Ω → Laplacian n u x = 0

def CM7.IsPoisson {n : ℕ} (u f : (Fin n → ℝ) → ℝ) (Ω : Set (Fin n → ℝ)) : Prop

The predicate that $u$ solves Poisson's equation $\Delta u = f$ on $\Omega$, i.e. for every $x \in \Omega$, $\Delta u(x) = f(x)$.

theorem CM7.harmonic_is_contDiffOn {n : ℕ} (u : (Fin n → ℝ) → ℝ) (Ω : Set (Fin n → ℝ)) (hu : IsHarmonic u Ω) : ContDiffOn ℝ 2 u Ω

A harmonic function is $C^2$ on its domain.

theorem CM7.IsHarmonic.sub {n : ℕ} {u v : (Fin n → ℝ) → ℝ} {Ω : Set (Fin n → ℝ)} (hu : IsHarmonic u Ω) (hΩ : IsOpen Ω) (hv : IsHarmonic v Ω) : IsHarmonic (fun (x : Fin n → ℝ) => u x - v x) Ω

The difference of two harmonic functions on an open set is harmonic.

theorem CM7.IsHarmonic.neg {n : ℕ} {u : (Fin n → ℝ) → ℝ} {Ω : Set (Fin n → ℝ)} (hu : IsHarmonic u Ω) : IsHarmonic (fun (x : Fin n → ℝ) => -u x) Ω

The negation of a harmonic function is harmonic.

noncomputable def CM7.gradNormSquaredIntegral {n : ℕ} (u : (Fin n → ℝ) → ℝ) (Ω : Set (Fin n → ℝ)) : ℝ

The Dirichlet energy $\int_\Omega \|\nabla u(x)\|^2\, dx$ of $u$ on $\Omega$.

opaque CM7.outwardUnitNormal (n : ℕ) : (Fin n → ℝ) → Fin n → ℝ

The outward unit normal vector field on the boundary of a domain in $\mathbb{R}^n$. Provided abstractly as an opaque function.

opaque CM7.surfaceMeasure (n : ℕ) (Ω : Set (Fin n → ℝ)) : MeasureTheory.Measure (Fin n → ℝ)

The surface (boundary) measure on $\partial \Omega$ for a domain $\Omega \subseteq \mathbb{R}^n$, provided abstractly as an opaque measure.

noncomputable def CM7.NormalDerivative (n : ℕ) (w : (Fin n → ℝ) → ℝ) (x : Fin n → ℝ) : ℝ

The outward normal derivative $\partial_\nu w(x) = \nabla w(x) \cdot \nu(x)$ at a boundary point $x$, where $\nu$ is the outward unit normal.

noncomputable def CM7.boundaryEnergyIntegral {n : ℕ} (w : (Fin n → ℝ) → ℝ) (Ω : Set (Fin n → ℝ)) : ℝ

The boundary energy integral $\int_{\partial \Omega} w(x) \, \partial_\nu w(x) \, dS$ arising from Green's first identity.

theorem CM7.greens_first_identity {n : ℕ} (w : (Fin n → ℝ) → ℝ) (Ω : Set (Fin n → ℝ)) (hΩ : IsOpen Ω) (hΩb : Bornology.IsBounded Ω) : gradNormSquaredIntegral w Ω + ∫ (x : Fin n → ℝ) in Ω, w x * Laplacian n w x = boundaryEnergyIntegral w Ω

Green's first identity for a bounded open set $\Omega$: $\int_\Omega \|\nabla w\|^2 + \int_\Omega w \, \Delta w = \int_{\partial \Omega} w \, \partial_\nu w \, dS$.

theorem CM7.energy_identity {n : ℕ} (w : (Fin n → ℝ) → ℝ) (Ω : Set (Fin n → ℝ)) (hΩ : IsOpen Ω) (hΩb : Bornology.IsBounded Ω) : ∫ (x : Fin n → ℝ) in Ω, w x * Laplacian n w x = -gradNormSquaredIntegral w Ω + boundaryEnergyIntegral w Ω

Rearranged form of Green's first identity: $\int_\Omega w \, \Delta w = -\int_\Omega \|\nabla w\|^2 + \int_{\partial \Omega} w \, \partial_\nu w \, dS$.

theorem CM7.gradNormSquaredIntegral_nonneg {n : ℕ} (w : (Fin n → ℝ) → ℝ) (Ω : Set (Fin n → ℝ)) : gradNormSquaredIntegral w Ω ≥ 0

The Dirichlet energy $\int_\Omega \|\nabla w\|^2$ is nonnegative.

theorem CM7.gradNormSquared_integrableOn {n : ℕ} (w : (Fin n → ℝ) → ℝ) (Ω : Set (Fin n → ℝ)) (_hΩo : IsOpen Ω) (hΩb : Bornology.IsBounded Ω) (hcont_fderiv : ContinuousOn (fun (x : Fin n → ℝ) => fderiv ℝ w x) (closure Ω)) : MeasureTheory.IntegrableOn (fun (x : Fin n → ℝ) => ‖fderiv ℝ w x‖ ^ 2) Ω MeasureTheory.volume

If the Fréchet derivative of $w$ is continuous on $\overline{\Omega}$ and $\Omega$ is bounded, then $\|\nabla w\|^2$ is integrable on $\Omega$.

theorem CM7.fderiv_continuousOn_of_contDiffOn {n : ℕ} (w : (Fin n → ℝ) → ℝ) (Ω : Set (Fin n → ℝ)) (hΩo : IsOpen Ω) (hw_c1 : ContDiffOn ℝ 1 w Ω) : ContinuousOn (fun (x : Fin n → ℝ) => fderiv ℝ w x) Ω

A $C^1$ function on an open set has continuous Fréchet derivative on that set.

theorem CM7.grad_zero_of_gradNormSquaredIntegral_zero {n : ℕ} (w : (Fin n → ℝ) → ℝ) (Ω : Set (Fin n → ℝ)) (hΩo : IsOpen Ω) (_hw_diff : DifferentiableOn ℝ w Ω) (hw_c1 : ContDiffOn ℝ 1 w Ω) (hΩb : Bornology.IsBounded Ω) (hcont_fderiv : ContinuousOn (fun (x : Fin n → ℝ) => fderiv ℝ w x) (closure Ω)) (hw : gradNormSquaredIntegral w Ω = 0) (x : Fin n → ℝ) : x ∈ Ω → fderiv ℝ w x = 0

If a $C^1$ function $w$ on a bounded open set $\Omega$ has vanishing Dirichlet energy $\int_\Omega \|\nabla w\|^2 = 0$, then $\nabla w = 0$ pointwise on $\Omega$.

theorem CM7.gradNormSquared_zero_implies_constant {n : ℕ} (w : (Fin n → ℝ) → ℝ) (Ω : Set (Fin n → ℝ)) (hΩo : IsOpen Ω) (hΩc : IsConnected Ω) (hΩb : Bornology.IsBounded Ω) (hw_diff : DifferentiableOn ℝ w Ω) (hw_c1 : ContDiffOn ℝ 1 w Ω) (hw_cont : ContinuousOn w (closure Ω)) (hcont_fderiv : ContinuousOn (fun (x : Fin n → ℝ) => fderiv ℝ w x) (closure Ω)) (hw : gradNormSquaredIntegral w Ω = 0) : ∃ (c : ℝ), ∀ x ∈ closure Ω, w x = c

If $w$ has zero Dirichlet energy on a connected, bounded open set $\Omega$ and is continuous up to the boundary, then $w$ is constant on $\overline{\Omega}$.

theorem CM7.not_isBounded_univ_fin_real {n : ℕ} (hn : 0 < n) : ¬Bornology.IsBounded Set.univ

For $n \geq 1$, the whole space $\mathbb{R}^n$ (modeled as Fin n → ℝ) is not bounded.

theorem CM7.frontier_nonempty_of_bounded_open_connected {n : ℕ} (hn : 0 < n) {Ω : Set (Fin n → ℝ)} (_hΩo : IsOpen Ω) (_hΩc : IsConnected Ω) (hΩb : Bornology.IsBounded Ω) (hΩne : Ω.Nonempty) : (frontier Ω).Nonempty

A nonempty, bounded, open, connected subset of $\mathbb{R}^n$ (with $n \geq 1$) has nonempty topological boundary.

theorem CM7.normalDerivative_sub {n : ℕ} (u v : (Fin n → ℝ) → ℝ) (x : Fin n → ℝ) (hu : DifferentiableAt ℝ u x) (hv : DifferentiableAt ℝ v x) : NormalDerivative n (fun (y : Fin n → ℝ) => u y - v y) x = NormalDerivative n u x - NormalDerivative n v x

Linearity of the normal derivative under subtraction: $\partial_\nu(u - v)(x) = \partial_\nu u(x) - \partial_\nu v(x)$.

theorem CM7.differentiableAt_of_contDiffOn_closure {n : ℕ} (u : (Fin n → ℝ) → ℝ) (Ω : Set (Fin n → ℝ)) (_hΩo : IsOpen Ω) (_hu_reg : ContDiffOn ℝ 2 u Ω) (_hu_cont : ContinuousOn u (closure Ω)) (hu_diff_closure : ∀ x ∈ closure Ω, DifferentiableAt ℝ u x) (x : Fin n → ℝ) (hx : x ∈ closure Ω) : DifferentiableAt ℝ u x

Glue lemma: a function differentiable at every point of $\overline{\Omega}$ is differentiable at any particular point of $\overline{\Omega}$.

theorem CM7.fderiv_zero_on_frontier_of_zero_on_open {n : ℕ} (w : (Fin n → ℝ) → ℝ) (Ω : Set (Fin n → ℝ)) (_hΩo : IsOpen Ω) (h_zero : ∀ y ∈ Ω, fderiv ℝ w y = 0) (hcont_fderiv : ContinuousOn (fun (x : Fin n → ℝ) => fderiv ℝ w x) (closure Ω)) (x : Fin n → ℝ) (hx : x ∈ frontier Ω) : fderiv ℝ w x = 0

If $\nabla w = 0$ on an open set $\Omega$ and $\nabla w$ is continuous on $\overline{\Omega}$, then $\nabla w = 0$ extends to the boundary $\partial \Omega$.

theorem CM7.gradNormSquared_zero_implies_normalDerivative_zero {n : ℕ} (w : (Fin n → ℝ) → ℝ) (Ω : Set (Fin n → ℝ)) (hΩo : IsOpen Ω) (hΩb : Bornology.IsBounded Ω) (hw_diff : DifferentiableOn ℝ w Ω) (hw_c1 : ContDiffOn ℝ 1 w Ω) (hcont_fderiv : ContinuousOn (fun (x : Fin n → ℝ) => fderiv ℝ w x) (closure Ω)) (hw : gradNormSquaredIntegral w Ω = 0) (x : Fin n → ℝ) (hx : x ∈ frontier Ω) : NormalDerivative n w x = 0

If $w$ has vanishing Dirichlet energy on $\Omega$, then the normal derivative $\partial_\nu w$ vanishes on $\partial \Omega$.

theorem CM7.boundary_energy_nonpos_robin {n : ℕ} (w : (Fin n → ℝ) → ℝ) (Ω : Set (Fin n → ℝ)) (_hΩo : IsOpen Ω) (_hΩb : Bornology.IsBounded Ω) {α : ℝ} (hα : 0 < α) (hbc : ∀ x ∈ frontier Ω, NormalDerivative n w x + α * w x = 0) : boundaryEnergyIntegral w Ω ≤ 0

Under a homogeneous Robin boundary condition $\partial_\nu w + \alpha w = 0$ with $\alpha > 0$, the boundary energy integral $\int_{\partial \Omega} w \, \partial_\nu w \, dS$ is nonpositive.

theorem CM7.boundary_energy_zero_neumann {n : ℕ} (w : (Fin n → ℝ) → ℝ) (Ω : Set (Fin n → ℝ)) (_hΩo : IsOpen Ω) (_hΩb : Bornology.IsBounded Ω) (hbc : ∀ x ∈ frontier Ω, NormalDerivative n w x = 0) : boundaryEnergyIntegral w Ω = 0

Under a homogeneous Neumann boundary condition $\partial_\nu w = 0$, the boundary energy integral vanishes.

theorem CM7.boundary_energy_zero_mixed {n : ℕ} (w : (Fin n → ℝ) → ℝ) (Ω : Set (Fin n → ℝ)) (_hΩo : IsOpen Ω) (_hΩb : Bornology.IsBounded Ω) {S_D S_N : Set (Fin n → ℝ)} (hcover : frontier Ω = S_D ∪ S_N) (_hdisjoint : Disjoint S_D S_N) (hbc_D : ∀ x ∈ S_D, w x = 0) (hbc_N : ∀ x ∈ S_N, NormalDerivative n w x = 0) : boundaryEnergyIntegral w Ω = 0

Under mixed boundary conditions — $w = 0$ on a Dirichlet portion $S_D$ and $\partial_\nu w = 0$ on a Neumann portion $S_N$, with $\partial \Omega = S_D \cup S_N$ — the boundary energy integral vanishes.

theorem CM7.poisson_uniqueness_robin {n : ℕ} (hn : 0 < n) {Ω : Set (Fin n → ℝ)} (hΩo : IsOpen Ω) (hΩc : IsConnected Ω) (hΩb : Bornology.IsBounded Ω) {f g : (Fin n → ℝ) → ℝ} {α : ℝ} (hα : 0 < α) {u v : (Fin n → ℝ) → ℝ} (_hu_reg : ContDiffOn ℝ 2 u Ω) (_hv_reg : ContDiffOn ℝ 2 v Ω) (_hu_cont : ContinuousOn u (closure Ω)) (_hv_cont : ContinuousOn v (closure Ω)) (_hu_diff_cl : ∀ x ∈ closure Ω, DifferentiableAt ℝ u x) (_hv_diff_cl : ∀ x ∈ closure Ω, DifferentiableAt ℝ v x) (_hu_fderiv_cont : ContinuousOn (fun (x : Fin n → ℝ) => fderiv ℝ u x) (closure Ω)) (_hv_fderiv_cont : ContinuousOn (fun (x : Fin n → ℝ) => fderiv ℝ v x) (closure Ω)) (hu : IsPoisson u f Ω) (hv : IsPoisson v f Ω) (hbc_u : ∀ x ∈ frontier Ω, NormalDerivative n u x + α * u x = g x) (hbc_v : ∀ x ∈ frontier Ω, NormalDerivative n v x + α * v x = g x) (x : Fin n → ℝ) : x ∈ closure Ω → u x = v x

Uniqueness for Poisson's equation with Robin boundary conditions $\partial_\nu u + \alpha u = g$ ($\alpha > 0$): two solutions $u, v$ of $\Delta u = f = \Delta v$ on a bounded connected open set $\Omega$ that satisfy the same Robin condition agree on $\overline{\Omega}$.

theorem CM7.poisson_uniqueness_neumann {n : ℕ} {Ω : Set (Fin n → ℝ)} (hΩo : IsOpen Ω) (hΩc : IsConnected Ω) (hΩb : Bornology.IsBounded Ω) {f h u v : (Fin n → ℝ) → ℝ} (_hu_reg : ContDiffOn ℝ 2 u Ω) (_hv_reg : ContDiffOn ℝ 2 v Ω) (_hu_cont : ContinuousOn u (closure Ω)) (_hv_cont : ContinuousOn v (closure Ω)) (_hu_diff_cl : ∀ x ∈ closure Ω, DifferentiableAt ℝ u x) (_hv_diff_cl : ∀ x ∈ closure Ω, DifferentiableAt ℝ v x) (_hu_fderiv_cont : ContinuousOn (fun (x : Fin n → ℝ) => fderiv ℝ u x) (closure Ω)) (_hv_fderiv_cont : ContinuousOn (fun (x : Fin n → ℝ) => fderiv ℝ v x) (closure Ω)) (hu : IsPoisson u f Ω) (hv : IsPoisson v f Ω) (hbc_u : ∀ x ∈ frontier Ω, NormalDerivative n u x = h x) (hbc_v : ∀ x ∈ frontier Ω, NormalDerivative n v x = h x) : ∃ (c : ℝ), ∀ x ∈ closure Ω, u x = v x + c

Uniqueness up to constants for Poisson's equation with Neumann boundary conditions $\partial_\nu u = h$: any two solutions $u, v$ differ by an additive constant on $\overline{\Omega}$.

theorem CM7.poisson_uniqueness_mixed {n : ℕ} {Ω : Set (Fin n → ℝ)} (hΩo : IsOpen Ω) (hΩc : IsConnected Ω) (hΩb : Bornology.IsBounded Ω) {f : (Fin n → ℝ) → ℝ} {S_D S_N : Set (Fin n → ℝ)} (hcover : frontier Ω = S_D ∪ S_N) (hdisjoint : Disjoint S_D S_N) (hSD_nonempty : S_D.Nonempty) {g_D g_N u v : (Fin n → ℝ) → ℝ} (_hu_reg : ContDiffOn ℝ 2 u Ω) (_hv_reg : ContDiffOn ℝ 2 v Ω) (_hu_cont : ContinuousOn u (closure Ω)) (_hv_cont : ContinuousOn v (closure Ω)) (_hu_diff_cl : ∀ x ∈ closure Ω, DifferentiableAt ℝ u x) (_hv_diff_cl : ∀ x ∈ closure Ω, DifferentiableAt ℝ v x) (_hu_fderiv_cont : ContinuousOn (fun (x : Fin n → ℝ) => fderiv ℝ u x) (closure Ω)) (_hv_fderiv_cont : ContinuousOn (fun (x : Fin n → ℝ) => fderiv ℝ v x) (closure Ω)) (hu : IsPoisson u f Ω) (hv : IsPoisson v f Ω) (hbc_u_D : ∀ x ∈ S_D, u x = g_D x) (hbc_v_D : ∀ x ∈ S_D, v x = g_D x) (hbc_u_N : ∀ x ∈ S_N, NormalDerivative n u x = g_N x) (hbc_v_N : ∀ x ∈ S_N, NormalDerivative n v x = g_N x) (x : Fin n → ℝ) : x ∈ closure Ω → u x = v x

Uniqueness for Poisson's equation under mixed Dirichlet/Neumann boundary conditions: with $\partial \Omega = S_D \sqcup S_N$ (nonempty Dirichlet portion $S_D$), $u = g_D$ on $S_D$ and $\partial_\nu u = g_N$ on $S_N$, any two such solutions agree on $\overline{\Omega}$.

noncomputable def CM7.sphericalMean {n : ℕ} (u : (Fin n → ℝ) → ℝ) (x : Fin n → ℝ) (r : ℝ) : ℝ

The spherical mean of $u$ around the point $x$ at radius $r$: the average value of $u$ over the sphere of radius $r$ centered at $x$, taken with respect to the $(n-1)$-dimensional Hausdorff measure. By convention, the value at $r = 0$ is $u(x)$.

noncomputable def CM7.sphericalAvgFun {n : ℕ} (u : (Fin n → ℝ) → ℝ) (x : Fin n → ℝ) : ℝ → ℝ

The "spherical-average" function $r \mapsto \fint_{S^{n-1}} u(x + r\omega) \, d\sigma(\omega)$, i.e. sphericalMean u x r but without the special-case branch at $r = 0$.

theorem CM7.sphericalAvgFun_differentiableOn_Ioo {n : ℕ} (u : (Fin n → ℝ) → ℝ) (x : Fin n → ℝ) (R : ℝ) (hR : 0 < R) (hu : IsHarmonic u (Metric.ball x R)) : DifferentiableOn ℝ (sphericalAvgFun u x) (Set.Ioo 0 R)

For a harmonic function $u$ on the ball $B(x, R)$, the spherical average function $r \mapsto \fint_{S^{n-1}} u(x + r\omega)\, d\sigma(\omega)$ is differentiable on $(0, R)$.

theorem CM7.divergence_theorem_ball {n : ℕ} (u : (Fin n → ℝ) → ℝ) (x : Fin n → ℝ) (r : ℝ) (hr : 0 < r) (hu : ContDiffOn ℝ 2 u (Metric.closedBall x r)) : ∫ (y : Fin n → ℝ) in Metric.ball x r, Laplacian n u y = ∫ (y : Fin n → ℝ) in frontier (Metric.ball x r), NormalDerivative n u y ∂surfaceMeasure n (Metric.ball x r)

The divergence theorem applied to $\nabla u$ on the ball $B(x, r)$: $\int_{B(x,r)} \Delta u = \int_{\partial B(x,r)} \partial_\nu u \, dS$.

theorem CM7.sphericalAvgFun_deriv_eq_boundary_normal_integral {n : ℕ} (u : (Fin n → ℝ) → ℝ) (x : Fin n → ℝ) (R : ℝ) (hR : 0 < R) (hu : ContDiffOn ℝ 2 u (Metric.ball x R)) (r : ℝ) (hr : r ∈ Set.Ioo 0 R) : ∃ (K : ℝ), deriv (sphericalAvgFun u x) r = K * ∫ (y : Fin n → ℝ) in frontier (Metric.ball x r), NormalDerivative n u y ∂surfaceMeasure n (Metric.ball x r)

For a $C^2$ function $u$ on $B(x, R)$, the derivative of the spherical average function at $r \in (0, R)$ is, up to a constant $K$, the boundary integral of the normal derivative $\int_{\partial B(x,r)} \partial_\nu u \, dS$.

theorem CM7.sphericalAvgFun_deriv_eq_scaled_laplacian_integral {n : ℕ} (u : (Fin n → ℝ) → ℝ) (x : Fin n → ℝ) (R : ℝ) (hR : 0 < R) (hu : ContDiffOn ℝ 2 u (Metric.ball x R)) (r : ℝ) (hr : r ∈ Set.Ioo 0 R) : ∃ (C : ℝ), deriv (sphericalAvgFun u x) r = C * ∫ (y : Fin n → ℝ) in Metric.ball x r, Laplacian n u y

Combining the boundary-normal formula for the derivative of the spherical mean with the divergence theorem: for $r \in (0, R)$, the derivative of the spherical-average function is, up to a constant, the volume integral of the Laplacian, $C \cdot \int_{B(x,r)} \Delta u$.

theorem CM7.sphericalAvgFun_deriv_eq_zero_of_harmonic {n : ℕ} (u : (Fin n → ℝ) → ℝ) (x : Fin n → ℝ) (R : ℝ) (hR : 0 < R) (hu : IsHarmonic u (Metric.ball x R)) : Set.EqOn (deriv (sphericalAvgFun u x)) 0 (Set.Ioo 0 R)

For a harmonic function $u$ on the ball $B(x, R)$, the derivative of the spherical-average function $r \mapsto \fint_{S^{n-1}} u(x + r\omega)$ vanishes on $(0, R)$.

theorem CM7.integrableOn_sphere_of_continuousAt (n : ℕ) (hn : 0 < n) (u : (Fin n → ℝ) → ℝ) (x : Fin n → ℝ) (hu : ContinuousAt u x) (t : ℝ) : MeasureTheory.IntegrableOn (fun (ω : Fin n → ℝ) => u (x + t • ω)) (Metric.sphere 0 1) (MeasureTheory.Measure.hausdorffMeasure ↑(n - 1))

If $u$ is continuous at $x$, then for any $t$ the scaled translate $\omega \mapsto u(x + t\omega)$ is integrable over the unit sphere with respect to the $(n-1)$-Hausdorff measure.

theorem CM7.norm_setAverage_sub_le {n : ℕ} (hn : 0 < n) (f : (Fin n → ℝ) → ℝ) (c C : ℝ) (hC : 0 ≤ C) (hf_int : MeasureTheory.IntegrableOn f (Metric.sphere 0 1) (MeasureTheory.Measure.hausdorffMeasure ↑(n - 1))) (hbound : ∀ ω ∈ Metric.sphere 0 1, ‖f ω - c‖ ≤ C) : ‖⨍ (ω : Fin n → ℝ) in Metric.sphere 0 1, f ω ∂MeasureTheory.Measure.hausdorffMeasure ↑(n - 1) - c‖ ≤ C

If $\|f(\omega) - c\| \leq C$ uniformly on the unit sphere $S^{n-1}$, then the deviation of the spherical average from $c$ is also bounded by $C$: $\|\fint_{S^{n-1}} f \, d\sigma - c\| \leq C$.

theorem CM7.setAverage_sphere_tendsto_of_continuousAt {n : ℕ} (hn : 0 < n) (u : (Fin n → ℝ) → ℝ) (x : Fin n → ℝ) (hu : ContinuousAt u x) : Filter.Tendsto (fun (t : ℝ) => ⨍ (ω : Fin n → ℝ) in Metric.sphere 0 1, u (x + t • ω) ∂MeasureTheory.Measure.hausdorffMeasure ↑(n - 1)) (nhdsWithin 0 (Set.Ioi 0)) (nhds (u x))

If $u$ is continuous at $x$, then the spherical average $\fint_{S^{n-1}} u(x + t\omega)\, d\sigma(\omega)$ tends to $u(x)$ as $t \to 0^+$.

theorem CM7.sphericalAvg_const_of_harmonic {n : ℕ} (u : (Fin n → ℝ) → ℝ) (x : Fin n → ℝ) (R : ℝ) (hR : 0 < R) (hu : IsHarmonic u (Metric.ball x R)) (r s : ℝ) (hr_pos : 0 < r) (hr_lt : r < R) (hs_pos : 0 < s) (hs_le : s ≤ r) : ⨍ (ω : Fin n → ℝ) in Metric.sphere 0 1, u (x + s • ω) ∂MeasureTheory.Measure.hausdorffMeasure ↑(n - 1) = ⨍ (ω : Fin n → ℝ) in Metric.sphere 0 1, u (x + r • ω) ∂MeasureTheory.Measure.hausdorffMeasure ↑(n - 1)

For $u$ harmonic on $B(x, R)$ and $0 < s \leq r < R$, the spherical averages of $u$ over spheres of radii $s$ and $r$ centered at $x$ agree.

theorem CM7.sphericalAvg_tendsto_at_zero {n : ℕ} (hn : 0 < n) (u : (Fin n → ℝ) → ℝ) (x : Fin n → ℝ) (R : ℝ) (hR : 0 < R) (hu : IsHarmonic u (Metric.ball x R)) : Filter.Tendsto (fun (t : ℝ) => ⨍ (ω : Fin n → ℝ) in Metric.sphere 0 1, u (x + t • ω) ∂MeasureTheory.Measure.hausdorffMeasure ↑(n - 1)) (nhdsWithin 0 (Set.Ioi 0)) (nhds (u x))

For $u$ harmonic on $B(x, R)$, the spherical average $\fint_{S^{n-1}} u(x + t\omega)\, d\sigma(\omega)$ tends to $u(x)$ as $t \to 0^+$ (specialization of the continuity-based version).

theorem CM7.sphericalMean_integral_eq_center {n : ℕ} (hn : 0 < n) (u : (Fin n → ℝ) → ℝ) (x : Fin n → ℝ) (R : ℝ) (hR : 0 < R) (hu : IsHarmonic u (Metric.ball x R)) (r : ℝ) (hr_pos : 0 < r) (hr_lt : r < R) : ⨍ (ω : Fin n → ℝ) in Metric.sphere 0 1, u (x + r • ω) ∂MeasureTheory.Measure.hausdorffMeasure ↑(n - 1) = u x

Spherical mean-value property: for $u$ harmonic on $B(x, R)$ and any $r \in (0, R)$, the spherical average $\fint_{S^{n-1}} u(x + r\omega)\, d\sigma(\omega)$ equals $u(x)$.

theorem CM7.sphericalMean_const_on_Ico_of_harmonic {n : ℕ} (hn : 0 < n) (u : (Fin n → ℝ) → ℝ) (x : Fin n → ℝ) (R : ℝ) (hR : 0 < R) (hu : IsHarmonic u (Metric.ball x R)) (r s : ℝ) (hr : r ∈ Set.Ico 0 R) (hs : s ∈ Set.Ico 0 R) : sphericalMean u x r = sphericalMean u x s

For $u$ harmonic on $B(x, R)$, the function $r \mapsto$ sphericalMean u x r is constant on $[0, R)$.

theorem CM7.sphericalMean_hasDerivWithinAt_zero_divergence {n : ℕ} (hn : 0 < n) (u : (Fin n → ℝ) → ℝ) (x : Fin n → ℝ) (R : ℝ) (hR : 0 < R) (hu : IsHarmonic u (Metric.ball x R)) (t : ℝ) (ht : t ∈ Set.Ico 0 R) : HasDerivWithinAt (sphericalMean u x) 0 (Set.Ici t) t

Since sphericalMean u x is constant on $[0, R)$ for harmonic $u$, it has right derivative zero at any $t \in [0, R)$ (in the sense of HasDerivWithinAt restricted to $[t, \infty)$).

theorem CM7.sphericalMean_continuousOn_Icc_sub {n : ℕ} (hn : 0 < n) (u : (Fin n → ℝ) → ℝ) (x : Fin n → ℝ) (R : ℝ) (hR : 0 < R) (hu : IsHarmonic u (Metric.ball x R)) (b : ℝ) (_hb_pos : 0 < b) (hb_lt : b < R) : ContinuousOn (sphericalMean u x) (Set.Icc 0 b)

For $u$ harmonic on $B(x, R)$ and $0 < b < R$, the spherical mean function is continuous on the closed interval $[0, b]$.

theorem CM7.sphericalMean_locallyConst_of_harmonic {n : ℕ} (hn : 0 < n) (u : (Fin n → ℝ) → ℝ) (x : Fin n → ℝ) (R : ℝ) (hR : 0 < R) (hu : IsHarmonic u (Metric.ball x R)) (r : ℝ) (hr : r ∈ Set.Ico 0 R) : ∀ᶠ (t : ℝ) in nhdsWithin r (Set.Ici r), sphericalMean u x t = sphericalMean u x r

For $u$ harmonic on $B(x, R)$, the spherical mean function is locally constant from the right at every $r \in [0, R)$: it agrees with sphericalMean u x r on a right-neighborhood of $r$ in $[r, \infty)$.

theorem CM7.sphericalMean_hasDerivWithinAt_zero {n : ℕ} (hn : 0 < n) (u : (Fin n → ℝ) → ℝ) (x : Fin n → ℝ) (R : ℝ) (hR : 0 < R) (hu : IsHarmonic u (Metric.ball x R)) (r : ℝ) (hr : r ∈ Set.Ico 0 R) : HasDerivWithinAt (sphericalMean u x) 0 (Set.Ici r) r

The right derivative of the spherical mean function is zero at every $r \in [0, R)$, for $u$ harmonic on $B(x, R)$.

theorem CM7.sphericalMean_diffOn_Ico {n : ℕ} (hn : 0 < n) (u : (Fin n → ℝ) → ℝ) (x : Fin n → ℝ) (R : ℝ) (hR : 0 < R) (hu : IsHarmonic u (Metric.ball x R)) : DifferentiableOn ℝ (sphericalMean u x) (Set.Ico 0 R)

For $u$ harmonic on $B(x, R)$, the spherical mean function is differentiable on $[0, R)$ (in the sense of DifferentiableOn).

theorem CM7.setAverage_sphere_leftContinuousAt {n : ℕ} (u : (Fin n → ℝ) → ℝ) (x : Fin n → ℝ) (R : ℝ) (hR : 0 < R) (hu : IsHarmonic u (Metric.ball x R)) : Filter.Tendsto (fun (r : ℝ) => ⨍ (ω : Fin n → ℝ) in Metric.sphere 0 1, u (x + r • ω) ∂MeasureTheory.Measure.hausdorffMeasure ↑(n - 1)) (nhdsWithin R (Set.Iio R)) (nhds (⨍ (ω : Fin n → ℝ) in Metric.sphere 0 1, u (x + R • ω) ∂MeasureTheory.Measure.hausdorffMeasure ↑(n - 1)))

Left-continuity of the spherical-average function at $r = R$ for $u$ harmonic on $B(x, R)$: the average $\fint_{S^{n-1}} u(x + r\omega)$ tends, as $r \to R^-$, to the corresponding average at radius $R$.

theorem CM7.sphericalMean_avg_eq_center_at_boundary {n : ℕ} (hn : 0 < n) (u : (Fin n → ℝ) → ℝ) (x : Fin n → ℝ) (R : ℝ) (hR : 0 < R) (hu : IsHarmonic u (Metric.ball x R)) : ⨍ (ω : Fin n → ℝ) in Metric.sphere 0 1, u (x + R • ω) ∂MeasureTheory.Measure.hausdorffMeasure ↑(n - 1) = u x

The spherical mean-value property extended to the boundary radius: for $u$ harmonic on $B(x, R)$, $\fint_{S^{n-1}} u(x + R\omega)\, d\sigma(\omega) = u(x)$.

theorem CM7.sphericalMean_avg_continuousWithinAt {n : ℕ} (hn : 0 < n) (u : (Fin n → ℝ) → ℝ) (x : Fin n → ℝ) (R : ℝ) (hR : 0 < R) (hu : IsHarmonic u (Metric.ball x R)) : ContinuousWithinAt (fun (r : ℝ) => ⨍ (ω : Fin n → ℝ) in Metric.sphere 0 1, u (x + r • ω) ∂MeasureTheory.Measure.hausdorffMeasure ↑(n - 1)) (Set.Icc 0 R) R

For $u$ harmonic on $B(x, R)$, the spherical-average function is continuous within $[0, R]$ at the endpoint $R$.

theorem CM7.sphericalMean_continuousWithinAt_endpoint {n : ℕ} (hn : 0 < n) (u : (Fin n → ℝ) → ℝ) (x : Fin n → ℝ) (R : ℝ) (hR : 0 < R) (hu : IsHarmonic u (Metric.ball x R)) : ContinuousWithinAt (sphericalMean u x) (Set.Icc 0 R) R

For $u$ harmonic on $B(x, R)$, the spherical mean function sphericalMean u x is continuous within $[0, R]$ at the endpoint $R$.

theorem CM7.sphericalMean_continuousOn {n : ℕ} (hn : 0 < n) (u : (Fin n → ℝ) → ℝ) (x : Fin n → ℝ) (R : ℝ) (hR : 0 < R) (hu : IsHarmonic u (Metric.ball x R)) : ContinuousOn (sphericalMean u x) (Set.Icc 0 R)

For $u$ harmonic on $B(x, R)$, the spherical mean function is continuous on the closed interval $[0, R]$.

theorem CM7.sphericalMean_at_zero {n : ℕ} (u : (Fin n → ℝ) → ℝ) (x : Fin n → ℝ) (R : ℝ) (_hR : 0 < R) (_hu : IsHarmonic u (Metric.ball x R)) : sphericalMean u x 0 = u x

By definition, sphericalMean u x 0 = u x.

theorem CM7.harmonic_sphere_mean_value {n : ℕ} (hn : 0 < n) (u : (Fin n → ℝ) → ℝ) (x : Fin n → ℝ) (R : ℝ) (hR : 0 < R) (hu : IsHarmonic u (Metric.ball x R)) (r : ℝ) (hr : 0 < r) (hrR : r ≤ R) : sphericalMean u x r = u x

Spherical mean-value property for harmonic functions: for $u$ harmonic on $B(x, R)$ and any $r \in (0, R]$, the spherical mean satisfies sphericalMean u x r = u(x).

theorem CM7.polar_coordinate_ball_integral_toSphere {n : ℕ} (hn : 0 < n) (g : (Fin n → ℝ) → ℝ) (R : ℝ) (hR : 0 < R) : ∫ (y : Fin n → ℝ) in Metric.ball 0 R, g y = (MeasureTheory.volume (Metric.ball 0 1)).toReal * ↑n * ∫ (r : ℝ) in 0..R, r ^ (↑n - 1) * ⨍ (ω : ↑(Metric.sphere 0 1)), g (r • ↑ω) ∂MeasureTheory.volume.toSphere

Polar-coordinate decomposition of a ball integral: for a function $g$ on $\mathbb{R}^n$, $\int_{B(0,R)} g(y)\, dy = |B(0,1)| \cdot n \int_0^R r^{n-1} \fint_{S^{n-1}} g(r\omega)\, d\omega \, dr$, where the inner average is taken with respect to the toSphere measure on the unit sphere.

theorem CM7.average_toSphere_eq_setAverage_hausdorff {n : ℕ} (hn : 0 < n) (f : (Fin n → ℝ) → ℝ) : ⨍ (ω : ↑(Metric.sphere 0 1)), f ↑ω ∂MeasureTheory.volume.toSphere = ⨍ (ω : Fin n → ℝ) in Metric.sphere 0 1, f ω ∂MeasureTheory.Measure.hausdorffMeasure ↑(n - 1)

Compatibility of two spherical averages on $S^{n-1}$: the average computed via the toSphere measure derived from the Lebesgue measure agrees with the average computed via the $(n-1)$-dimensional Hausdorff measure.

theorem CM7.setIntegral_ball_zero_eq_radial_sphericalAvg {n : ℕ} (hn : 0 < n) (g : (Fin n → ℝ) → ℝ) (R : ℝ) (hR : 0 < R) : ∫ (y : Fin n → ℝ) in Metric.ball 0 R, g y = (MeasureTheory.volume (Metric.ball 0 1)).toReal * ↑n * ∫ (r : ℝ) in 0..R, r ^ (↑n - 1) * ⨍ (ω : Fin n → ℝ) in Metric.sphere 0 1, g (r • ω) ∂MeasureTheory.Measure.hausdorffMeasure ↑(n - 1)

Polar-coordinate decomposition of a ball integral with the spherical average expressed via the $(n-1)$-Hausdorff measure: $\int_{B(0,R)} g(y)\, dy = |B(0,1)| \cdot n \int_0^R r^{n-1} \fint_{S^{n-1}} g(r\omega)\, d\sigma(\omega)\, dr$.

theorem CM7.setIntegral_ball_eq_radial_sphericalMean {n : ℕ} (hn : 0 < n) (u : (Fin n → ℝ) → ℝ) (x : Fin n → ℝ) (R : ℝ) (hR : 0 < R) : ∫ (y : Fin n → ℝ) in Metric.ball x R, u y = (MeasureTheory.volume (Metric.ball 0 1)).toReal * ↑n * ∫ (r : ℝ) in 0..R, r ^ (↑n - 1) * sphericalMean u x r

Radial decomposition of the integral of $u$ over $B(x, R)$ in terms of spherical means: $\int_{B(x,R)} u(y)\, dy = |B(0,1)| \cdot n \int_0^R r^{n-1} \cdot \mathrm{sphericalMean}(u, x, r)\, dr$.

theorem CM7.polar_coordinate_volume_decomposition {n : ℕ} (hn : 0 < n) (u : (Fin n → ℝ) → ℝ) (x : Fin n → ℝ) (R : ℝ) (hR : 0 < R) : ⨍ (y : Fin n → ℝ) in Metric.ball x R, u y = ↑n / R ^ ↑n * ∫ (r : ℝ) in 0..R, r ^ (↑n - 1) * sphericalMean u x r

Volume average of $u$ over $B(x, R)$ as a weighted integral of spherical means: $\fint_{B(x,R)} u \, dy = \frac{n}{R^n} \int_0^R r^{n-1} \cdot \mathrm{sphericalMean}(u, x, r)\, dr$.

theorem CM7.volume_average_from_constant_sphere_mean {n : ℕ} (u : (Fin n → ℝ) → ℝ) (x : Fin n → ℝ) (R : ℝ) (hR : 0 < R) (c : ℝ) (hsphere : ∀ (r : ℝ), 0 < r → r ≤ R → sphericalMean u x r = c) (hn : 0 < n) : ⨍ (y : Fin n → ℝ) in Metric.ball x R, u y = c

If the spherical mean sphericalMean u x r equals a constant $c$ for every $r \in (0, R]$, then the volume average of $u$ over $B(x, R)$ equals $c$.

theorem CM7.harmonic_volume_mean_value {n : ℕ} (hn : 0 < n) {Ω : Set (Fin n → ℝ)} {u : (Fin n → ℝ) → ℝ} (hu : IsHarmonic u Ω) {x : Fin n → ℝ} {R : ℝ} (hR : 0 < R) (hball : Metric.closedBall x R ⊆ Ω) : u x = ⨍ (y : Fin n → ℝ) in Metric.ball x R, u y

Volume mean-value property for harmonic functions: if $u$ is harmonic on $\Omega$ and $\overline{B(x, R)} \subseteq \Omega$, then $u(x) = \fint_{B(x, R)} u(y)\, dy$.

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

The predicate that $u$ is continuous on $\Omega$ and satisfies the volume mean-value property on $\Omega$: for every $x \in \Omega$ and every closed ball $\overline{B(x, R)} \subseteq \Omega$, $u(x) = \fint_{B(x, R)} u$.

theorem CM7.mvp_max_const_on_ball {n : ℕ} {u : (Fin n → ℝ) → ℝ} {q : Fin n → ℝ} {r M : ℝ} (hr : 0 < r) (Ω : Set (Fin n → ℝ)) (hball : Metric.closedBall q r ⊆ Ω) (hcont : ContinuousOn u Ω) (hmvp_q : u q = ⨍ (y : Fin n → ℝ) in Metric.ball q r, u y) (hle : ∀ y ∈ Metric.ball q r, u y ≤ M) (hqM : u q = M) (y : Fin n → ℝ) : y ∈ Metric.ball q r → u y = M

Mean-value maximum lemma: if a continuous function $u$ satisfies the volume MVP at $q$ on $B(q, r)$, is bounded above by $M$ on $B(q, r)$, and attains the value $M$ at $q$, then $u \equiv M$ on the whole open ball $B(q, r)$.

theorem CM7.strong_max_principle {n : ℕ} {Ω : Set (Fin n → ℝ)} (hΩo : IsOpen Ω) (hΩc : IsConnected Ω) {u : (Fin n → ℝ) → ℝ} (hmvp : HasVolumeMVP u Ω) {p : Fin n → ℝ} (hp : p ∈ Ω) (hmax : ∀ x ∈ Ω, u x ≤ u p) (x : Fin n → ℝ) : x ∈ Ω → u x = u p

Strong maximum principle: if $u$ has the volume mean-value property on a connected open set $\Omega$ and attains its supremum over $\Omega$ at an interior point $p$, then $u$ is constant on $\Omega$.

theorem CM7.strong_min_principle {n : ℕ} {Ω : Set (Fin n → ℝ)} (hΩo : IsOpen Ω) (hΩc : IsConnected Ω) {u : (Fin n → ℝ) → ℝ} (hmvp : HasVolumeMVP u Ω) {p : Fin n → ℝ} (hp : p ∈ Ω) (hmin : ∀ x ∈ Ω, u p ≤ u x) (x : Fin n → ℝ) : x ∈ Ω → u x = u p

Strong minimum principle: if $u$ has the volume mean-value property on a connected open set $\Omega$ and attains its infimum over $\Omega$ at an interior point $p$, then $u$ is constant on $\Omega$.

theorem CM7.weak_max_principle {n : ℕ} (hn : 0 < n) {Ω : Set (Fin n → ℝ)} (hΩo : IsOpen Ω) (hΩc : IsConnected Ω) (hΩb : Bornology.IsBounded Ω) (hΩne : Ω.Nonempty) {u : (Fin n → ℝ) → ℝ} (hu : IsHarmonic u Ω) (hcont : ContinuousOn u (closure Ω)) (x : Fin n → ℝ) (hx : x ∈ closure Ω) : ∃ q ∈ frontier Ω, u x ≤ u q

Weak maximum principle for harmonic functions: if $u$ is harmonic on a bounded connected open set $\Omega$ and continuous on $\overline{\Omega}$, then for every $x \in \overline{\Omega}$ there is a point $q \in \partial \Omega$ with $u(x) \leq u(q)$.

theorem CM7.dirichlet_uniqueness {n : ℕ} (hn : 0 < n) {Ω : Set (Fin n → ℝ)} (hΩo : IsOpen Ω) (hΩc : IsConnected Ω) (hΩb : Bornology.IsBounded Ω) {u₁ u₂ : (Fin n → ℝ) → ℝ} (h1 : IsHarmonic u₁ Ω) (h2 : IsHarmonic u₂ Ω) (hbdy : ∀ x ∈ frontier Ω, u₁ x = u₂ x) (hcont1 : ContinuousOn u₁ (closure Ω)) (hcont2 : ContinuousOn u₂ (closure Ω)) (x : Fin n → ℝ) : x ∈ Ω → u₁ x = u₂ x

Uniqueness for the Dirichlet problem for Laplace's equation: two harmonic functions on a bounded connected open set $\Omega$ that agree on the boundary $\partial \Omega$ and are continuous on $\overline{\Omega}$ agree throughout $\Omega$.

theorem CM7.poisson_uniqueness_dirichlet {n : ℕ} (hn : 0 < n) {Ω : Set (Fin n → ℝ)} (hΩo : IsOpen Ω) (hΩc : IsConnected Ω) (hΩb : Bornology.IsBounded Ω) {f u v : (Fin n → ℝ) → ℝ} (_hu_reg : ContDiffOn ℝ 2 u Ω) (_hv_reg : ContDiffOn ℝ 2 v Ω) (_hu_cont : ContinuousOn u (closure Ω)) (_hv_cont : ContinuousOn v (closure Ω)) (hu : IsPoisson u f Ω) (hv : IsPoisson v f Ω) (hbc : ∀ x ∈ frontier Ω, u x = v x) (x : Fin n → ℝ) : x ∈ closure Ω → u x = v x

Uniqueness for Poisson's equation with Dirichlet boundary data: if $u, v$ both solve $\Delta u = f$ on a bounded connected open set $\Omega$, are continuous on $\overline{\Omega}$, and agree on $\partial \Omega$, then $u = v$ on $\overline{\Omega}$.

theorem CM7.comparison_principle {n : ℕ} (hn : 0 < n) {Ω : Set (Fin n → ℝ)} (hΩo : IsOpen Ω) (hΩc : IsConnected Ω) (hΩb : Bornology.IsBounded Ω) {u_f u_g : (Fin n → ℝ) → ℝ} (hf : IsHarmonic u_f Ω) (hg : IsHarmonic u_g Ω) (hcont_f : ContinuousOn u_f (closure Ω)) (hcont_g : ContinuousOn u_g (closure Ω)) (hbdy_ge : ∀ x ∈ frontier Ω, u_f x ≥ u_g x) (hbdy_ne : ∃ y ∈ frontier Ω, u_f y > u_g y) (x : Fin n → ℝ) (hx : x ∈ Ω) : u_f x > u_g x

Comparison principle (strict version): if $u_f, u_g$ are harmonic on a bounded connected open $\Omega$, continuous on $\overline{\Omega}$, with $u_f \geq u_g$ on $\partial \Omega$ and strict inequality $u_f > u_g$ at some boundary point, then $u_f > u_g$ throughout $\Omega$.

theorem CM7.laplace_stability_estimate {n : ℕ} (hn : 0 < n) {Ω : Set (Fin n → ℝ)} (hΩo : IsOpen Ω) (hΩc : IsConnected Ω) (hΩb : Bornology.IsBounded Ω) {u_f u_g : (Fin n → ℝ) → ℝ} (huf : IsHarmonic u_f Ω) (hug : IsHarmonic u_g Ω) (huf_cont : ContinuousOn u_f (closure Ω)) (hug_cont : ContinuousOn u_g (closure Ω)) {f g : (Fin n → ℝ) → ℝ} (huf_bd : ∀ x ∈ frontier Ω, u_f x = f x) (hug_bd : ∀ x ∈ frontier Ω, u_g x = g x) {M : ℝ} (hM : ∀ y ∈ frontier Ω, |f y - g y| ≤ M) (x : Fin n → ℝ) (hx : x ∈ Ω) : |u_f x - u_g x| ≤ M

Stability estimate for Laplace's equation: if $u_f, u_g$ are harmonic on $\Omega$ with boundary values $f, g$ respectively, and $|f - g| \leq M$ on $\partial \Omega$, then $|u_f - u_g| \leq M$ throughout $\Omega$.

theorem CM7.poisson_uniqueness : (∀ {n : ℕ}, 0 < n → ∀ {Ω : Set (Fin n → ℝ)}, IsOpen Ω → IsConnected Ω → Bornology.IsBounded Ω → ∀ {f u v : (Fin n → ℝ) → ℝ}, ContDiffOn ℝ 2 u Ω → ContDiffOn ℝ 2 v Ω → ContinuousOn u (closure Ω) → ContinuousOn v (closure Ω) → IsPoisson u f Ω → IsPoisson v f Ω → (∀ x ∈ frontier Ω, u x = v x) → ∀ x ∈ closure Ω, u x = v x) ∧ (∀ {n : ℕ}, 0 < n → ∀ {Ω : Set (Fin n → ℝ)}, IsOpen Ω → IsConnected Ω → Bornology.IsBounded Ω → ∀ {f g : (Fin n → ℝ) → ℝ} {α : ℝ}, 0 < α → ∀ {u v : (Fin n → ℝ) → ℝ}, ContDiffOn ℝ 2 u Ω → ContDiffOn ℝ 2 v Ω → ContinuousOn u (closure Ω) → ContinuousOn v (closure Ω) → (∀ x ∈ closure Ω, DifferentiableAt ℝ u x) → (∀ x ∈ closure Ω, DifferentiableAt ℝ v x) → ContinuousOn (fun (x : Fin n → ℝ) => fderiv ℝ u x) (closure Ω) → ContinuousOn (fun (x : Fin n → ℝ) => fderiv ℝ v x) (closure Ω) → IsPoisson u f Ω → IsPoisson v f Ω → (∀ x ∈ frontier Ω, NormalDerivative n u x + α * u x = g x) → (∀ x ∈ frontier Ω, NormalDerivative n v x + α * v x = g x) → ∀ x ∈ closure Ω, u x = v x) ∧ (∀ {n : ℕ} {Ω : Set (Fin n → ℝ)}, IsOpen Ω → IsConnected Ω → Bornology.IsBounded Ω → ∀ {f h u v : (Fin n → ℝ) → ℝ}, ContDiffOn ℝ 2 u Ω → ContDiffOn ℝ 2 v Ω → ContinuousOn u (closure Ω) → ContinuousOn v (closure Ω) → (∀ x ∈ closure Ω, DifferentiableAt ℝ u x) → (∀ x ∈ closure Ω, DifferentiableAt ℝ v x) → ContinuousOn (fun (x : Fin n → ℝ) => fderiv ℝ u x) (closure Ω) → ContinuousOn (fun (x : Fin n → ℝ) => fderiv ℝ v x) (closure Ω) → IsPoisson u f Ω → IsPoisson v f Ω → (∀ x ∈ frontier Ω, NormalDerivative n u x = h x) → (∀ x ∈ frontier Ω, NormalDerivative n v x = h x) → ∃ (c : ℝ), ∀ x ∈ closure Ω, u x = v x + c) ∧ ∀ {n : ℕ} {Ω : Set (Fin n → ℝ)}, IsOpen Ω → IsConnected Ω → Bornology.IsBounded Ω → ∀ {f : (Fin n → ℝ) → ℝ} {S_D S_N : Set (Fin n → ℝ)}, frontier Ω = S_D ∪ S_N → Disjoint S_D S_N → S_D.Nonempty → ∀ {g_D g_N u v : (Fin n → ℝ) → ℝ}, ContDiffOn ℝ 2 u Ω → ContDiffOn ℝ 2 v Ω → ContinuousOn u (closure Ω) → ContinuousOn v (closure Ω) → (∀ x ∈ closure Ω, DifferentiableAt ℝ u x) → (∀ x ∈ closure Ω, DifferentiableAt ℝ v x) → ContinuousOn (fun (x : Fin n → ℝ) => fderiv ℝ u x) (closure Ω) → ContinuousOn (fun (x : Fin n → ℝ) => fderiv ℝ v x) (closure Ω) → IsPoisson u f Ω → IsPoisson v f Ω → (∀ x ∈ S_D, u x = g_D x) → (∀ x ∈ S_D, v x = g_D x) → (∀ x ∈ S_N, NormalDerivative n u x = g_N x) → (∀ x ∈ S_N, NormalDerivative n v x = g_N x) → ∀ x ∈ closure Ω, u x = v x

Master uniqueness result for Poisson's equation, packaging the four boundary-condition variants: Dirichlet (unique on $\overline{\Omega}$), Robin with $\alpha > 0$ (unique), Neumann (unique up to an additive constant), and mixed Dirichlet/Neumann (unique).