The Laplacian against test functions

For a C² function u on an open set Ω of a finite-dimensional real inner product space and a test function φ ∈ 𝓓(Ω), integrating by parts twice in each coordinate direction gives Green's second identity in the boundary-free form

∫ Δφ • u ∂μ = ∫ φ • Δu ∂μ,

for any additive Haar measure μ: the classical Laplacian of a C² function is its distributional Laplacian on Ω. In particular a function harmonic on Ω is weakly harmonic: ∫ Δφ • u = 0 for every test function φ on Ω. This is the form in which harmonicity enters integral arguments such as the mean-value property, where the test functions are radial.

The two integrations by parts are the defining identities of the weak derivative TauCeti.HasWeakLineDerivOn, applied to u and to its first directional derivative, both of which are classical derivatives and hence weak ones (TauCeti.hasWeakLineDerivOn_of_hasLineDerivAt). No boundary term appears because the test function is compactly supported in Ω, and no regularity of ∂Ω is used.

Main declarations

• ContDiffOn.integral_fderiv_fderiv_smul_eq_integral_smul_fderiv_fderiv: second-order integration by parts in one direction, ∫ ∂ᵥ∂ᵥφ • u = ∫ φ • ∂ᵥ∂ᵥu.
• ContDiffOn.integral_laplacian_smul_eq_integral_smul_laplacian: Green's second identity against a test function, ∫ Δφ • u = ∫ φ • Δu.
• InnerProductSpace.HarmonicOnNhd.integral_laplacian_smul_eq_zero: a harmonic function is weakly harmonic.
• TestFunction.laplacianCLM_apply: the test-function Laplacian agrees pointwise with the classical Laplacian.

theorem ContDiffOn.integral_fderiv_fderiv_smul_eq_integral_smul_fderiv_fderiv {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure] {Ω : TopologicalSpace.Opens E} {u : E → F} (hu : ContDiffOn ℝ 2 u ↑Ω) (φ : TestFunction Ω ℝ ⊤) (v : E) : ∫ (x : E), (fderiv ℝ (fun (y : E) => (fderiv ℝ (⇑φ) y) v) x) v • u x ∂μ = ∫ (x : E), φ x • (fderiv ℝ (fun (y : E) => (fderiv ℝ u y) v) x) v ∂μ

Second-order integration by parts against a test function, in one direction v. For u of class C² on the open set Ω and a test function φ on Ω, ∫ ∂ᵥ∂ᵥφ • u = ∫ φ • ∂ᵥ∂ᵥu.

theorem ContDiffOn.integral_laplacian_smul_eq_integral_smul_laplacian {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure] {Ω : TopologicalSpace.Opens E} {u : E → F} (hu : ContDiffOn ℝ 2 u ↑Ω) (φ : TestFunction Ω ℝ ⊤) : ∫ (x : E), Laplacian.laplacian (⇑φ) x • u x ∂μ = ∫ (x : E), φ x • Laplacian.laplacian u x ∂μ

Green's second identity against a test function. For u of class C² on the open set Ω and a test function φ on Ω, ∫ Δφ • u ∂μ = ∫ φ • Δu ∂μ: the classical Laplacian of a C² function is its distributional Laplacian.

theorem InnerProductSpace.HarmonicOnNhd.integral_laplacian_smul_eq_zero {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure] {Ω : TopologicalSpace.Opens E} {u : E → F} (hu : HarmonicOnNhd u ↑Ω) (φ : TestFunction Ω ℝ ⊤) : ∫ (x : E), Laplacian.laplacian (⇑φ) x • u x ∂μ = 0

A harmonic function is weakly harmonic. If u is harmonic on the open set Ω, then ∫ Δφ • u ∂μ = 0 for every test function φ on Ω.

@[simp]

theorem TestFunction.laplacianCLM_apply {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω : TopologicalSpace.Opens E} (φ : TestFunction Ω F ⊤) (y : E) : ((LineDeriv.laplacianCLM ℝ E (TestFunction Ω F ⊤)) φ) y = Laplacian.laplacian (⇑φ) y

Applying the test-function Laplacian operator agrees pointwise with the classical Laplacian of the underlying smooth function.