structure PoissonEquation.SmoothZeroAtInfty (n : ℕ) : Type

A smooth ℂ-valued function on ℝⁿ whose iterated derivatives of every order decay to zero at infinity (i.e. tend to 0 along the cocompact filter).

• toFun : EuclideanSpace ℝ (Fin n) → ℂ
• smooth' : ContDiff ℝ (↑⊤) self.toFun
• zero_at_infty' (m : ℕ) : Filter.Tendsto (fun (x : EuclideanSpace ℝ (Fin n)) => ‖iteratedFDeriv ℝ m self.toFun x‖) (Filter.cocompact (EuclideanSpace ℝ (Fin n))) (nhds 0)

@[implicit_reducible]

instance PoissonEquation.SmoothZeroAtInfty.instFunLikeEuclideanSpaceRealFinComplex {n : ℕ} : FunLike (SmoothZeroAtInfty n) (EuclideanSpace ℝ (Fin n)) ℂ

Treat SmoothZeroAtInfty n as a FunLike so that an element can be applied like a function.

theorem PoissonEquation.SmoothZeroAtInfty.ext {n : ℕ} {f g : SmoothZeroAtInfty n} (h : ∀ (x : EuclideanSpace ℝ (Fin n)), f x = g x) : f = g

Pointwise extensionality for SmoothZeroAtInfty.

theorem PoissonEquation.SmoothZeroAtInfty.ext_iff {n : ℕ} {f g : SmoothZeroAtInfty n} : f = g ↔ ∀ (x : EuclideanSpace ℝ (Fin n)), f x = g x

theorem PoissonEquation.SmoothZeroAtInfty.smooth {n : ℕ} (f : SmoothZeroAtInfty n) : ContDiff ℝ ↑⊤ ⇑f

An element of SmoothZeroAtInfty n is C^∞ smooth.

theorem PoissonEquation.SmoothZeroAtInfty.zero_at_infty {n : ℕ} (f : SmoothZeroAtInfty n) (m : ℕ) : Filter.Tendsto (fun (x : EuclideanSpace ℝ (Fin n)) => ‖iteratedFDeriv ℝ m (⇑f) x‖) (Filter.cocompact (EuclideanSpace ℝ (Fin n))) (nhds 0)

The m-th iterated derivative norm of f : SmoothZeroAtInfty n tends to 0 at infinity.

def PoissonEquation.IsLaplacianOf (n : ℕ) (f g : EuclideanSpace ℝ (Fin n) → ℂ) : Prop

IsLaplacianOf n f g says that g = -Δ f pointwise, where Δ is the standard Laplacian on ℝⁿ defined via the iterated Fréchet derivative.

theorem PoissonEquation.harmonic_fderiv_norm_le_div {n : ℕ} (hn : 1 ≤ n) (u : EuclideanSpace ℝ (Fin n) → ℂ) (hsmooth : ContDiff ℝ (↑⊤) u) (hharm : IsLaplacianOf n u 0) (C : ℝ) (hC : 0 ≤ C) (hbd : ∀ (x : EuclideanSpace ℝ (Fin n)), ‖u x‖ ≤ C) (R : ℝ) (hR : 0 < R) (a : EuclideanSpace ℝ (Fin n)) : ‖fderiv ℝ u a‖ ≤ ↑n * C / R

Gradient estimate (mean value inequality) for a bounded harmonic function: ‖∇u(a)‖ ≤ n · C / R for any radius R > 0.

theorem PoissonEquation.bounded_harmonic_fderiv_eq_zero {n : ℕ} (hn : 1 ≤ n) (u : EuclideanSpace ℝ (Fin n) → ℂ) (hsmooth : ContDiff ℝ (↑⊤) u) (hharm : IsLaplacianOf n u 0) (hbd : ∃ (C : ℝ), ∀ (x : EuclideanSpace ℝ (Fin n)), ‖u x‖ ≤ C) (x : EuclideanSpace ℝ (Fin n)) : fderiv ℝ u x = 0

Liouville-type derivative vanishing: a bounded harmonic function has zero Fréchet derivative everywhere.

theorem PoissonEquation.bounded_harmonic_is_constant {n : ℕ} (hn : 1 ≤ n) (u : EuclideanSpace ℝ (Fin n) → ℂ) (hsmooth : ContDiff ℝ (↑⊤) u) (hharm : IsLaplacianOf n u 0) (hbd : ∃ (C : ℝ), ∀ (x : EuclideanSpace ℝ (Fin n)), ‖u x‖ ≤ C) : ∃ (c : ℂ), u = Function.const (EuclideanSpace ℝ (Fin n)) c

Liouville's theorem: a bounded harmonic function on ℝⁿ is constant.

theorem PoissonEquation.laplacianOp_smooth_eq_classical {n : ℕ} (hn : 3 ≤ n) (u : SmoothZeroAtInfty n) (u_td : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) (hu_td : ∀ (φ : SchwartzMap (EuclideanSpace ℝ (Fin n)) ℂ), u_td φ = ∫ (x : EuclideanSpace ℝ (Fin n)), φ x • u x) (φ : SchwartzMap (EuclideanSpace ℝ (Fin n)) ℂ) : (DifferentialOperators.laplacianOp u_td) φ = ∫ (x : EuclideanSpace ℝ (Fin n)), φ x • -∑ j : Fin n, (iteratedFDeriv ℝ 2 (⇑u) x) fun (x : Fin 2) => EuclideanSpace.single j 1

Integration by parts: for a smooth, decaying u representing a tempered distribution u_td, the distributional Laplacian acts as the pointwise classical Laplacian against test functions.

theorem PoissonEquation.schwartz_determines_continuous {n : ℕ} (hn : 3 ≤ n) (u : SmoothZeroAtInfty n) (f : SchwartzMap (EuclideanSpace ℝ (Fin n)) ℂ) (h : ∀ (φ : SchwartzMap (EuclideanSpace ℝ (Fin n)) ℂ), (∫ (x : EuclideanSpace ℝ (Fin n)), φ x • -∑ j : Fin n, (iteratedFDeriv ℝ 2 (⇑u) x) fun (x : Fin 2) => EuclideanSpace.single j 1) = ∫ (x : EuclideanSpace ℝ (Fin n)), φ x • f x) (x : EuclideanSpace ℝ (Fin n)) : f x = -∑ j : Fin n, (iteratedFDeriv ℝ 2 (⇑u) x) fun (x : Fin 2) => EuclideanSpace.single j 1

Schwartz testing determines continuous functions pointwise: if two continuous functions integrate identically against every Schwartz test, they coincide.

theorem PoissonEquation.distributional_laplacian_eq_pointwise {n : ℕ} (hn : 3 ≤ n) (u : SmoothZeroAtInfty n) (f : SchwartzMap (EuclideanSpace ℝ (Fin n)) ℂ) (u_td : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) (hu_td : ∀ (φ : SchwartzMap (EuclideanSpace ℝ (Fin n)) ℂ), u_td φ = ∫ (x : EuclideanSpace ℝ (Fin n)), φ x • u x) (hlap : DifferentialOperators.laplacianOp u_td = (SchwartzMap.toTemperedDistributionCLM (EuclideanSpace ℝ (Fin n)) ℂ MeasureTheory.volume) f) : IsLaplacianOf n ⇑u ⇑f

The distributional Laplacian of u agrees with the pointwise Laplacian when both are defined and u is smooth and decaying.

theorem PoissonEquation.fourier_laplacian_inverse_schwartz {n : ℕ} (hn : 3 ≤ n) (f : SchwartzMap (EuclideanSpace ℝ (Fin n)) ℂ) : ∃ (g : EuclideanSpace ℝ (Fin n) → ℂ), ContDiff ℝ (↑⊤) g ∧ (∀ (m : ℕ), Filter.Tendsto (fun (x : EuclideanSpace ℝ (Fin n)) => ‖iteratedFDeriv ℝ m g x‖) (Filter.cocompact (EuclideanSpace ℝ (Fin n))) (nhds 0)) ∧ IsLaplacianOf n g ⇑f

Existence of a smooth, decaying Laplacian inverse for a Schwartz right-hand side f in dimension n ≥ 3.

theorem PoissonEquation.laplacian_injective {n : ℕ} (hn : 3 ≤ n) (u₁ u₂ : SmoothZeroAtInfty n) (f : EuclideanSpace ℝ (Fin n) → ℂ) (h₁ : IsLaplacianOf n (⇑u₁) f) (h₂ : IsLaplacianOf n (⇑u₂) f) : u₁ = u₂

Injectivity of the Laplacian on SmoothZeroAtInfty n: two decaying solutions of -Δuᵢ = f agree.