theorem CM6.harmonic_volume_mean_value {n : ℕ} (hn : 0 < n) {Ω : Set (Fin n → ℝ)} {u : (Fin n → ℝ) → ℝ} (hu : CM7.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 (Theorem 4.1, first formula): if $u$ is harmonic on $\Omega$ and $\overline{B_R(x)} \subset \Omega$, then $u(x)$ equals the average of $u$ over the ball $B_R(x)$: $u(x) = \frac{n}{\omega_n R^n} \int_{B_R(x)} u(y) \, d^n y$.

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

Spherical mean value property (Theorem 4.1, second formula): if $u$ is harmonic on $\Omega$ and $\overline{B_R(x)} \subset \Omega$, then $u(x)$ equals the average of $u$ over the sphere $\partial B_R(x)$: $u(x) = \frac{1}{\omega_n R^{n-1}} \int_{\partial B_R(x)} u(\sigma) \, d\sigma$.

theorem CM6.mean_value_property {n : ℕ} (hn : 0 < n) {Ω : Set (Fin n → ℝ)} {u : (Fin n → ℝ) → ℝ} (hu : CM7.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 ∧ u x = ⨍ (ω : Fin n → ℝ) in Metric.sphere 0 1, u (x + R • ω) ∂MeasureTheory.Measure.hausdorffMeasure ↑(n - 1)

Mean value properties (Theorem 4.1, combined): a harmonic function $u$ on $\Omega$ satisfies both the volume and the spherical mean value formulas on every ball $\overline{B_R(x)} \subset \Omega$.

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

Strong Maximum Principle (Theorem 5.1, max version): if $u \in C(\Omega)$ verifies the volume mean value property and attains its maximum at an interior point $p \in \Omega$ of a connected open set $\Omega$, then $u$ is constant on $\Omega$.

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

Strong Minimum Principle (Theorem 5.1, min version): if $u \in C(\Omega)$ verifies the volume mean value property and attains its minimum at an interior point $p \in \Omega$ of a connected open set $\Omega$, then $u$ is constant on $\Omega$.

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

Strong Maximum Principle (Theorem 5.1): if $u$ attains either its maximum or its minimum on $\Omega$ at an interior point, then $u$ is constant on $\Omega$.

theorem CM6.strong_max_principle_bounded {n : ℕ} {Ω : Set (Fin n → ℝ)} (hΩo : IsOpen Ω) (hΩc : IsConnected Ω) (hΩb : Bornology.IsBounded Ω) {u : (Fin n → ℝ) → ℝ} (hmvp : CM7.HasVolumeMVP u Ω) (huc : ContinuousOn u (closure Ω)) (hnc : ¬∀ x ∈ Ω, ∀ y ∈ Ω, u x = u y) {x : Fin n → ℝ} (hx : x ∈ Ω) : (∃ q ∈ frontier Ω, u x < u q) ∧ ∃ q ∈ frontier Ω, u q < u x

Strong Maximum Principle on bounded domains (Theorem 5.1 boundary form): if $\Omega$ is bounded, $u$ verifies the mean value property and is continuous on $\overline{\Omega}$, and $u$ is non-constant on $\Omega$, then for every $x \in \Omega$ there exist boundary points $q, q' \in \partial \Omega$ with $u(x) < u(q)$ and $u(q') < u(x)$.

theorem CM6.strong_max_principle_boundary_bounds {n : ℕ} {Ω : Set (Fin n → ℝ)} (hΩo : IsOpen Ω) (hΩc : IsConnected Ω) (hΩb : Bornology.IsBounded Ω) {u : (Fin n → ℝ) → ℝ} (hmvp : CM7.HasVolumeMVP u Ω) (huc : ContinuousOn u (closure Ω)) (hnc : ¬∀ x ∈ Ω, ∀ y ∈ Ω, u x = u y) {x : Fin n → ℝ} (hx : x ∈ Ω) : u x < sSup (u '' frontier Ω) ∧ sInf (u '' frontier Ω) < u x

Strong Maximum Principle in sup/inf form (Theorem 5.1): for a non-constant $u$ on a bounded, connected open $\Omega$ with the mean value property and continuous on $\overline{\Omega}$, every interior $x \in \Omega$ satisfies $\inf_{\partial \Omega} u < u(x) < \sup_{\partial \Omega} u$.

theorem CM6.strong_maximum_principle_full {n : ℕ} {Ω : Set (Fin n → ℝ)} (hΩo : IsOpen Ω) (hΩc : IsConnected Ω) (hΩb : Bornology.IsBounded Ω) {u : (Fin n → ℝ) → ℝ} (hmvp : CM7.HasVolumeMVP u Ω) (huc : ContinuousOn u (closure Ω)) : (∀ p ∈ Ω, ((∀ x ∈ Ω, u x ≤ u p) ∨ ∀ x ∈ Ω, u p ≤ u x) → ∀ x ∈ Ω, u x = u p) ∧ ((¬∀ x ∈ Ω, ∀ y ∈ Ω, u x = u y) → ∀ x ∈ Ω, u x < sSup (u '' frontier Ω) ∧ sInf (u '' frontier Ω) < u x)

Combined statement of the Strong Maximum Principle (Theorem 5.1): interior extrema force the function to be constant, and for non-constant solutions every interior value is strictly between the boundary infimum and supremum.

theorem CM6.dirichlet_uniqueness_comparison_stability {n : ℕ} (hn : 0 < n) {Ω : Set (Fin n → ℝ)} (hΩo : IsOpen Ω) (hΩc : IsConnected Ω) (hΩb : Bornology.IsBounded Ω) : (∀ (u₁ u₂ : (Fin n → ℝ) → ℝ), CM7.IsHarmonic u₁ Ω → CM7.IsHarmonic u₂ Ω → (∀ x ∈ frontier Ω, u₁ x = u₂ x) → ContinuousOn u₁ (closure Ω) → ContinuousOn u₂ (closure Ω) → ∀ x ∈ Ω, u₁ x = u₂ x) ∧ (∀ (u_f u_g : (Fin n → ℝ) → ℝ), CM7.IsHarmonic u_f Ω → CM7.IsHarmonic u_g Ω → ContinuousOn u_f (closure Ω) → ContinuousOn u_g (closure Ω) → (∀ x ∈ frontier Ω, u_f x ≥ u_g x) → (∃ y ∈ frontier Ω, u_f y > u_g y) → ∀ x ∈ Ω, u_f x > u_g x) ∧ ∀ (u_f u_g : (Fin n → ℝ) → ℝ), CM7.IsHarmonic u_f Ω → CM7.IsHarmonic u_g Ω → ContinuousOn u_f (closure Ω) → ContinuousOn u_g (closure Ω) → ∀ (f g : (Fin n → ℝ) → ℝ) (M : ℝ), (∀ x ∈ frontier Ω, u_f x = f x) → (∀ x ∈ frontier Ω, u_g x = g x) → (∀ y ∈ frontier Ω, |f y - g y| ≤ M) → ∀ x ∈ Ω, |u_f x - u_g x| ≤ M

Corollary 5.0.1: for the Dirichlet problem $\Delta u = 0$ in $\Omega$, $u = f$ on $\partial \Omega$ on a bounded, connected open $\Omega \subset \mathbb{R}^n$, the following hold: (1) uniqueness of harmonic solutions sharing boundary values; (2) a comparison principle — if the boundary data satisfies $f \geq g$ with strict inequality somewhere, then $u_f > u_g$ in $\Omega$; (3) a stability estimate $|u_f - u_g| \leq M$ in $\Omega$ whenever $|f - g| \leq M$ on $\partial \Omega$.