The Laplacian of a W^{2,p} function

For u ∈ W^{2,p}(Ω) on an open set Ω of a finite-dimensional real inner product space, the weak Hessian TauCeti.Wkp.iteratedGradient 1 u is an Lᵖ field of endomorphisms, and its trace is the Laplacian of u in the sense of distributions: for every test function φ on Ω,

∫ Δφ • u = ∫ φ • tr D²u.

Consequently the two notions of a solution of Δu = f coincide in W^{2,p}(Ω): for locally integrable f, the weak formulation ∫ Δφ • u = ∫ φ • f for all test functions φ holds exactly when u is a strong solution, tr D²u = f almost everywhere in Ω. This is the form in which Lᵖ estimates for the second derivatives, which are stated through the Laplacian, apply to solutions of Poisson's equation given in either formulation.

No boundedness or boundary regularity of Ω is used.

Main declarations

• TauCeti.Wkp.integral_laplacian_smul_value_eq: the distributional Laplacian of a W^{2,p} function is the trace of its weak Hessian.
• TauCeti.Wkp.forall_integral_laplacian_smul_value_eq_iff: weak and strong solutions of Δu = f agree in W^{2,p}(Ω).
• TauCeti.Wkp.trace_iteratedGradient_ofTestFunctionₗ_ae_eq: for a test function φ, regarded as an element of W^{2,p}(Ω), the trace of the weak Hessian is Δφ.

References

• D. Gilbarg, N. S. Trudinger, Elliptic Partial Differential Equations of Second Order, §9.4.

theorem TauCeti.Wkp.integral_laplacian_smul_value_eq {E : Type u_1} [MeasurableSpace E] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {Omega : TopologicalSpace.Opens E} {p : ENNReal} [Fact (1 ≤ p)] (u : Wkp mu Omega p 2) (φ : TestFunction Omega ℝ ⊤) : ∫ (x : E), Laplacian.laplacian (⇑φ) x • ↑↑(value 2 u) x ∂mu = ∫ (x : E), φ x • (LinearMap.trace ℝ E) ↑(↑↑(iteratedGradient 1 u) x) ∂mu

The distributional Laplacian of a W^{2,p} function is the trace of its weak Hessian: ∫ Δφ • u = ∫ φ • tr D²u for every test function φ on Ω.

theorem TauCeti.Wkp.forall_integral_laplacian_smul_value_eq_iff {E : Type u_1} [MeasurableSpace E] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {Omega : TopologicalSpace.Opens E} {p : ENNReal} [Fact (1 ≤ p)] (u : Wkp mu Omega p 2) {f : E → ℝ} (hf : MeasureTheory.LocallyIntegrableOn f (↑Omega) mu) : (∀ (φ : TestFunction Omega ℝ ⊤), ∫ (x : E), Laplacian.laplacian (⇑φ) x • ↑↑(value 2 u) x ∂mu = ∫ (x : E), φ x • f x ∂mu) ↔ (fun (x : E) => (LinearMap.trace ℝ E) ↑(↑↑(iteratedGradient 1 u) x)) =ᵐ[mu.restrict ↑Omega] f

Weak and strong solutions of Δu = f agree in W^{2,p}(Ω). For u ∈ W^{2,p}(Ω) and f locally integrable on Ω, ∫ Δφ • u = ∫ φ • f holds for every test function φ on Ω if and only if the trace of the weak Hessian of u is f almost everywhere in Ω.

theorem TauCeti.Wkp.trace_iteratedGradient_ofTestFunctionₗ_ae_eq {E : Type u_1} [MeasurableSpace E] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {Omega : TopologicalSpace.Opens E} {p : ENNReal} [Fact (1 ≤ p)] (φ : TestFunction Omega ℝ ⊤) : (fun (x : E) => (LinearMap.trace ℝ E) ↑(↑↑(iteratedGradient 1 ((ofTestFunctionₗ 2) φ)) x)) =ᵐ[mu.restrict ↑Omega] Laplacian.laplacian ⇑φ

The trace of the weak Hessian of a test function is its Laplacian: for a test function φ on Ω, regarded as an element of W^{2,p}(Ω), tr D²φ = Δφ almost everywhere in Ω.