The Laplacian of an integral over a compact parameter space

For a function F that is C² on an open set W ⊆ E × P of a finite-dimensional real inner product space E times a parameter space P, a continuous map ι : α → P from a compact space, and an integrable weight g on α, the Laplacian in x commutes with integration:

Δ (x ↦ ∫ g(y) F(x, ι y) dμ(y)) = ∫ g(y) Δ (F(·, ι y)) dμ(y)

on any open set U with U × ι(α) ⊆ W. In particular the integral is harmonic there as soon as each F(·, ι y) is, which is how the Poisson integral of integrable boundary data on a sphere is shown to be harmonic.

Main declarations

• TauCeti.laplacian_integral_smul_of_contDiffOn: the Laplacian of the integral is the integral of the Laplacians.
• TauCeti.harmonicOnNhd_integral_smul_of_contDiffOn: an integral of harmonic functions against an integrable weight is harmonic.

theorem TauCeti.laplacian_integral_smul_of_contDiffOn {E : Type u_1} {P : Type u_2} {G : Type u_3} {α : Type u_4} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup G] [NormedSpace ℝ G] [CompleteSpace G] [TopologicalSpace α] [CompactSpace α] [SecondCountableTopology α] [MeasurableSpace α] [OpensMeasurableSpace α] {μ : MeasureTheory.Measure α} {ι : α → P} {g : α → ℝ} {W : Set (E × P)} {U : Set E} {F : E × P → G} (hg : MeasureTheory.Integrable g μ) (hι : Continuous ι) (hW : IsOpen W) (hF : ContDiffOn ℝ 2 F W) (hU : IsOpen U) (hUW : ∀ x ∈ U, ∀ (y : α), (x, ι y) ∈ W) {x₀ : E} (hx₀ : x₀ ∈ U) : Laplacian.laplacian (fun (x : E) => ∫ (y : α), g y • F (x, ι y) ∂μ) x₀ = ∫ (y : α), g y • Laplacian.laplacian (fun (x : E) => F (x, ι y)) x₀ ∂μ

The Laplacian commutes with integration over a compact parameter space. If F is C² on an open set W ⊆ E × P and U × ι(α) ⊆ W for an open set U, then at every point of U the Laplacian of x ↦ ∫ g(y) F(x, ι y) dμ(y) is the integral of the Laplacians of the slices F(·, ι y).

theorem TauCeti.harmonicOnNhd_integral_smul_of_contDiffOn {E : Type u_1} {P : Type u_2} {G : Type u_3} {α : Type u_4} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup G] [NormedSpace ℝ G] [CompleteSpace G] [TopologicalSpace α] [CompactSpace α] [SecondCountableTopology α] [MeasurableSpace α] [OpensMeasurableSpace α] {μ : MeasureTheory.Measure α} {ι : α → P} {g : α → ℝ} {W : Set (E × P)} {U : Set E} {F : E × P → G} (hg : MeasureTheory.Integrable g μ) (hι : Continuous ι) (hW : IsOpen W) (hF : ContDiffOn ℝ 2 F W) (hU : IsOpen U) (hUW : ∀ x ∈ U, ∀ (y : α), (x, ι y) ∈ W) (hharm : ∀ (y : α), InnerProductSpace.HarmonicOnNhd (fun (x : E) => F (x, ι y)) U) : InnerProductSpace.HarmonicOnNhd (fun (x : E) => ∫ (y : α), g y • F (x, ι y) ∂μ) U

Integrals of harmonic functions are harmonic. If F is C² on an open set W ⊆ E × P, U × ι(α) ⊆ W for an open set U, and each slice F(·, ι y) is harmonic on U, then x ↦ ∫ g(y) F(x, ι y) dμ(y) is harmonic on U for every integrable weight g.