The solenoidal subspace of L²(ℝ³; ℝ³) and convolution operators

For prop:lps-smoothing: the weakly divergence-free fields form the orthogonal complement of the test gradients in L²(ℝ³; ℝ³), realised as three L²(ℝ³) components. Convolution with a continuous compactly supported kernel acts componentwise as a bounded operator whose adjoint is convolution with the reflected kernel; it preserves the solenoidal subspace and therefore commutes with the orthogonal projection onto it.

@[reducible, inline]

abbrev ESS.LpsL2Field : Type

L²(ℝ³; ℝ³) as three real L²(ℝ³) components (prop:lps-smoothing).

Equations

• ESS.LpsL2Field = PiLp 2 fun (x : Fin 3) => ↥(MeasureTheory.Lp ℝ 2 MeasureTheory.volume)

@[reducible, inline]

abbrev ESS.LpsTestFunction : Type

Smooth compactly supported scalar test functions on ℝ³ (prop:lps-smoothing).

Equations

• ESS.LpsTestFunction = { φ : CKN.Foundation.Parabolic.Vec3 → ℝ // ContDiff ℝ (↑⊤) φ ∧ HasCompactSupport φ }

theorem ESS.lpsLeray_memLp_spatialDeriv_test {φ : CKN.Foundation.Parabolic.Vec3 → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (hφc : HasCompactSupport φ) (i : Fin 3) : MeasureTheory.MemLp (CKN.spatialDeriv φ i) 2 MeasureTheory.volume

Partial derivatives of test functions are square integrable (prop:lps-smoothing).

noncomputable def ESS.lpsTestGradient (φ : LpsTestFunction) : LpsL2Field

The gradient of a test function as an element of L²(ℝ³; ℝ³) (prop:lps-smoothing).

Equations

• ESS.lpsTestGradient φ = WithLp.toLp 2 fun (i : Fin 3) => MeasureTheory.MemLp.toLp (CKN.spatialDeriv (↑φ) i) ⋯

noncomputable def ESS.lpsSolenoidal : Submodule ℝ LpsL2Field

The weakly divergence-free fields in L²(ℝ³; ℝ³): the orthogonal complement of the test gradients (prop:lps-smoothing).

Equations

• ESS.lpsSolenoidal = (Submodule.span ℝ (Set.range ESS.lpsTestGradient))ᗮ

instance ESS.instHasOrthogonalProjectionRealLpsL2FieldLpsSolenoidal : lpsSolenoidal.HasOrthogonalProjection

theorem ESS.lpsLeray_inner_toLp (f : ↥(MeasureTheory.Lp ℝ 2 MeasureTheory.volume)) {ψ : CKN.Foundation.Parabolic.Vec3 → ℝ} (hψ : MeasureTheory.MemLp ψ 2 MeasureTheory.volume) : inner ℝ f (MeasureTheory.MemLp.toLp ψ hψ) = ∫ (x : CKN.Foundation.Parabolic.Vec3), ↑↑f x * ψ x

The L² pairing with a square-integrable function is the integral of the product (prop:lps-smoothing).

theorem ESS.lpsLeray_inner_testGradient (g : LpsL2Field) (φ : LpsTestFunction) : inner ℝ g (lpsTestGradient φ) = ∑ i : Fin 3, ∫ (x : CKN.Foundation.Parabolic.Vec3), ↑↑(g.ofLp i) x * CKN.spatialDeriv (↑φ) i x

Pairing a field with a test gradient (prop:lps-smoothing).

theorem ESS.mem_lpsSolenoidal_iff_inner (g : LpsL2Field) : g ∈ lpsSolenoidal ↔ ∀ (φ : LpsTestFunction), inner ℝ g (lpsTestGradient φ) = 0

Membership in the solenoidal subspace, tested on test gradients (prop:lps-smoothing).

theorem ESS.mem_lpsSolenoidal_iff (g : LpsL2Field) : g ∈ lpsSolenoidal ↔ ∀ (φ : CKN.Foundation.Parabolic.Vec3 → ℝ), ContDiff ℝ (↑⊤) φ → HasCompactSupport φ → ∑ i : Fin 3, ∫ (x : CKN.Foundation.Parabolic.Vec3), ↑↑(g.ofLp i) x * CKN.spatialDeriv φ i x = 0

Membership in the solenoidal subspace is the weak divergence-free condition (prop:lps-smoothing).

theorem ESS.lpsLeray_convolutionExists {θ f : CKN.Foundation.Parabolic.Vec3 → ℝ} (hθ : Continuous θ) (hθc : HasCompactSupport θ) (hf : MeasureTheory.MemLp f 2 MeasureTheory.volume) : MeasureTheory.ConvolutionExists θ f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume

Existence of convolutions of L² functions with continuous compactly supported kernels.

noncomputable def ESS.lpsConvL2 (θ : CKN.Foundation.Parabolic.Vec3 → ℝ) (hθ : Continuous θ) (hθc : HasCompactSupport θ) : ↥(MeasureTheory.Lp ℝ 2 MeasureTheory.volume) →L[ℝ] ↥(MeasureTheory.Lp ℝ 2 MeasureTheory.volume)

Convolution with a continuous compactly supported kernel as a bounded operator on L²(ℝ³) (prop:lps-smoothing).

Equations

• One or more equations did not get rendered due to their size.

theorem ESS.lpsConvL2_coeFn (θ : CKN.Foundation.Parabolic.Vec3 → ℝ) (hθ : Continuous θ) (hθc : HasCompactSupport θ) (f : ↥(MeasureTheory.Lp ℝ 2 MeasureTheory.volume)) : ↑↑((lpsConvL2 θ hθ hθc) f) =ᵐ[MeasureTheory.volume] MeasureTheory.convolution θ (↑↑f) (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume

The operator lpsConvL2 is convolution almost everywhere (prop:lps-smoothing).

theorem ESS.lpsConvL2_inner {θ θ' : CKN.Foundation.Parabolic.Vec3 → ℝ} (hθ : Continuous θ) (hθc : HasCompactSupport θ) (hθ' : Continuous θ') (hθc' : HasCompactSupport θ') (hrefl : ∀ (y : CKN.Foundation.Parabolic.Vec3), θ' y = θ (-y)) (f h : ↥(MeasureTheory.Lp ℝ 2 MeasureTheory.volume)) : inner ℝ ((lpsConvL2 θ hθ hθc) f) h = inner ℝ f ((lpsConvL2 θ' hθ' hθc') h)

The adjoint of convolution with θ on L²(ℝ³) is convolution with the reflected kernel (prop:lps-smoothing).

noncomputable def ESS.lpsConvField (θ : CKN.Foundation.Parabolic.Vec3 → ℝ) (hθ : Continuous θ) (hθc : HasCompactSupport θ) : LpsL2Field →L[ℝ] LpsL2Field

Componentwise convolution with a continuous compactly supported kernel on L²(ℝ³; ℝ³) (prop:lps-smoothing).

Equations

• One or more equations did not get rendered due to their size.

theorem ESS.lpsConvField_apply (θ : CKN.Foundation.Parabolic.Vec3 → ℝ) (hθ : Continuous θ) (hθc : HasCompactSupport θ) (g : LpsL2Field) (i : Fin 3) : ((lpsConvField θ hθ hθc) g).ofLp i = (lpsConvL2 θ hθ hθc) (g.ofLp i)

Components of lpsConvField (prop:lps-smoothing).

theorem ESS.lpsConvField_inner {θ θ' : CKN.Foundation.Parabolic.Vec3 → ℝ} (hθ : Continuous θ) (hθc : HasCompactSupport θ) (hθ' : Continuous θ') (hθc' : HasCompactSupport θ') (hrefl : ∀ (y : CKN.Foundation.Parabolic.Vec3), θ' y = θ (-y)) (f h : LpsL2Field) : inner ℝ ((lpsConvField θ hθ hθc) f) h = inner ℝ f ((lpsConvField θ' hθ' hθc') h)

The adjoint of componentwise convolution is componentwise convolution with the reflected kernel (prop:lps-smoothing).

theorem ESS.lpsLeray_continuous_reflect {θ : CKN.Foundation.Parabolic.Vec3 → ℝ} (hθ : Continuous θ) : Continuous fun (y : CKN.Foundation.Parabolic.Vec3) => θ (-y)

The reflection of a continuous kernel is continuous (prop:lps-smoothing).

theorem ESS.lpsLeray_hasCompactSupport_reflect {θ : CKN.Foundation.Parabolic.Vec3 → ℝ} (hθc : HasCompactSupport θ) : HasCompactSupport fun (y : CKN.Foundation.Parabolic.Vec3) => θ (-y)

The reflection of a compactly supported kernel is compactly supported (prop:lps-smoothing).

theorem ESS.lpsConvField_testGradient {θ : CKN.Foundation.Parabolic.Vec3 → ℝ} (hθ : Continuous θ) (hθc : HasCompactSupport θ) (φ : LpsTestFunction) : (lpsConvField θ hθ hθc) (lpsTestGradient φ) = lpsTestGradient ⟨MeasureTheory.convolution θ (↑φ) (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume, ⋯⟩

Convolution maps test gradients to test gradients (prop:lps-smoothing).

theorem ESS.lpsConvField_mem_lpsSolenoidal {θ : CKN.Foundation.Parabolic.Vec3 → ℝ} (hθ : Continuous θ) (hθc : HasCompactSupport θ) {g : LpsL2Field} (hg : g ∈ lpsSolenoidal) : (lpsConvField θ hθ hθc) g ∈ lpsSolenoidal

Convolution with a continuous compactly supported kernel preserves the solenoidal subspace (prop:lps-smoothing).

theorem ESS.lpsConvField_starProjection {θ : CKN.Foundation.Parabolic.Vec3 → ℝ} (hθ : Continuous θ) (hθc : HasCompactSupport θ) (f : LpsL2Field) : lpsSolenoidal.starProjection ((lpsConvField θ hθ hθc) f) = (lpsConvField θ hθ hθc) (lpsSolenoidal.starProjection f)

Convolution with a continuous compactly supported kernel commutes with the orthogonal projection onto the solenoidal subspace (prop:lps-smoothing).