def DifferentialOperators.IsHarmonic {n : ℕ} (u : EuclideanSpace ℝ (Fin n) → ℂ) : Prop

A complex-valued function on Euclidean space is harmonic if it is smooth and its Laplacian (sum of pure second partial derivatives along the standard basis directions) vanishes everywhere.

theorem DifferentialOperators.SmoothZeroAtInfty.exists_norm_le {n : ℕ} (u : SmoothZeroAtInfty n) : ∃ (C : ℝ), ∀ (x : EuclideanSpace ℝ (Fin n)), ‖u x‖ ≤ C

Any smooth function that vanishes at infinity on Euclidean space is globally bounded: combine continuity with the eventually-small tail to get a uniform bound.

theorem DifferentialOperators.bounded_harmonic_is_constant {n : ℕ} (hn : 0 < n) (u : EuclideanSpace ℝ (Fin n) → ℂ) (hharm : IsHarmonic u) (hbdd : ∃ (C : ℝ), ∀ (x : EuclideanSpace ℝ (Fin n)), ‖u x‖ ≤ C) : ∃ (c : ℂ), ∀ (x : EuclideanSpace ℝ (Fin n)), u x = c

Liouville's theorem in the form used for Poisson uniqueness: a bounded harmonic function on ℝⁿ (n > 0) is constant.

theorem DifferentialOperators.eq_zero_of_const_tendsto_zero {n : ℕ} (hn : 0 < n) (c : ℂ) (h : Filter.Tendsto (fun (x : EuclideanSpace ℝ (Fin n)) => c) (Filter.cocompact (EuclideanSpace ℝ (Fin n))) (nhds 0)) : c = 0

A constant function on a noncompact Euclidean space that tends to zero at infinity must be zero, since constants converge to themselves and limits are unique.