def PoissonHarnack.euclidBall {n : ℕ} (c : Fin n → ℝ) (R : ℝ) : Set (Fin n → ℝ)

The open Euclidean ball $B_R(c) = \{x : \|x - c\| < R\}$ in $\mathbb{R}^n$, using the Euclidean norm CM8.euclidNorm.

noncomputable def PoissonHarnack.kelvinReflection (p : Fin 3 → ℝ) (R : ℝ) (x : Fin 3 → ℝ) : Fin 3 → ℝ

The Kelvin reflection of $x$ across the sphere $\partial B_R(p) \subset \mathbb{R}^3$: $x^* = p + \frac{R^2}{|x-p|^2}(x - p)$. This maps the interior of the ball to its exterior and is used to construct the Green function for a ball.

noncomputable def PoissonHarnack.greenBall (R : ℝ) (p x y : Fin 3 → ℝ) : ℝ

The Green function for the ball $B_R(p) \subset \mathbb{R}^3$ defined via the fundamental solution and its image under Kelvin reflection: $G(x, y) = \Phi_3(x - y) - \frac{R}{|x-p|}\,\Phi_3(x^* - y)$.

theorem PoissonHarnack.kelvinReflection_sub_eq (p x y : Fin 3 → ℝ) (R : ℝ) : kelvinReflection p R x - y = fun (i : Fin 3) => R ^ 2 / CM8.euclidNorm (x - p) ^ 2 * (x i - p i) - (y i - p i)

The componentwise expression for $x^* - y$ where $x^*$ is the Kelvin reflection of $x$.

noncomputable def PoissonHarnack.greenBallFormula (R : ℝ) (p x y : Fin 3 → ℝ) : ℝ

The explicit closed-form expression of greenBall for $x \neq p$: $G(x,y) = -\frac{1}{4\pi|x-y|} + \frac{1}{4\pi}\cdot\frac{R}{|x-p|\,\bigl|\frac{R^2}{|x-p|^2}(x-p)-(y-p)\bigr|}$.

theorem PoissonHarnack.greenBall_eq_explicit_formula (R : ℝ) (p x y : Fin 3 → ℝ) : greenBall R p x y = greenBallFormula R p x y

The Green function greenBall agrees with the explicit closed form greenBallFormula.

noncomputable def PoissonHarnack.greenBallFormula_at_center (R : ℝ) (p y : Fin 3 → ℝ) : ℝ

The value of the Green function for the ball at the center $p$: $G(p, y) = -\frac{1}{4\pi|y-p|} + \frac{1}{4\pi R}$.

def PoissonHarnack.innerProd3 (a b : Fin 3 → ℝ) : ℝ

The standard inner product of two vectors in $\mathbb{R}^3$: $\langle a, b \rangle = \sum_i a_i b_i$.

theorem PoissonHarnack.euclidNorm_sq (v : Fin 3 → ℝ) : CM8.euclidNorm v ^ 2 = PoissonHarnack.normSq✝ v

The square of the Euclidean norm equals the sum of squares: $\|v\|^2 = \sum_i v_i^2$.

theorem PoissonHarnack.normSq_kelvin_sub (p x σ : Fin 3 → ℝ) (R : ℝ) : PoissonHarnack.normSq✝ (kelvinReflection p R x - σ) = PoissonHarnack.normSq✝¹ fun (i : Fin 3) => p i + R ^ 2 / CM8.euclidNorm (x - p) ^ 2 * (x i - p i) - σ i

Rewrite $\|x^* - \sigma\|^2$ in coordinates using the definition of the Kelvin reflection.

theorem PoissonHarnack.normSq_diff_eq (x σ p : Fin 3 → ℝ) : PoissonHarnack.normSq✝ (x - σ) = PoissonHarnack.normSq✝¹ (x - p) - 2 * innerProd3 (x - p) (σ - p) + PoissonHarnack.normSq✝² (σ - p)

Expansion identity: $\|x - \sigma\|^2 = \|x-p\|^2 - 2\langle x-p, \sigma-p\rangle + \|\sigma-p\|^2$.

theorem PoissonHarnack.normSq_kr_expand (p x σ : Fin 3 → ℝ) (c : ℝ) : (PoissonHarnack.normSq✝ fun (i : Fin 3) => p i + c * (x i - p i) - σ i) = c ^ 2 * PoissonHarnack.normSq✝¹ (x - p) - 2 * c * innerProd3 (x - p) (σ - p) + PoissonHarnack.normSq✝² (σ - p)

Quadratic expansion: $\|p + c(x-p) - \sigma\|^2 = c^2\|x-p\|^2 - 2c\langle x-p, \sigma-p\rangle + \|\sigma-p\|^2$.

theorem PoissonHarnack.normSq_product_eq (p x σ : Fin 3 → ℝ) (R : ℝ) (hS : PoissonHarnack.normSq✝ (x - p) ≠ 0) (hσ : PoissonHarnack.normSq✝¹ (σ - p) = R ^ 2) : PoissonHarnack.normSq✝² (kelvinReflection p R x - σ) * PoissonHarnack.normSq✝³ (x - p) = R ^ 2 * PoissonHarnack.normSq✝⁴ (x - σ)

Key identity for the Kelvin reflection across the sphere $|\sigma - p| = R$: $\|x^* - \sigma\|^2 \cdot \|x - p\|^2 = R^2 \cdot \|x - \sigma\|^2$.

theorem PoissonHarnack.norm_product_identity (p x σ : Fin 3 → ℝ) (R : ℝ) (hR : 0 < R) (hxp : 0 < CM8.euclidNorm (x - p)) (hσ : CM8.euclidNorm (σ - p) = R) : CM8.euclidNorm (kelvinReflection p R x - σ) * CM8.euclidNorm (x - p) = R * CM8.euclidNorm (x - σ)

The norm form of the Kelvin reflection identity on the sphere $|\sigma - p| = R$: $\|x^* - \sigma\|\,\|x - p\| = R\,\|x - \sigma\|$.

theorem PoissonHarnack.euclidNorm_zero_imp_eq (a b : Fin 3 → ℝ) (h : CM8.euclidNorm (a - b) = 0) : a = b

If $\|a - b\| = 0$ in $\mathbb{R}^3$, then $a = b$ (positive-definiteness of the Euclidean norm).

theorem PoissonHarnack.greenBall_boundary_vanish (R : ℝ) (hR : 0 < R) (p x σ : Fin 3 → ℝ) (hxp : 0 < CM8.euclidNorm (x - p)) (hx : CM8.euclidNorm (x - p) < R) (hσ : CM8.euclidNorm (σ - p) = R) : greenBall R p x σ = 0

Boundary vanishing of the Green function: for $x \in B_R(p)$ with $x \neq p$ and $\sigma \in \partial B_R(p)$, the Green function $G(x, \sigma) = 0$.

noncomputable def PoissonHarnack.poissonKernel (R : ℝ) (p x y : Fin 3 → ℝ) : ℝ

The Poisson kernel for the ball $B_R(p) \subset \mathbb{R}^3$: $P(x, y) = \frac{R^2 - |x-p|^2}{4\pi R\,|x-y|^3}$. This is the negative outward normal derivative of the Green function on the boundary.

theorem PoissonHarnack.euclidNorm_continuous' {n : ℕ} : Continuous fun (x : Fin n → ℝ) => CM8.euclidNorm x

The Euclidean norm is a continuous function $\mathbb{R}^n \to \mathbb{R}$.

theorem PoissonHarnack.abs_component_le_euclidNorm' {n : ℕ} (x : Fin n → ℝ) (i : Fin n) : |x i| ≤ CM8.euclidNorm x

Each component is bounded by the Euclidean norm: $|x_i| \le \|x\|$.

theorem PoissonHarnack.euclidNorm_smul' {n : ℕ} (c : ℝ) (x : Fin n → ℝ) : CM8.euclidNorm (c • x) = |c| * CM8.euclidNorm x

The Euclidean norm is absolutely homogeneous: $\|c \cdot x\| = |c|\,\|x\|$.

theorem PoissonHarnack.boundary_in_closure' {n : ℕ} (R : ℝ) (hR : 0 < R) (p z : Fin n → ℝ) (heq : CM8.euclidNorm (z - p) = R) : z ∈ closure {w : Fin n → ℝ | CM8.euclidNorm (w - p) < R}

Every point on the sphere $\|z - p\| = R$ lies in the closure of the open ball $\{w : \|w - p\| < R\}$, witnessed by an explicit approximating sequence.

theorem PoissonHarnack.isLipschitzDomain_euclidBall (R : ℝ) (hR : 0 < R) (p : Fin 3 → ℝ) : CM8.IsLipschitzDomain {z : Fin 3 → ℝ | CM8.euclidNorm (z - p) < R}

The open Euclidean ball in $\mathbb{R}^3$ is a Lipschitz domain (in the sense of CM8.IsLipschitzDomain), which permits the application of integration-by-parts results to the ball.

theorem PoissonHarnack.isOpen_euclidBall (R : ℝ) (p : Fin 3 → ℝ) : IsOpen {z : Fin 3 → ℝ | CM8.euclidNorm (z - p) < R}

The open Euclidean ball $\{z : \|z - p\| < R\}$ is an open set.

theorem PoissonHarnack.isBounded_euclidBall (R : ℝ) (hR : 0 < R) (p : Fin 3 → ℝ) : Bornology.IsBounded {z : Fin 3 → ℝ | CM8.euclidNorm (z - p) < R}

The open Euclidean ball is bounded in the sense of Bornology.IsBounded.

theorem PoissonHarnack.frontier_euclidBall_eq (R : ℝ) (hR : 0 < R) (p : Fin 3 → ℝ) : frontier {z : Fin 3 → ℝ | CM8.euclidNorm (z - p) < R} = {z : Fin 3 → ℝ | CM8.euclidNorm (z - p) = R}

The topological frontier of the open Euclidean ball is the sphere: $\partial B_R(p) = \{z : \|z - p\| = R\}$.

theorem PoissonHarnack.fundSolN_continuousOn_frontier_euclidBall (R : ℝ) (hR : 0 < R) (p x : Fin 3 → ℝ) : x ∈ {z : Fin 3 → ℝ | CM8.euclidNorm (z - p) < R} → ContinuousOn (fun (σ : Fin 3 → ℝ) => CM8.FundSolN (x - σ)) (frontier {z : Fin 3 → ℝ | CM8.euclidNorm (z - p) < R})

For every $x$ inside the open ball, the fundamental solution $\sigma \mapsto \Phi(x - \sigma)$ is continuous on the sphere (boundary of the ball), since $x \neq \sigma$ on the boundary.

theorem PoissonHarnack.harmonic_continuousOn_closure_euclidBall (R : ℝ) (hR : 0 < R) (p : Fin 3 → ℝ) (u g : (Fin 3 → ℝ) → ℝ) (hu : CM7.IsHarmonic u {x : Fin 3 → ℝ | CM8.euclidNorm (x - p) < R}) (hu_bdy : ∀ (σ : Fin 3 → ℝ), CM8.euclidNorm (σ - p) = R → u σ = g σ) : ContinuousOn u (closure {z : Fin 3 → ℝ | CM8.euclidNorm (z - p) < R})

A harmonic function on the open ball that matches a boundary datum $g$ on $\partial B_R(p)$ extends continuously to the closed ball.

theorem PoissonHarnack.corrector_contDiffOn_closure_euclidBall (R : ℝ) (hR : 0 < R) (p : Fin 3 → ℝ) (φ : (Fin 3 → ℝ) → (Fin 3 → ℝ) → ℝ) (hφ_c2 : ∀ x ∈ {z : Fin 3 → ℝ | CM8.euclidNorm (z - p) < R}, ContDiffOn ℝ 2 (φ x) {z : Fin 3 → ℝ | CM8.euclidNorm (z - p) < R}) (hφ_harm : ∀ x ∈ {z : Fin 3 → ℝ | CM8.euclidNorm (z - p) < R}, ∀ y ∈ {z : Fin 3 → ℝ | CM8.euclidNorm (z - p) < R}, CM8.laplacian (φ x) y = 0) (x : Fin 3 → ℝ) : x ∈ {z : Fin 3 → ℝ | CM8.euclidNorm (z - p) < R} → ContDiffOn ℝ 2 (φ x) (closure {z : Fin 3 → ℝ | CM8.euclidNorm (z - p) < R})

Interior $C^2$ regularity of the harmonic corrector $\phi$ extends to the closed ball: if $\phi(x, \cdot)$ is $C^2$ and harmonic in the open ball, it is $C^2$ on its closure.

theorem PoissonHarnack.laplacian_compat (u : (Fin 3 → ℝ) → ℝ) (x : Fin 3 → ℝ) : CM7.Laplacian 3 u x = CM8.laplacian u x

Compatibility between the two formulations of the Laplacian in CM7 and CM8: they agree definitionally on the same function.

theorem PoissonHarnack.green_representation_ball3_axiom (R : ℝ) (hR : 0 < R) (p : Fin 3 → ℝ) (g u : (Fin 3 → ℝ) → ℝ) (hu_harmonic : CM7.IsHarmonic u {x : Fin 3 → ℝ | CM8.euclidNorm (x - p) < R}) (hu_bdy : ∀ (σ : Fin 3 → ℝ), CM8.euclidNorm (σ - p) = R → u σ = g σ) (x : Fin 3 → ℝ) (hx : CM8.euclidNorm (x - p) < R) : ∃ (gf : CM8.GreenFunctionN 3 {z : Fin 3 → ℝ | CM8.euclidNorm (z - p) < R}), u x = (-∫ (y : Fin 3 → ℝ) in {z : Fin 3 → ℝ | CM8.euclidNorm (z - p) < R}, 0 * gf.G x y) - CM8.surfaceIntegral {z : Fin 3 → ℝ | CM8.euclidNorm (z - p) < R} fun (σ : Fin 3 → ℝ) => g σ * CM8.normalDeriv {z : Fin 3 → ℝ | CM8.euclidNorm (z - p) < R} (fun (z : Fin 3 → ℝ) => gf.G x z) σ

Green's representation formula specialised to a ball in $\mathbb{R}^3$: any harmonic function $u$ on $B_R(p)$ continuous on the closure can be expressed as a surface integral against the normal derivative of the Green function.

noncomputable def PoissonHarnack.greenBallN_explicit_exists (R : ℝ) (hR : 0 < R) (p : Fin 3 → ℝ) : CM8.GreenFunctionN 3 {z : Fin 3 → ℝ | CM8.euclidNorm (z - p) < R}

Existence of the Green function for the ball: an explicit construction packaged as a CM8.GreenFunctionN 3 structure.

theorem PoissonHarnack.greenFunctionN_ball_unique (R : ℝ) (hR : 0 < R) (p : Fin 3 → ℝ) (gf₁ gf₂ : CM8.GreenFunctionN 3 {z : Fin 3 → ℝ | CM8.euclidNorm (z - p) < R}) (x : Fin 3 → ℝ) (hx : CM8.euclidNorm (x - p) < R) (y : Fin 3 → ℝ) : gf₁.G x y = gf₂.G x y

Uniqueness of the Green function for the ball: any two Green functions for $B_R(p)$ agree at every pair $(x, y)$ with $x$ in the interior.

theorem PoissonHarnack.fderiv_greenBallN_explicit_eq (R : ℝ) (hR : 0 < R) (p x : Fin 3 → ℝ) (hx : CM8.euclidNorm (x - p) < R) (σ : Fin 3 → ℝ) (hσ : CM8.euclidNorm (σ - p) = R) (v : Fin 3 → ℝ) : (fderiv ℝ (fun (z : Fin 3 → ℝ) => (greenBallN_explicit_exists R hR p).G x z) σ) v = -(1 - CM8.euclidNorm (x - p) ^ 2 / R ^ 2) / (4 * Real.pi * CM8.euclidNorm (x - σ) ^ 3) * ∑ i : Fin 3, (σ i - p i) * v i

Formula for the Fréchet derivative of the explicit Green function in the second variable evaluated on the boundary: $D_y G(x, \sigma) \cdot v = -\frac{1 - |x-p|^2/R^2}{4\pi |x-\sigma|^3} \sum_i (\sigma_i - p_i) v_i$.

theorem PoissonHarnack.fderiv_greenFunctionN_ball_eq (R : ℝ) (hR : 0 < R) (p x : Fin 3 → ℝ) (hx : CM8.euclidNorm (x - p) < R) (gf : CM8.GreenFunctionN 3 {z : Fin 3 → ℝ | CM8.euclidNorm (z - p) < R}) (σ : Fin 3 → ℝ) (hσ : CM8.euclidNorm (σ - p) = R) (v : Fin 3 → ℝ) : (fderiv ℝ (fun (z : Fin 3 → ℝ) => gf.G x z) σ) v = -(1 - CM8.euclidNorm (x - p) ^ 2 / R ^ 2) / (4 * Real.pi * CM8.euclidNorm (x - σ) ^ 3) * ∑ i : Fin 3, (σ i - p i) * v i

Formula for the Fréchet derivative on the boundary for any Green function on the ball (follows from uniqueness).

theorem PoissonHarnack.normalDeriv_greenFunctionN_ball_eq_neg_poisson (R : ℝ) (hR : 0 < R) (p x : Fin 3 → ℝ) (hx : CM8.euclidNorm (x - p) < R) (gf : CM8.GreenFunctionN 3 {z : Fin 3 → ℝ | CM8.euclidNorm (z - p) < R}) (σ : Fin 3 → ℝ) (hσ : σ ∈ frontier {z : Fin 3 → ℝ | CM8.euclidNorm (z - p) < R}) : CM8.normalDeriv {z : Fin 3 → ℝ | CM8.euclidNorm (z - p) < R} (fun (z : Fin 3 → ℝ) => gf.G x z) σ = -poissonKernel R p x σ

The outward normal derivative of the Green function on the boundary of the ball equals the negative of the Poisson kernel: $\partial_{\hat N} G(x, \sigma) = -P(x, \sigma)$.

theorem PoissonHarnack.surfaceIntegral_ball_eq_sphere {n : ℕ} (R : ℝ) (hR : 0 < R) (p : Fin n → ℝ) (f : (Fin n → ℝ) → ℝ) : CM8.surfaceIntegral {z : Fin n → ℝ | CM8.euclidNorm (z - p) < R} f = CM8.surfaceIntegral {y : Fin n → ℝ | CM8.euclidNorm (y - p) = R} f

The surface integral over the frontier of the open ball equals the surface integral over the sphere $\|y - p\| = R$.

theorem PoissonHarnack.surfaceIntegral_normalDeriv_greenBall3_eq (R : ℝ) (hR : 0 < R) (p : Fin 3 → ℝ) (g : (Fin 3 → ℝ) → ℝ) (x : Fin 3 → ℝ) (hx : CM8.euclidNorm (x - p) < R) (gf : CM8.GreenFunctionN 3 {z : Fin 3 → ℝ | CM8.euclidNorm (z - p) < R}) : (CM8.surfaceIntegral {z : Fin 3 → ℝ | CM8.euclidNorm (z - p) < R} fun (σ : Fin 3 → ℝ) => g σ * CM8.normalDeriv {z : Fin 3 → ℝ | CM8.euclidNorm (z - p) < R} (fun (z : Fin 3 → ℝ) => gf.G x z) σ) = -CM8.surfaceIntegral {y : Fin 3 → ℝ | CM8.euclidNorm (y - p) = R} fun (σ : Fin 3 → ℝ) => poissonKernel R p x σ * g σ

Surface integral of $g \cdot \partial_{\hat N} G$ on the sphere equals the negative of the surface integral of $P(x, \sigma) g(\sigma)$, using $\partial_{\hat N} G(x, \sigma) = -P(x, \sigma)$.

theorem PoissonHarnack.poisson_formula_axiom (R : ℝ) (hR : 0 < R) (p : Fin 3 → ℝ) (g u : (Fin 3 → ℝ) → ℝ) (hu_harmonic : CM7.IsHarmonic u {x : Fin 3 → ℝ | CM8.euclidNorm (x - p) < R}) (hu_bdy : ∀ (σ : Fin 3 → ℝ), CM8.euclidNorm (σ - p) = R → u σ = g σ) (x : Fin 3 → ℝ) (hx : CM8.euclidNorm (x - p) < R) : u x = CM8.surfaceIntegral {y : Fin 3 → ℝ | CM8.euclidNorm (y - p) = R} fun (σ : Fin 3 → ℝ) => poissonKernel R p x σ * g σ

Auxiliary form of Poisson's formula (Theorem 3.1 in IPDE) combining Green's representation with the boundary-vanishing properties: for a harmonic $u$ on $B_R(p) \subset \mathbb{R}^3$ with boundary data $g$, $u(x) = \int_{\partial B_R(p)} P(x, \sigma) g(\sigma)\, d\sigma$.

theorem PoissonHarnack.poisson_formula (R : ℝ) (hR : 0 < R) (p : Fin 3 → ℝ) (g u : (Fin 3 → ℝ) → ℝ) (hu_harmonic : CM7.IsHarmonic u {x : Fin 3 → ℝ | CM8.euclidNorm (x - p) < R}) (hu_bdy : ∀ (σ : Fin 3 → ℝ), CM8.euclidNorm (σ - p) = R → u σ = g σ) (x : Fin 3 → ℝ) (hx : CM8.euclidNorm (x - p) < R) : u x = CM8.surfaceIntegral {y : Fin 3 → ℝ | CM8.euclidNorm (y - p) = R} fun (σ : Fin 3 → ℝ) => poissonKernel R p x σ * g σ

Theorem 3.1 (Poisson's formula). Let $u$ be harmonic on $B_R(p) \subset \mathbb{R}^3$ with continuous boundary values $u(\sigma) = f(\sigma)$ on $\partial B_R(p)$. Then for any $x \in B_R(p)$, $u(x) = \frac{R^2 - |x-p|^2}{4\pi R} \int_{\partial B_R(p)} \frac{f(\sigma)}{|x-\sigma|^3}\, d\sigma$.

theorem PoissonHarnack.greenBall_at_center (R : ℝ) (hR : 0 < R) (p y : Fin 3 → ℝ) (hy : CM8.euclidNorm (y - p) = R) : Filter.Tendsto (fun (x : Fin 3 → ℝ) => greenBall R p x y) (nhdsWithin p {x : Fin 3 → ℝ | 0 < CM8.euclidNorm (x - p)}) (nhds (-1 / (4 * Real.pi * CM8.euclidNorm (y - p)) + 1 / (4 * Real.pi * R)))

Limit at the center: as $x \to p$ with $x \neq p$, $G(x, y)$ tends to $-\frac{1}{4\pi|y - p|} + \frac{1}{4\pi R}$ for $y$ on the boundary. (This value is $0$ since $|y - p| = R$.)

theorem PoissonHarnack.greenBall_at_center_eq_formula (R : ℝ) (hR : 0 < R) (p y : Fin 3 → ℝ) (hy : CM8.euclidNorm (y - p) = R) : Filter.Tendsto (fun (x : Fin 3 → ℝ) => greenBall R p x y) (nhdsWithin p {x : Fin 3 → ℝ | 0 < CM8.euclidNorm (x - p)}) (nhds (greenBallFormula_at_center R p y))

Restatement of greenBall_at_center in terms of greenBallFormula_at_center.

theorem PoissonHarnack.outwardUnitNormal_ball_spec (R : ℝ) (hR : 0 < R) (p σ : Fin 3 → ℝ) (hσ : CM8.euclidNorm (σ - p) = R) : CM8.outwardUnitNormal {y : Fin 3 → ℝ | CM8.euclidNorm (y - p) < R} σ = fun (i : Fin 3) => (σ i - p i) / R

The outward unit normal on the sphere $\|σ - p\| = R$ is the radial direction $\hat N(\sigma) = (\sigma - p) / R$.

theorem PoissonHarnack.outwardUnitNormal_euclidBall (R : ℝ) (hR : 0 < R) (p σ : Fin 3 → ℝ) (hσ : CM8.euclidNorm (σ - p) = R) : CM8.outwardUnitNormal {y : Fin 3 → ℝ | CM8.euclidNorm (y - p) < R} σ = fun (i : Fin 3) => (σ i - p i) / R

Alias for outwardUnitNormal_ball_spec: the outward unit normal on the sphere is $(\sigma - p) / R$.

def PoissonHarnack.normSq3' (y : Fin 3 → ℝ) : ℝ

Squared Euclidean norm in $\mathbb{R}^3$ as a function: $y \mapsto \sum_j y_j^2$.

noncomputable def PoissonHarnack.normSq3_CLM' (x : Fin 3 → ℝ) : (Fin 3 → ℝ) →L[ℝ] ℝ

Fréchet derivative of normSq3' at $x$ packaged as a continuous linear map: $v \mapsto \sum_j 2 x_j v_j = 2\langle x, v\rangle$.

theorem PoissonHarnack.normSq3_pos' (x : Fin 3 → ℝ) (hx : CM8.euclidNorm x ≠ 0) : 0 < normSq3' x

The squared norm is strictly positive when the underlying vector is nonzero.

theorem PoissonHarnack.hasFDerivAt_normSq3' (x : Fin 3 → ℝ) : HasFDerivAt normSq3' (normSq3_CLM' x) x

normSq3' has Fréchet derivative normSq3_CLM' x at every point $x \in \mathbb{R}^3$.

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

Derivative computation: $\frac{d}{ds}\left[-\frac{1}{4\pi\sqrt s}\right] = \frac{1}{8\pi(\sqrt s)^3}$.

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

Fréchet derivative of the fundamental solution $\Phi_3$ in $\mathbb{R}^3$ at $y \neq 0$.

theorem PoissonHarnack.hasFDerivAt_const_sub_fin3 (a y : Fin 3 → ℝ) : HasFDerivAt (fun (y' : Fin 3 → ℝ) => a - y') (-ContinuousLinearMap.id ℝ (Fin 3 → ℝ)) y

The map $y' \mapsto a - y'$ has Fréchet derivative $-\mathrm{id}$ at every point.

theorem PoissonHarnack.hasFDerivAt_Phi3_sub_chain (a y : Fin 3 → ℝ) (ha : CM8.euclidNorm (a - y) ≠ 0) : HasFDerivAt (fun (y' : Fin 3 → ℝ) => CM8.Phi3 (a - y')) (((1 / (8 * Real.pi * CM8.euclidNorm (a - y) ^ 3)) • normSq3_CLM' (a - y)).comp (-ContinuousLinearMap.id ℝ (Fin 3 → ℝ))) y

Chain rule: $\frac{d}{dy'}\Phi_3(a - y')$ at $y$ for $a \neq y$.

theorem PoissonHarnack.normSq3_CLM_apply' (x v : Fin 3 → ℝ) : (normSq3_CLM' x) v = ∑ j : Fin 3, 2 * x j * v j

Explicit action of normSq3_CLM' x on a vector $v$: $\sum_j 2 x_j v_j$.

theorem PoissonHarnack.fderiv_Phi3_sub_eq (a y : Fin 3 → ℝ) (ha : CM8.euclidNorm (a - y) ≠ 0) (v : Fin 3 → ℝ) : (fderiv ℝ (fun (y' : Fin 3 → ℝ) => CM8.Phi3 (a - y')) y) v = -((∑ i : Fin 3, (a i - y i) * v i) / (4 * Real.pi * CM8.euclidNorm (a - y) ^ 3))

Explicit formula for the Fréchet derivative of $y' \mapsto \Phi_3(a - y')$ at $y$, applied to a direction $v$: $D\Phi_3(a - \cdot)(y)(v) = -\frac{\langle a - y, v\rangle}{4\pi |a - y|^3}$.

theorem PoissonHarnack.differentiableAt_Phi3_sub (a y : Fin 3 → ℝ) (ha : CM8.euclidNorm (a - y) ≠ 0) : DifferentiableAt ℝ (fun (y' : Fin 3 → ℝ) => CM8.Phi3 (a - y')) y

$y' \mapsto \Phi_3(a - y')$ is differentiable at $y$ when $a \neq y$.

theorem PoissonHarnack.fderiv_greenBall_decompose (R : ℝ) (hR : 0 < R) (p x : Fin 3 → ℝ) (hx : CM8.euclidNorm (x - p) < R) (hxp : 0 < CM8.euclidNorm (x - p)) (σ : Fin 3 → ℝ) (hσ : CM8.euclidNorm (σ - p) = R) (v : Fin 3 → ℝ) : (fderiv ℝ (fun (y : Fin 3 → ℝ) => greenBall R p x y) σ) v = (fderiv ℝ (fun (y : Fin 3 → ℝ) => CM8.Phi3 (x - y)) σ) v - R / CM8.euclidNorm (x - p) * (fderiv ℝ (fun (y : Fin 3 → ℝ) => CM8.Phi3 (kelvinReflection p R x - y)) σ) v

Linearity decomposition of the Fréchet derivative of greenBall in the boundary variable: $D_y G(x, \sigma) v = D_y \Phi_3(x - \sigma) v - \frac{R}{|x-p|} D_y \Phi_3(x^* - \sigma) v$.

theorem PoissonHarnack.fderiv_greenBall_eq (R : ℝ) (hR : 0 < R) (p x : Fin 3 → ℝ) (hx : CM8.euclidNorm (x - p) < R) (hxp : 0 < CM8.euclidNorm (x - p)) (σ : Fin 3 → ℝ) (hσ : CM8.euclidNorm (σ - p) = R) (v : Fin 3 → ℝ) : (fderiv ℝ (fun (y : Fin 3 → ℝ) => greenBall R p x y) σ) v = (1 - CM8.euclidNorm (x - p) ^ 2 / R ^ 2) / (4 * Real.pi * CM8.euclidNorm (x - σ) ^ 3) * ∑ i : Fin 3, (σ i - p i) * v i

Explicit formula for the Fréchet derivative of greenBall in the boundary variable: $D_y G(x, \sigma) v = \frac{1 - |x-p|^2/R^2}{4\pi |x - \sigma|^3} \sum_i (\sigma_i - p_i) v_i$.

theorem PoissonHarnack.greenBall_normal_deriv_eq_poisson (R : ℝ) (hR : 0 < R) (p x : Fin 3 → ℝ) (hx : CM8.euclidNorm (x - p) < R) (hxp : 0 < CM8.euclidNorm (x - p)) (σ : Fin 3 → ℝ) (hσ : CM8.euclidNorm (σ - p) = R) : CM8.normalDeriv {y : Fin 3 → ℝ | CM8.euclidNorm (y - p) < R} (fun (y : Fin 3 → ℝ) => greenBall R p x y) σ = poissonKernel R p x σ

The outward normal derivative of the explicit greenBall on the sphere equals the Poisson kernel: $\partial_{\hat N(\sigma)} G(x, \sigma) = \frac{R^2 - |x-p|^2}{4\pi R\, |x-\sigma|^3}$.

theorem PoissonHarnack.lemma_2_0_1_green_ball (R : ℝ) (hR : 0 < R) (p x : Fin 3 → ℝ) (hx : CM8.euclidNorm (x - p) < R) (hxp : 0 < CM8.euclidNorm (x - p)) (σ : Fin 3 → ℝ) (hσ : CM8.euclidNorm (σ - p) = R) : greenBall R p x σ = greenBallFormula R p x σ ∧ greenBall R p x σ = 0 ∧ Filter.Tendsto (fun (z : Fin 3 → ℝ) => greenBall R p z σ) (nhdsWithin p {z : Fin 3 → ℝ | 0 < CM8.euclidNorm (z - p)}) (nhds (greenBallFormula_at_center R p σ)) ∧ CM8.normalDeriv {y : Fin 3 → ℝ | CM8.euclidNorm (y - p) < R} (fun (y : Fin 3 → ℝ) => greenBall R p x y) σ = poissonKernel R p x σ

Lemma 2.0.1 (Green function for the ball). Combined statement of the four characterising properties of the Green function for a ball $B_R(p) \subset \mathbb{R}^3$: (i) the explicit closed-form formula; (ii) boundary vanishing $G(x, \sigma) = 0$ for $\sigma \in \partial B_R(p)$; (iii) the value at the center; (iv) the normal derivative on the boundary equals the Poisson kernel.

def PoissonHarnack.toPiLp {n : ℕ} (v : Fin n → ℝ) : PiLp 2 fun (x : Fin n) => ℝ

The natural identification of a tuple $v : \mathrm{Fin}\,n \to \mathbb{R}$ with an element of the $\ell^2$ norm space PiLp 2 (fun _ => ℝ).

theorem PoissonHarnack.euclidNorm_eq_piLp_norm {n : ℕ} (v : Fin n → ℝ) : CM8.euclidNorm v = ‖toPiLp v‖

The Euclidean norm agrees with the canonical $\ell^2$ norm on PiLp 2.

theorem PoissonHarnack.euclidNorm_sub_le {n : ℕ} (a b : Fin n → ℝ) : CM8.euclidNorm (a - b) ≤ CM8.euclidNorm a + CM8.euclidNorm b

Triangle inequality for the Euclidean norm: $\|a - b\| \le \|a\| + \|b\|$.

theorem PoissonHarnack.euclidNorm_reverse_triangle {n : ℕ} (x σ : Fin n → ℝ) : CM8.euclidNorm σ - CM8.euclidNorm x ≤ CM8.euclidNorm (x - σ)

Reverse triangle inequality: $\|\sigma\| - \|x\| \le \|x - \sigma\|$.

theorem PoissonHarnack.distance_upper_bound_on_sphere {n : ℕ} (x σ : Fin n → ℝ) (R : ℝ) (hσ : CM8.euclidNorm σ = R) : CM8.euclidNorm (x - σ) ≤ R + CM8.euclidNorm x

Upper bound for the distance from $x$ to a point on the sphere of radius $R$: $\|x - \sigma\| \le R + \|x\|$.

theorem PoissonHarnack.distance_lower_bound_on_sphere {n : ℕ} (x σ : Fin n → ℝ) (R : ℝ) (hσ : CM8.euclidNorm σ = R) : R - CM8.euclidNorm x ≤ CM8.euclidNorm (x - σ)

Lower bound for the distance from $x$ to a point on the sphere of radius $R$: $R - \|x\| \le \|x - \sigma\|$.

theorem PoissonHarnack.poisson_representation_weight_axiom {n : ℕ} (u : (Fin n → ℝ) → ℝ) (R : ℝ) (hR : 0 < R) (_hu_harmonic : CM7.IsHarmonic u (euclidBall 0 R)) (hu_nonneg : ∀ x ∈ euclidBall 0 R, 0 ≤ u x) (x : Fin n → ℝ) (hx : x ∈ euclidBall 0 R) : ∃ (W : ℝ), 0 ≤ W ∧ u x = (R ^ 2 - CM8.euclidNorm x ^ 2) * W

For a non-negative harmonic function $u$ on $B_R(0)$, there exists a non-negative weight $W \ge 0$ such that $u(x) = (R^2 - |x|^2) W$. This packages the positivity of $u(x)$ and the positivity of $R^2 - |x|^2$ inside the ball.

theorem PoissonHarnack.poisson_integral_lower_bound_primitive {n : ℕ} (u : (Fin n → ℝ) → ℝ) (R : ℝ) (hR : 0 < R) (hu_harmonic : CM7.IsHarmonic u (euclidBall 0 R)) (hu_nonneg : ∀ x ∈ euclidBall 0 R, 0 ≤ u x) (x : Fin n → ℝ) (hx : x ∈ euclidBall 0 R) (d : ℝ) (hd : 0 < d) (hd_bound : ∀ (σ : Fin n → ℝ), CM8.euclidNorm σ = R → CM8.euclidNorm (x - σ) ≤ d) : R ^ (n - 2) * (R ^ 2 - CM8.euclidNorm x ^ 2) / d ^ n * u 0 ≤ u x

Primitive lower bound: given a uniform upper bound $\|x - \sigma\| \le d$ for $\sigma$ on the sphere, we have $\frac{R^{n-2}(R^2 - |x|^2)}{d^n}\, u(0) \le u(x)$. This bound is the starting point of the Harnack inequality argument.

theorem PoissonHarnack.poisson_weight_lower_bound_from_surface_monotonicity_MVP_helper {n : ℕ} (u : (Fin n → ℝ) → ℝ) (R : ℝ) (hR : 0 < R) (hu_harmonic : CM7.IsHarmonic u (euclidBall 0 R)) (hu_nonneg : ∀ x ∈ euclidBall 0 R, 0 ≤ u x) (x : Fin n → ℝ) (hx : x ∈ euclidBall 0 R) (W : ℝ) (hW_nn : 0 ≤ W) (hW_eq : u x = (R ^ 2 - CM8.euclidNorm x ^ 2) * W) (d : ℝ) (hd : 0 < d) (hd_bound : ∀ (σ : Fin n → ℝ), CM8.euclidNorm σ = R → CM8.euclidNorm (x - σ) ≤ d) : R ^ (n - 2) * u 0 / d ^ n ≤ W

Helper deriving a lower bound on the Poisson weight $W$ from poisson_integral_lower_bound_primitive and the representation $u(x) = (R^2-|x|^2) W$.

theorem PoissonHarnack.poisson_integral_lower_bound_from_surface_monotonicity_MVP {n : ℕ} (u : (Fin n → ℝ) → ℝ) (R : ℝ) (hR : 0 < R) (hu_harmonic : CM7.IsHarmonic u (euclidBall 0 R)) (hu_nonneg : ∀ x ∈ euclidBall 0 R, 0 ≤ u x) (x : Fin n → ℝ) (hx : x ∈ euclidBall 0 R) (d : ℝ) (hd : 0 < d) (hd_bound : ∀ (σ : Fin n → ℝ), CM8.euclidNorm σ = R → CM8.euclidNorm (x - σ) ≤ d) : R ^ (n - 2) * (R ^ 2 - CM8.euclidNorm x ^ 2) / d ^ n * u 0 ≤ u x

Mean-value type lower bound: $\frac{R^{n-2}(R^2 - |x|^2)}{d^n}\, u(0) \le u(x)$ when $\|x - \sigma\| \le d$ for all $\sigma$ on the sphere.

theorem PoissonHarnack.poisson_weight_lower_bound_kernel_MVP_axiom {n : ℕ} (u : (Fin n → ℝ) → ℝ) (R : ℝ) (hR : 0 < R) (hu_harmonic : CM7.IsHarmonic u (euclidBall 0 R)) (hu_nonneg : ∀ x ∈ euclidBall 0 R, 0 ≤ u x) (x : Fin n → ℝ) (hx : x ∈ euclidBall 0 R) (W : ℝ) (_hW_nn : 0 ≤ W) (hW_eq : u x = (R ^ 2 - CM8.euclidNorm x ^ 2) * W) (d : ℝ) (hd : 0 < d) (hd_bound : ∀ (σ : Fin n → ℝ), CM8.euclidNorm σ = R → CM8.euclidNorm (x - σ) ≤ d) : R ^ (n - 2) * u 0 / d ^ n ≤ W

Variant of poisson_weight_lower_bound_from_surface_monotonicity_MVP_helper: the same lower bound $R^{n-2}u(0)/d^n \le W$ on the Poisson weight.

theorem PoissonHarnack.poisson_integral_lower_bound_fundamental {n : ℕ} (u : (Fin n → ℝ) → ℝ) (R : ℝ) (hR : 0 < R) (hu_harmonic : CM7.IsHarmonic u (euclidBall 0 R)) (hu_nonneg : ∀ x ∈ euclidBall 0 R, 0 ≤ u x) (x : Fin n → ℝ) (hx : x ∈ euclidBall 0 R) (d : ℝ) (hd : 0 < d) (hd_bound : ∀ (σ : Fin n → ℝ), CM8.euclidNorm σ = R → CM8.euclidNorm (x - σ) ≤ d) : R ^ (n - 2) * (R ^ 2 - CM8.euclidNorm x ^ 2) / d ^ n * u 0 ≤ u x

Fundamental form of the Poisson integral lower bound derived from the weight bound.

theorem PoissonHarnack.poisson_integral_lower_bound_core_helper {n : ℕ} (u : (Fin n → ℝ) → ℝ) (R : ℝ) (hR : 0 < R) (hu_harmonic : CM7.IsHarmonic u (euclidBall 0 R)) (hu_nonneg : ∀ x ∈ euclidBall 0 R, 0 ≤ u x) (x : Fin n → ℝ) (hx : x ∈ euclidBall 0 R) (d : ℝ) (hd : 0 < d) (hd_bound : ∀ (σ : Fin n → ℝ), CM8.euclidNorm σ = R → CM8.euclidNorm (x - σ) ≤ d) : R ^ (n - 2) * (R ^ 2 - CM8.euclidNorm x ^ 2) / d ^ n * u 0 ≤ u x

Core helper specialisation of the Poisson integral lower bound.

theorem PoissonHarnack.poisson_weight_lower_bound_core {n : ℕ} (u : (Fin n → ℝ) → ℝ) (R : ℝ) (hR : 0 < R) (hu_harmonic : CM7.IsHarmonic u (euclidBall 0 R)) (hu_nonneg : ∀ x ∈ euclidBall 0 R, 0 ≤ u x) (x : Fin n → ℝ) (hx : x ∈ euclidBall 0 R) (W : ℝ) (hW_eq : u x = (R ^ 2 - CM8.euclidNorm x ^ 2) * W) (_hW_nn : 0 ≤ W) (d : ℝ) (hd : 0 < d) (hd_bound : ∀ (σ : Fin n → ℝ), CM8.euclidNorm σ = R → CM8.euclidNorm (x - σ) ≤ d) : R ^ (n - 2) * u 0 / d ^ n ≤ W

Core lower bound on the Poisson weight $W$ given $\|x - \sigma\| \le d$ on the sphere.

theorem PoissonHarnack.poisson_integral_lower_bound_surface_monotonicity_MVP_core {n : ℕ} (u : (Fin n → ℝ) → ℝ) (R : ℝ) (hR : 0 < R) (hu_harmonic : CM7.IsHarmonic u (euclidBall 0 R)) (hu_nonneg : ∀ x ∈ euclidBall 0 R, 0 ≤ u x) (x : Fin n → ℝ) (hx : x ∈ euclidBall 0 R) (d : ℝ) (hd : 0 < d) (hd_bound : ∀ (σ : Fin n → ℝ), CM8.euclidNorm σ = R → CM8.euclidNorm (x - σ) ≤ d) : R ^ (n - 2) * (R ^ 2 - CM8.euclidNorm x ^ 2) / d ^ n * u 0 ≤ u x

Core version of the Poisson integral lower bound combining the weight bound and the representation $u(x) = (R^2 - |x|^2) W$.

theorem PoissonHarnack.poisson_weight_lower_bound_surface_monotonicity_MVP_direct {n : ℕ} (u : (Fin n → ℝ) → ℝ) (R : ℝ) (hR : 0 < R) (hu_harmonic : CM7.IsHarmonic u (euclidBall 0 R)) (hu_nonneg : ∀ x ∈ euclidBall 0 R, 0 ≤ u x) (x : Fin n → ℝ) (hx : x ∈ euclidBall 0 R) (W : ℝ) (hW_eq : u x = (R ^ 2 - CM8.euclidNorm x ^ 2) * W) (_hW_nn : 0 ≤ W) (d : ℝ) (hd : 0 < d) (hd_bound : ∀ (σ : Fin n → ℝ), CM8.euclidNorm σ = R → CM8.euclidNorm (x - σ) ≤ d) : R ^ (n - 2) * u 0 / d ^ n ≤ W

Direct version of the Poisson weight lower bound: $R^{n-2} u(0) / d^n \le W$.

theorem PoissonHarnack.poisson_integral_lower_bound_surface_monotonicity_MVP {n : ℕ} (u : (Fin n → ℝ) → ℝ) (R : ℝ) (hR : 0 < R) (hu_harmonic : CM7.IsHarmonic u (euclidBall 0 R)) (hu_nonneg : ∀ x ∈ euclidBall 0 R, 0 ≤ u x) (x : Fin n → ℝ) (hx : x ∈ euclidBall 0 R) (d : ℝ) (hd : 0 < d) (hd_bound : ∀ (σ : Fin n → ℝ), CM8.euclidNorm σ = R → CM8.euclidNorm (x - σ) ≤ d) : R ^ (n - 2) * (R ^ 2 - CM8.euclidNorm x ^ 2) / d ^ n * u 0 ≤ u x

Mean-value type lower bound for the Poisson integral derived from surface monotonicity.

theorem PoissonHarnack.poisson_weight_bound_from_surface_integral_MVP_lower {n : ℕ} (u : (Fin n → ℝ) → ℝ) (R : ℝ) (hR : 0 < R) (hu_harmonic : CM7.IsHarmonic u (euclidBall 0 R)) (hu_nonneg : ∀ x ∈ euclidBall 0 R, 0 ≤ u x) (x : Fin n → ℝ) (hx : x ∈ euclidBall 0 R) (W : ℝ) (hW_eq : u x = (R ^ 2 - CM8.euclidNorm x ^ 2) * W) (_hW_nn : 0 ≤ W) (d : ℝ) (hd : 0 < d) (hd_bound : ∀ (σ : Fin n → ℝ), CM8.euclidNorm σ = R → CM8.euclidNorm (x - σ) ≤ d) : R ^ (n - 2) * u 0 / d ^ n ≤ W

Alias for poisson_weight_lower_bound_surface_monotonicity_MVP_direct, expressing the lower bound $R^{n-2} u(0) / d^n \le W$.

theorem PoissonHarnack.poisson_formula_monotonicity_MVP_lower {n : ℕ} (u : (Fin n → ℝ) → ℝ) (R : ℝ) (hR : 0 < R) (hu_harmonic : CM7.IsHarmonic u (euclidBall 0 R)) (hu_nonneg : ∀ x ∈ euclidBall 0 R, 0 ≤ u x) (x : Fin n → ℝ) (hx : x ∈ euclidBall 0 R) (d : ℝ) (hd : 0 < d) (hd_bound : ∀ (σ : Fin n → ℝ), CM8.euclidNorm σ = R → CM8.euclidNorm (x - σ) ≤ d) : R ^ (n - 2) * (R ^ 2 - CM8.euclidNorm x ^ 2) / d ^ n * u 0 ≤ u x

Poisson-formula style lower bound consequence: $\frac{R^{n-2}(R^2 - |x|^2)}{d^n} u(0) \le u(x)$ when $\|x - \sigma\| \le d$.

theorem PoissonHarnack.poisson_weight_upper_bound_from_surface_monotonicity_MVP_helper {n : ℕ} (u : (Fin n → ℝ) → ℝ) (R : ℝ) (hR : 0 < R) (hu_harmonic : CM7.IsHarmonic u (euclidBall 0 R)) (hu_nonneg : ∀ x ∈ euclidBall 0 R, 0 ≤ u x) (x : Fin n → ℝ) (hx : x ∈ euclidBall 0 R) (W : ℝ) (hW_nn : 0 ≤ W) (hW_eq : u x = (R ^ 2 - CM8.euclidNorm x ^ 2) * W) (d : ℝ) (hd : 0 < d) (hd_bound : ∀ (σ : Fin n → ℝ), CM8.euclidNorm σ = R → d ≤ CM8.euclidNorm (x - σ)) : W ≤ R ^ (n - 2) * u 0 / d ^ n

Upper-bound counterpart: if $d \le \|x - \sigma\|$ for all $\sigma$ on the sphere, then $W \le R^{n-2} u(0) / d^n$.

theorem PoissonHarnack.poisson_integral_upper_bound_from_surface_monotonicity_MVP {n : ℕ} (u : (Fin n → ℝ) → ℝ) (R : ℝ) (hR : 0 < R) (hu_harmonic : CM7.IsHarmonic u (euclidBall 0 R)) (hu_nonneg : ∀ x ∈ euclidBall 0 R, 0 ≤ u x) (x : Fin n → ℝ) (hx : x ∈ euclidBall 0 R) (d : ℝ) (hd : 0 < d) (hd_bound : ∀ (σ : Fin n → ℝ), CM8.euclidNorm σ = R → d ≤ CM8.euclidNorm (x - σ)) : u x ≤ R ^ (n - 2) * (R ^ 2 - CM8.euclidNorm x ^ 2) / d ^ n * u 0

Upper bound: $u(x) \le \frac{R^{n-2}(R^2 - |x|^2)}{d^n} u(0)$ when $d \le \|x - \sigma\|$ on the sphere.

theorem PoissonHarnack.poisson_weight_upper_bound_fundamental {n : ℕ} (u : (Fin n → ℝ) → ℝ) (R : ℝ) (hR : 0 < R) (hu_harmonic : CM7.IsHarmonic u (euclidBall 0 R)) (hu_nonneg : ∀ x ∈ euclidBall 0 R, 0 ≤ u x) (x : Fin n → ℝ) (hx : x ∈ euclidBall 0 R) (W : ℝ) (hW_eq : u x = (R ^ 2 - CM8.euclidNorm x ^ 2) * W) (d : ℝ) (hd : 0 < d) (hd_bound : ∀ (σ : Fin n → ℝ), CM8.euclidNorm σ = R → d ≤ CM8.euclidNorm (x - σ)) : W ≤ R ^ (n - 2) * u 0 / d ^ n

Fundamental upper bound on the Poisson weight derived from poisson_integral_upper_bound_from_surface_monotonicity_MVP.

theorem PoissonHarnack.poisson_integral_upper_bound_fundamental {n : ℕ} (u : (Fin n → ℝ) → ℝ) (R : ℝ) (hR : 0 < R) (hu_harmonic : CM7.IsHarmonic u (euclidBall 0 R)) (hu_nonneg : ∀ x ∈ euclidBall 0 R, 0 ≤ u x) (x : Fin n → ℝ) (hx : x ∈ euclidBall 0 R) (d : ℝ) (hd : 0 < d) (hd_bound : ∀ (σ : Fin n → ℝ), CM8.euclidNorm σ = R → d ≤ CM8.euclidNorm (x - σ)) : u x ≤ R ^ (n - 2) * (R ^ 2 - CM8.euclidNorm x ^ 2) / d ^ n * u 0

Fundamental upper bound: $u(x) \le \frac{R^{n-2}(R^2 - |x|^2)}{d^n} u(0)$.

theorem PoissonHarnack.poisson_integral_upper_bound_core_helper {n : ℕ} (u : (Fin n → ℝ) → ℝ) (R : ℝ) (hR : 0 < R) (hu_harmonic : CM7.IsHarmonic u (euclidBall 0 R)) (hu_nonneg : ∀ x ∈ euclidBall 0 R, 0 ≤ u x) (x : Fin n → ℝ) (hx : x ∈ euclidBall 0 R) (d : ℝ) (hd : 0 < d) (hd_bound : ∀ (σ : Fin n → ℝ), CM8.euclidNorm σ = R → d ≤ CM8.euclidNorm (x - σ)) : u x ≤ R ^ (n - 2) * (R ^ 2 - CM8.euclidNorm x ^ 2) / d ^ n * u 0

Core helper specialisation of the Poisson integral upper bound.

theorem PoissonHarnack.poisson_weight_upper_bound_core {n : ℕ} (u : (Fin n → ℝ) → ℝ) (R : ℝ) (hR : 0 < R) (hu_harmonic : CM7.IsHarmonic u (euclidBall 0 R)) (hu_nonneg : ∀ x ∈ euclidBall 0 R, 0 ≤ u x) (x : Fin n → ℝ) (hx : x ∈ euclidBall 0 R) (W : ℝ) (hW_eq : u x = (R ^ 2 - CM8.euclidNorm x ^ 2) * W) (_hW_nn : 0 ≤ W) (d : ℝ) (hd : 0 < d) (hd_bound : ∀ (σ : Fin n → ℝ), CM8.euclidNorm σ = R → d ≤ CM8.euclidNorm (x - σ)) : W ≤ R ^ (n - 2) * u 0 / d ^ n

Core upper bound on the Poisson weight $W \le R^{n-2} u(0) / d^n$.

theorem PoissonHarnack.poisson_integral_upper_bound_surface_monotonicity_MVP_core {n : ℕ} (u : (Fin n → ℝ) → ℝ) (R : ℝ) (hR : 0 < R) (hu_harmonic : CM7.IsHarmonic u (euclidBall 0 R)) (hu_nonneg : ∀ x ∈ euclidBall 0 R, 0 ≤ u x) (x : Fin n → ℝ) (hx : x ∈ euclidBall 0 R) (d : ℝ) (hd : 0 < d) (hd_bound : ∀ (σ : Fin n → ℝ), CM8.euclidNorm σ = R → d ≤ CM8.euclidNorm (x - σ)) : u x ≤ R ^ (n - 2) * (R ^ 2 - CM8.euclidNorm x ^ 2) / d ^ n * u 0

Core MVP-style version of the Poisson integral upper bound combining weight and representation steps.

theorem PoissonHarnack.poisson_weight_upper_bound_surface_monotonicity_MVP_direct {n : ℕ} (u : (Fin n → ℝ) → ℝ) (R : ℝ) (hR : 0 < R) (hu_harmonic : CM7.IsHarmonic u (euclidBall 0 R)) (hu_nonneg : ∀ x ∈ euclidBall 0 R, 0 ≤ u x) (x : Fin n → ℝ) (hx : x ∈ euclidBall 0 R) (W : ℝ) (hW_eq : u x = (R ^ 2 - CM8.euclidNorm x ^ 2) * W) (_hW_nn : 0 ≤ W) (d : ℝ) (hd : 0 < d) (hd_bound : ∀ (σ : Fin n → ℝ), CM8.euclidNorm σ = R → d ≤ CM8.euclidNorm (x - σ)) : W ≤ R ^ (n - 2) * u 0 / d ^ n

Direct version of the Poisson weight upper bound: $W \le R^{n-2} u(0) / d^n$.

theorem PoissonHarnack.poisson_weight_bound_from_surface_integral_MVP_upper {n : ℕ} (u : (Fin n → ℝ) → ℝ) (R : ℝ) (hR : 0 < R) (hu_harmonic : CM7.IsHarmonic u (euclidBall 0 R)) (hu_nonneg : ∀ x ∈ euclidBall 0 R, 0 ≤ u x) (x : Fin n → ℝ) (hx : x ∈ euclidBall 0 R) (W : ℝ) (hW_eq : u x = (R ^ 2 - CM8.euclidNorm x ^ 2) * W) (_hW_nn : 0 ≤ W) (d : ℝ) (hd : 0 < d) (hd_bound : ∀ (σ : Fin n → ℝ), CM8.euclidNorm σ = R → d ≤ CM8.euclidNorm (x - σ)) : W ≤ R ^ (n - 2) * u 0 / d ^ n

Alias for poisson_weight_upper_bound_surface_monotonicity_MVP_direct.

theorem PoissonHarnack.poisson_formula_monotonicity_MVP_upper {n : ℕ} (u : (Fin n → ℝ) → ℝ) (R : ℝ) (hR : 0 < R) (hu_harmonic : CM7.IsHarmonic u (euclidBall 0 R)) (hu_nonneg : ∀ x ∈ euclidBall 0 R, 0 ≤ u x) (x : Fin n → ℝ) (hx : x ∈ euclidBall 0 R) (d : ℝ) (hd : 0 < d) (hd_bound : ∀ (σ : Fin n → ℝ), CM8.euclidNorm σ = R → d ≤ CM8.euclidNorm (x - σ)) : u x ≤ R ^ (n - 2) * (R ^ 2 - CM8.euclidNorm x ^ 2) / d ^ n * u 0

Poisson-formula style upper bound consequence: $u(x) \le \frac{R^{n-2}(R^2-|x|^2)}{d^n} u(0)$.

theorem PoissonHarnack.poisson_integral_lower_bound_surfaceIntegral_helper {n : ℕ} (u : (Fin n → ℝ) → ℝ) (R : ℝ) (hR : 0 < R) (hu_harmonic : CM7.IsHarmonic u (euclidBall 0 R)) (hu_nonneg : ∀ x ∈ euclidBall 0 R, 0 ≤ u x) (x : Fin n → ℝ) (hx : x ∈ euclidBall 0 R) (d : ℝ) (hd : 0 < d) (hd_bound : ∀ (σ : Fin n → ℝ), CM8.euclidNorm σ = R → CM8.euclidNorm (x - σ) ≤ d) : R ^ (n - 2) * (R ^ 2 - CM8.euclidNorm x ^ 2) / d ^ n * u 0 ≤ u x

Helper alias for the Poisson integral lower bound.

theorem PoissonHarnack.poisson_weight_lower_bound_from_kernel_MVP {n : ℕ} (u : (Fin n → ℝ) → ℝ) (R : ℝ) (hR : 0 < R) (hu_harmonic : CM7.IsHarmonic u (euclidBall 0 R)) (hu_nonneg : ∀ x ∈ euclidBall 0 R, 0 ≤ u x) (x : Fin n → ℝ) (hx : x ∈ euclidBall 0 R) (W : ℝ) (hW_eq : u x = (R ^ 2 - CM8.euclidNorm x ^ 2) * W) (d : ℝ) (hd : 0 < d) (hd_bound : ∀ (σ : Fin n → ℝ), CM8.euclidNorm σ = R → CM8.euclidNorm (x - σ) ≤ d) : R ^ (n - 2) * u 0 / d ^ n ≤ W

Lower bound on the Poisson weight $W$ derived from the kernel-based mean-value bound.

theorem PoissonHarnack.poisson_integral_upper_bound_surfaceIntegral_helper {n : ℕ} (u : (Fin n → ℝ) → ℝ) (R : ℝ) (hR : 0 < R) (hu_harmonic : CM7.IsHarmonic u (euclidBall 0 R)) (hu_nonneg : ∀ x ∈ euclidBall 0 R, 0 ≤ u x) (x : Fin n → ℝ) (hx : x ∈ euclidBall 0 R) (d : ℝ) (hd : 0 < d) (hd_bound : ∀ (σ : Fin n → ℝ), CM8.euclidNorm σ = R → d ≤ CM8.euclidNorm (x - σ)) : u x ≤ R ^ (n - 2) * (R ^ 2 - CM8.euclidNorm x ^ 2) / d ^ n * u 0

Helper alias for the Poisson integral upper bound.

theorem PoissonHarnack.poisson_weight_upper_bound_from_kernel_MVP {n : ℕ} (u : (Fin n → ℝ) → ℝ) (R : ℝ) (hR : 0 < R) (hu_harmonic : CM7.IsHarmonic u (euclidBall 0 R)) (hu_nonneg : ∀ x ∈ euclidBall 0 R, 0 ≤ u x) (x : Fin n → ℝ) (hx : x ∈ euclidBall 0 R) (W : ℝ) (hW_eq : u x = (R ^ 2 - CM8.euclidNorm x ^ 2) * W) (d : ℝ) (hd : 0 < d) (hd_bound : ∀ (σ : Fin n → ℝ), CM8.euclidNorm σ = R → d ≤ CM8.euclidNorm (x - σ)) : W ≤ R ^ (n - 2) * u 0 / d ^ n

Upper bound on the Poisson weight $W$ derived from the kernel-based mean-value bound.

theorem PoissonHarnack.poisson_integral_lower_bound_from_MVP {n : ℕ} (u : (Fin n → ℝ) → ℝ) (R : ℝ) (hR : 0 < R) (hu_harmonic : CM7.IsHarmonic u (euclidBall 0 R)) (hu_nonneg : ∀ x ∈ euclidBall 0 R, 0 ≤ u x) (x : Fin n → ℝ) (hx : x ∈ euclidBall 0 R) (d : ℝ) (hd : 0 < d) (hd_bound : ∀ (σ : Fin n → ℝ), CM8.euclidNorm σ = R → CM8.euclidNorm (x - σ) ≤ d) : R ^ (n - 2) * (R ^ 2 - CM8.euclidNorm x ^ 2) / d ^ n * u 0 ≤ u x

Poisson integral lower bound derived from the mean-value property.

theorem PoissonHarnack.poisson_integral_upper_bound_from_MVP {n : ℕ} (u : (Fin n → ℝ) → ℝ) (R : ℝ) (hR : 0 < R) (hu_harmonic : CM7.IsHarmonic u (euclidBall 0 R)) (hu_nonneg : ∀ x ∈ euclidBall 0 R, 0 ≤ u x) (x : Fin n → ℝ) (hx : x ∈ euclidBall 0 R) (d : ℝ) (hd : 0 < d) (hd_bound : ∀ (σ : Fin n → ℝ), CM8.euclidNorm σ = R → d ≤ CM8.euclidNorm (x - σ)) : u x ≤ R ^ (n - 2) * (R ^ 2 - CM8.euclidNorm x ^ 2) / d ^ n * u 0

Poisson integral upper bound derived from the mean-value property.

theorem PoissonHarnack.poisson_weight_lower_bound_from_integral_monotonicity {n : ℕ} (u : (Fin n → ℝ) → ℝ) (R : ℝ) (hR : 0 < R) (hu_harmonic : CM7.IsHarmonic u (euclidBall 0 R)) (hu_nonneg : ∀ x ∈ euclidBall 0 R, 0 ≤ u x) (x : Fin n → ℝ) (hx : x ∈ euclidBall 0 R) (W : ℝ) (hW_eq : u x = (R ^ 2 - CM8.euclidNorm x ^ 2) * W) (_hW_nn : 0 ≤ W) (d : ℝ) (hd : 0 < d) (hd_bound : ∀ (σ : Fin n → ℝ), CM8.euclidNorm σ = R → CM8.euclidNorm (x - σ) ≤ d) : R ^ (n - 2) * u 0 / d ^ n ≤ W

Lower bound on the Poisson weight $W$ derived from the integral monotonicity bound.

theorem PoissonHarnack.poisson_integral_lower_bound_axiom {n : ℕ} (u : (Fin n → ℝ) → ℝ) (R : ℝ) (hR : 0 < R) (hu_harmonic : CM7.IsHarmonic u (euclidBall 0 R)) (hu_nonneg : ∀ x ∈ euclidBall 0 R, 0 ≤ u x) (x : Fin n → ℝ) (hx : x ∈ euclidBall 0 R) (d : ℝ) (hd : 0 < d) (hd_bound : ∀ (σ : Fin n → ℝ), CM8.euclidNorm σ = R → CM8.euclidNorm (x - σ) ≤ d) : R ^ (n - 2) * (R ^ 2 - CM8.euclidNorm x ^ 2) / d ^ n * u 0 ≤ u x

Axiomatic form of the Poisson integral lower bound used in the Harnack inequality chain.

theorem PoissonHarnack.poisson_weight_lower_bound_axiom {n : ℕ} (u : (Fin n → ℝ) → ℝ) (R : ℝ) (hR : 0 < R) (hu_harmonic : CM7.IsHarmonic u (euclidBall 0 R)) (hu_nonneg : ∀ x ∈ euclidBall 0 R, 0 ≤ u x) (x : Fin n → ℝ) (hx : x ∈ euclidBall 0 R) (W : ℝ) (hW : u x = (R ^ 2 - CM8.euclidNorm x ^ 2) * W) (d : ℝ) (hd : 0 < d) (hd_bound : ∀ (σ : Fin n → ℝ), CM8.euclidNorm σ = R → CM8.euclidNorm (x - σ) ≤ d) : R ^ (n - 2) * u 0 / d ^ n ≤ W

Axiomatic form of the Poisson weight lower bound.

theorem PoissonHarnack.poisson_weight_upper_bound_axiom {n : ℕ} (u : (Fin n → ℝ) → ℝ) (R : ℝ) (hR : 0 < R) (hu_harmonic : CM7.IsHarmonic u (euclidBall 0 R)) (hu_nonneg : ∀ x ∈ euclidBall 0 R, 0 ≤ u x) (x : Fin n → ℝ) (hx : x ∈ euclidBall 0 R) (W : ℝ) (hW : u x = (R ^ 2 - CM8.euclidNorm x ^ 2) * W) (d : ℝ) (hd : 0 < d) (hd_bound : ∀ (σ : Fin n → ℝ), CM8.euclidNorm σ = R → d ≤ CM8.euclidNorm (x - σ)) : W ≤ R ^ (n - 2) * u 0 / d ^ n

Axiomatic form of the Poisson weight upper bound.

theorem PoissonHarnack.poisson_estimate_from_distance_upper {n : ℕ} (u : (Fin n → ℝ) → ℝ) (R : ℝ) (hR : 0 < R) (hu_harmonic : CM7.IsHarmonic u (euclidBall 0 R)) (hu_nonneg : ∀ x ∈ euclidBall 0 R, 0 ≤ u x) (x : Fin n → ℝ) (hx : x ∈ euclidBall 0 R) (d : ℝ) (hd : 0 < d) (hd_bound : ∀ (σ : Fin n → ℝ), CM8.euclidNorm σ = R → CM8.euclidNorm (x - σ) ≤ d) : R ^ (n - 2) * (R ^ 2 - CM8.euclidNorm x ^ 2) / d ^ n * u 0 ≤ u x

Poisson estimate from a distance upper bound: produces the lower bound $\frac{R^{n-2}(R^2 - |x|^2)}{d^n} u(0) \le u(x)$ when $\|x - \sigma\| \le d$.

theorem PoissonHarnack.poisson_estimate_from_distance_lower {n : ℕ} (u : (Fin n → ℝ) → ℝ) (R : ℝ) (hR : 0 < R) (hu_harmonic : CM7.IsHarmonic u (euclidBall 0 R)) (hu_nonneg : ∀ x ∈ euclidBall 0 R, 0 ≤ u x) (x : Fin n → ℝ) (hx : x ∈ euclidBall 0 R) (d : ℝ) (hd : 0 < d) (hd_bound : ∀ (σ : Fin n → ℝ), CM8.euclidNorm σ = R → d ≤ CM8.euclidNorm (x - σ)) : u x ≤ R ^ (n - 2) * (R ^ 2 - CM8.euclidNorm x ^ 2) / d ^ n * u 0

Poisson estimate from a distance lower bound: produces the upper bound $u(x) \le \frac{R^{n-2}(R^2 - |x|^2)}{d^n} u(0)$ when $d \le \|x - \sigma\|$.

theorem PoissonHarnack.poisson_integral_lower_estimate {n : ℕ} (u : (Fin n → ℝ) → ℝ) (R : ℝ) (hR : 0 < R) (hu_harmonic : CM7.IsHarmonic u (euclidBall 0 R)) (hu_nonneg : ∀ x ∈ euclidBall 0 R, 0 ≤ u x) (x : Fin n → ℝ) (hx : x ∈ euclidBall 0 R) : R ^ (n - 2) * (R ^ 2 - CM8.euclidNorm x ^ 2) / (R + CM8.euclidNorm x) ^ n * u 0 ≤ u x

Specialised lower Poisson estimate using $d = R + |x|$ (the maximum distance from $x$ to the sphere): $\frac{R^{n-2}(R^2 - |x|^2)}{(R + |x|)^n} u(0) \le u(x)$.

theorem PoissonHarnack.poisson_integral_upper_estimate {n : ℕ} (u : (Fin n → ℝ) → ℝ) (R : ℝ) (hR : 0 < R) (hu_harmonic : CM7.IsHarmonic u (euclidBall 0 R)) (hu_nonneg : ∀ x ∈ euclidBall 0 R, 0 ≤ u x) (x : Fin n → ℝ) (hx : x ∈ euclidBall 0 R) : u x ≤ R ^ (n - 2) * (R ^ 2 - CM8.euclidNorm x ^ 2) / (R - CM8.euclidNorm x) ^ n * u 0

Specialised upper Poisson estimate using $d = R - |x|$ (the minimum distance from $x$ to the sphere): $u(x) \le \frac{R^{n-2}(R^2 - |x|^2)}{(R - |x|)^n} u(0)$.

theorem PoissonHarnack.lower_bound_simplify (R d a : ℝ) (n : ℕ) (hn : 1 ≤ n) (hRd : R + d ≠ 0) : R ^ (n - 2) * (R ^ 2 - d ^ 2) / (R + d) ^ n * a = R ^ (n - 2) * (R - d) / (R + d) ^ (n - 1) * a

Algebraic simplification: $\frac{R^{n-2}(R^2 - d^2)}{(R+d)^n} = \frac{R^{n-2}(R - d)}{(R+d)^{n-1}}$, using $R^2 - d^2 = (R - d)(R + d)$.

theorem PoissonHarnack.upper_bound_simplify (R d a : ℝ) (n : ℕ) (hn : 1 ≤ n) (hRd : R - d ≠ 0) : R ^ (n - 2) * (R ^ 2 - d ^ 2) / (R - d) ^ n * a = R ^ (n - 2) * (R + d) / (R - d) ^ (n - 1) * a

Algebraic simplification: $\frac{R^{n-2}(R^2 - d^2)}{(R-d)^n} = \frac{R^{n-2}(R + d)}{(R-d)^{n-1}}$.

theorem PoissonHarnack.euclidNorm_fin_zero (x : Fin 0 → ℝ) : CM8.euclidNorm x = 0

The Euclidean norm on the trivial space $\mathbb{R}^0$ is identically zero.

theorem PoissonHarnack.lower_bound_n_zero {u : (Fin 0 → ℝ) → ℝ} (R : ℝ) (hR : 0 < R) (hu_nonneg : ∀ x ∈ euclidBall 0 R, 0 ≤ u x) (x : Fin 0 → ℝ) (_hx : x ∈ euclidBall 0 R) (h : (R ^ 2 - CM8.euclidNorm x ^ 2) * u 0 ≤ u x) : (R - CM8.euclidNorm x) * u 0 ≤ u x

Degenerate $n = 0$ case of the lower bound: simplifies away $|x|^2 = 0$.

theorem PoissonHarnack.upper_bound_n_zero {u : (Fin 0 → ℝ) → ℝ} (R : ℝ) (hR : 0 < R) (hu_nonneg : ∀ x ∈ euclidBall 0 R, 0 ≤ u x) (x : Fin 0 → ℝ) (_hx : x ∈ euclidBall 0 R) (h : u x ≤ (R ^ 2 - CM8.euclidNorm x ^ 2) * u 0) : u x ≤ (R + CM8.euclidNorm x) * u 0

Degenerate $n = 0$ case of the upper bound: simplifies away $|x|^2 = 0$.

theorem PoissonHarnack.euclidNorm_nonneg {n : ℕ} (v : Fin n → ℝ) : 0 ≤ CM8.euclidNorm v

The Euclidean norm is non-negative: $0 \le \|v\|$.

theorem PoissonHarnack.poisson_kernel_lower_bound {n : ℕ} (u : (Fin n → ℝ) → ℝ) (R : ℝ) (hR : 0 < R) (hu_harmonic : CM7.IsHarmonic u (euclidBall 0 R)) (hu_nonneg : ∀ x ∈ euclidBall 0 R, 0 ≤ u x) (x : Fin n → ℝ) (hx : x ∈ euclidBall 0 R) : R ^ (n - 2) * (R - CM8.euclidNorm x) / (R + CM8.euclidNorm x) ^ (n - 1) * u 0 ≤ u x

Harnack-style lower bound (Poisson-kernel form): $\frac{R^{n-2}(R - |x|)}{(R + |x|)^{n-1}} u(0) \le u(x)$ for $u$ harmonic and non-negative on $B_R(0)$.

theorem PoissonHarnack.poisson_kernel_upper_bound {n : ℕ} (u : (Fin n → ℝ) → ℝ) (R : ℝ) (hR : 0 < R) (hu_harmonic : CM7.IsHarmonic u (euclidBall 0 R)) (hu_nonneg : ∀ x ∈ euclidBall 0 R, 0 ≤ u x) (x : Fin n → ℝ) (hx : x ∈ euclidBall 0 R) : u x ≤ R ^ (n - 2) * (R + CM8.euclidNorm x) / (R - CM8.euclidNorm x) ^ (n - 1) * u 0

Harnack-style upper bound (Poisson-kernel form): $u(x) \le \frac{R^{n-2}(R + |x|)}{(R - |x|)^{n-1}} u(0)$ for $u$ harmonic and non-negative on $B_R(0)$.

theorem PoissonHarnack.harnack_inequality {n : ℕ} (u : (Fin n → ℝ) → ℝ) (R : ℝ) (hR : 0 < R) (hu_harmonic : CM7.IsHarmonic u (euclidBall 0 R)) (hu_nonneg : ∀ x ∈ euclidBall 0 R, 0 ≤ u x) (x : Fin n → ℝ) (hx : x ∈ euclidBall 0 R) : R ^ (n - 2) * (R - CM8.euclidNorm x) / (R + CM8.euclidNorm x) ^ (n - 1) * u 0 ≤ u x ∧ u x ≤ R ^ (n - 2) * (R + CM8.euclidNorm x) / (R - CM8.euclidNorm x) ^ (n - 1) * u 0

Theorem 4.1 (Harnack's inequality). Let $u$ be harmonic and non-negative on the ball $B_R(0) \subset \mathbb{R}^n$. Then for any $x \in B_R(0)$: $\frac{R^{n-2}(R - |x|)}{(R + |x|)^{n-1}} u(0) \le u(x) \le \frac{R^{n-2}(R + |x|)}{(R - |x|)^{n-1}} u(0)$.

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

The Laplacian of a constant function vanishes identically: $\Delta(c) = 0$.

theorem PoissonHarnack.isHarmonic_const {n : ℕ} (c : ℝ) (Ω : Set (Fin n → ℝ)) : CM7.IsHarmonic (fun (x : Fin n → ℝ) => c) Ω

Every constant function is harmonic on any domain $\Omega \subset \mathbb{R}^n$.

theorem PoissonHarnack.IsHarmonic.add_const {n : ℕ} {u : (Fin n → ℝ) → ℝ} {Ω : Set (Fin n → ℝ)} (hu : CM7.IsHarmonic u Ω) (c : ℝ) (hΩ : IsOpen Ω) : CM7.IsHarmonic (fun (x : Fin n → ℝ) => u x + c) Ω

Adding a constant preserves harmonicity: if $u$ is harmonic on $\Omega$, then so is $u + c$.

theorem PoissonHarnack.IsHarmonic.restrict {n : ℕ} {u : (Fin n → ℝ) → ℝ} (hu : CM7.IsHarmonic u Set.univ) (Ω : Set (Fin n → ℝ)) : CM7.IsHarmonic u Ω

A harmonic function on all of $\mathbb{R}^n$ is harmonic on any subset $\Omega$.

theorem PoissonHarnack.mem_euclidBall_of_lt {n : ℕ} (x : Fin n → ℝ) (R : ℝ) (hR : CM8.euclidNorm x < R) : x ∈ euclidBall 0 R

If $\|x\| < R$, then $x$ lies in the ball $B_R(0)$.

theorem PoissonHarnack.tendsto_div_sub_const (d : ℝ) : Filter.Tendsto (fun (R : ℝ) => R / (R - d)) Filter.atTop (nhds 1)

Limit identity: $\frac{R}{R - d} \to 1$ as $R \to \infty$.

theorem PoissonHarnack.tendsto_pow_ratio (k : ℕ) (d : ℝ) : Filter.Tendsto (fun (R : ℝ) => R ^ k / (R - d) ^ k) Filter.atTop (nhds 1)

Limit identity: $\left(\frac{R}{R - d}\right)^k \to 1$ as $R \to \infty$.

theorem PoissonHarnack.tendsto_add_div_sub (d : ℝ) : Filter.Tendsto (fun (R : ℝ) => (R + d) / (R - d)) Filter.atTop (nhds 1)

Limit identity: $\frac{R + d}{R - d} \to 1$ as $R \to \infty$.

theorem PoissonHarnack.tendsto_sub_div_add (d : ℝ) (hd : 0 ≤ d) : Filter.Tendsto (fun (R : ℝ) => (R - d) / (R + d)) Filter.atTop (nhds 1)

Limit identity: $\frac{R - d}{R + d} \to 1$ as $R \to \infty$, for $d \ge 0$.

theorem PoissonHarnack.tendsto_div_add_const (d : ℝ) (hd : 0 ≤ d) : Filter.Tendsto (fun (R : ℝ) => R / (R + d)) Filter.atTop (nhds 1)

Limit identity: $\frac{R}{R + d} \to 1$ as $R \to \infty$, for $d \ge 0$.

theorem PoissonHarnack.tendsto_pow_ratio_add (k : ℕ) (d : ℝ) (hd : 0 ≤ d) : Filter.Tendsto (fun (R : ℝ) => R ^ k / (R + d) ^ k) Filter.atTop (nhds 1)

Limit identity: $\left(\frac{R}{R + d}\right)^k \to 1$ as $R \to \infty$, for $d \ge 0$.

theorem PoissonHarnack.tendsto_upper_coeff (n : ℕ) (hn : 2 ≤ n) (d : ℝ) : Filter.Tendsto (fun (R : ℝ) => R ^ (n - 2) * (R + d) / (R - d) ^ (n - 1)) Filter.atTop (nhds 1)

Limit of the upper Harnack coefficient: $\frac{R^{n-2}(R+d)}{(R-d)^{n-1}} \to 1$ as $R \to \infty$.

theorem PoissonHarnack.tendsto_lower_coeff (n : ℕ) (hn : 2 ≤ n) (d : ℝ) (hd : 0 ≤ d) : Filter.Tendsto (fun (R : ℝ) => R ^ (n - 2) * (R - d) / (R + d) ^ (n - 1)) Filter.atTop (nhds 1)

Limit of the lower Harnack coefficient: $\frac{R^{n-2}(R-d)}{(R+d)^{n-1}} \to 1$ as $R \to \infty$.

theorem PoissonHarnack.harnack_upper_squeeze {n : ℕ} (d : ℝ) (hd : 0 ≤ d) (a b : ℝ) (h_le : ∀ (R : ℝ), d < R → b ≤ R ^ (n - 2) * (R + d) / (R - d) ^ (n - 1) * a) (h_ge : ∀ (R : ℝ), d < R → R ^ (n - 2) * (R - d) / (R + d) ^ (n - 1) * a ≤ b) : b = a

Harnack squeeze principle: if $b$ is squeezed between the lower and upper Harnack coefficients applied to $a$ for all sufficiently large $R$, then taking $R \to \infty$ forces $b = a$. This is the key analytical step in deducing Liouville's theorem from Harnack's inequality.

theorem PoissonHarnack.liouville_nonneg {n : ℕ} (v : (Fin n → ℝ) → ℝ) (hv_harmonic : CM7.IsHarmonic v Set.univ) (hv_nonneg : ∀ (x : Fin n → ℝ), 0 ≤ v x) : ∃ (c : ℝ), ∀ (x : Fin n → ℝ), v x = c

Liouville's theorem for non-negative harmonic functions: a non-negative harmonic function on $\mathbb{R}^n$ is constant.

theorem PoissonHarnack.liouville_theorem {n : ℕ} (u : (Fin n → ℝ) → ℝ) (hu_harmonic : CM7.IsHarmonic u Set.univ) (_hu_smooth : ContDiff ℝ 2 u) (M : ℝ) (hu_bdd : (∀ (x : Fin n → ℝ), M ≤ u x) ∨ ∀ (x : Fin n → ℝ), u x ≤ M) : ∃ (c : ℝ), ∀ (x : Fin n → ℝ), u x = c

Corollary 4.0.4 (Liouville's theorem). Suppose $u \in C^2(\mathbb{R}^n)$ is harmonic on all of $\mathbb{R}^n$, and there exists $M \in \mathbb{R}$ such that either $u(x) \ge M$ for all $x$ or $u(x) \le M$ for all $x$. Then $u$ is constant.