The Leray projection on L²(ℝ³; ℝ³)

The Leray projection used in the proof of prop:lps-smoothing: the orthogonal projection P onto the weakly divergence-free fields is a contraction, is self-adjoint, fixes weakly divergence-free fields, annihilates gradients of H¹ functions, and commutes with weak partial derivatives. The last property follows from the commutation of P with convolutions: a weak derivative is moved onto the kernel of a mollifier and the mollifier is then removed in the limit.

theorem ESS.lpsLeray_gradient_mem_orthogonal {q : CKN.Foundation.Parabolic.Vec3 → ℝ} {G : LpsL2Field} (hq : MeasureTheory.MemLp q 2 MeasureTheory.volume) (hG : ∀ (i : Fin 3), CKN.HasWeakPartialDerivOn Set.univ i q ↑↑(G.ofLp i)) : G ∈ lpsSolenoidalᗮ

Gradients of H¹(ℝ³) functions are orthogonal to the weakly divergence-free fields (prop:lps-smoothing).

theorem ESS.lpsLeray_conv_reflect_spatialDeriv {θ g G : CKN.Foundation.Parabolic.Vec3 → ℝ} {k : Fin 3} (hθ : ContDiff ℝ (↑⊤) θ) (hθc : HasCompactSupport θ) (hg : CKN.HasWeakPartialDerivOn Set.univ k g G) (x : CKN.Foundation.Parabolic.Vec3) : MeasureTheory.convolution (fun (y : CKN.Foundation.Parabolic.Vec3) => CKN.spatialDeriv θ k (-y)) g (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume x = -MeasureTheory.convolution (fun (y : CKN.Foundation.Parabolic.Vec3) => θ (-y)) G (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume x

Moving a weak derivative of g onto the reflected derivative of a smooth kernel (prop:lps-smoothing).

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

Test functions are square integrable (prop:lps-smoothing).

theorem ESS.lpsLeray_starProjection_pairing {g G : LpsL2Field} {k : Fin 3} (h : ∀ (i : Fin 3), CKN.HasWeakPartialDerivOn Set.univ k ↑↑(g.ofLp i) ↑↑(G.ofLp i)) (i : Fin 3) {θ : CKN.Foundation.Parabolic.Vec3 → ℝ} (hθ : ContDiff ℝ (↑⊤) θ) (hθc : HasCompactSupport θ) {φ : CKN.Foundation.Parabolic.Vec3 → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (hφc : HasCompactSupport φ) : ∫ (x : CKN.Foundation.Parabolic.Vec3), ↑↑((lpsSolenoidal.starProjection g).ofLp i) x * MeasureTheory.convolution θ (CKN.spatialDeriv φ k) (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume x = -∫ (x : CKN.Foundation.Parabolic.Vec3), ↑↑((lpsSolenoidal.starProjection G).ofLp i) x * MeasureTheory.convolution θ φ (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume x

The pairing identity behind the commutation of the Leray projection with weak derivatives, for one smooth compactly supported kernel θ (prop:lps-smoothing).

theorem ESS.lpsLeray_tendsto_integral_mul_mollify (f : ↥(MeasureTheory.Lp ℝ 2 MeasureTheory.volume)) {ψ : CKN.Foundation.Parabolic.Vec3 → ℝ} (hψ : MeasureTheory.MemLp ψ 2 MeasureTheory.volume) {ε : ℕ → ℝ} (hε : Filter.Tendsto ε Filter.atTop (nhds 0)) (hεpos : ∀ (n : ℕ), 0 < ε n) : Filter.Tendsto (fun (n : ℕ) => ∫ (x : CKN.Foundation.Parabolic.Vec3), ↑↑f x * CKN.mollify ψ (ε n) ⋯ x) Filter.atTop (nhds (∫ (x : CKN.Foundation.Parabolic.Vec3), ↑↑f x * ψ x))

Pairing an L² function with a mollified L² function converges to the unmollified pairing (prop:lps-smoothing).

theorem ESS.lpsLeray_starProjection_hasWeakPartialDerivOn {g G : LpsL2Field} {k : Fin 3} (h : ∀ (i : Fin 3), CKN.HasWeakPartialDerivOn Set.univ k ↑↑(g.ofLp i) ↑↑(G.ofLp i)) (i : Fin 3) : CKN.HasWeakPartialDerivOn Set.univ k ↑↑((lpsSolenoidal.starProjection g).ofLp i) ↑↑((lpsSolenoidal.starProjection G).ofLp i)

The Leray projection commutes with weak partial derivatives (prop:lps-smoothing).

theorem ESS.lps_leray_exists : ∃ (P : (PiLp 2 fun (x : Fin 3) => ↥(MeasureTheory.Lp ℝ 2 MeasureTheory.volume)) →L[ℝ] PiLp 2 fun (x : Fin 3) => ↥(MeasureTheory.Lp ℝ 2 MeasureTheory.volume)), (∀ (g : PiLp 2 fun (x : Fin 3) => ↥(MeasureTheory.Lp ℝ 2 MeasureTheory.volume)), ‖P g‖ ≤ ‖g‖) ∧ (∀ (g : PiLp 2 fun (x : Fin 3) => ↥(MeasureTheory.Lp ℝ 2 MeasureTheory.volume)), (∀ (φ : CKN.Foundation.Parabolic.Vec3 → ℝ), ContDiff ℝ (↑⊤) φ → HasCompactSupport φ → ∑ i : Fin 3, ∫ (x : CKN.Foundation.Parabolic.Vec3), ↑↑(g.ofLp i) x * CKN.spatialDeriv φ i x = 0) → P g = g) ∧ (∀ (g : PiLp 2 fun (x : Fin 3) => ↥(MeasureTheory.Lp ℝ 2 MeasureTheory.volume)) (φ : CKN.Foundation.Parabolic.Vec3 → ℝ), ContDiff ℝ (↑⊤) φ → HasCompactSupport φ → ∑ i : Fin 3, ∫ (x : CKN.Foundation.Parabolic.Vec3), ↑↑((P g).ofLp i) x * CKN.spatialDeriv φ i x = 0) ∧ (∀ (q : CKN.Foundation.Parabolic.Vec3 → ℝ) (G : PiLp 2 fun (x : Fin 3) => ↥(MeasureTheory.Lp ℝ 2 MeasureTheory.volume)), MeasureTheory.MemLp q 2 MeasureTheory.volume → (∀ (i : Fin 3), CKN.HasWeakPartialDerivOn Set.univ i q ↑↑(G.ofLp i)) → P G = 0) ∧ (∀ (g G : PiLp 2 fun (x : Fin 3) => ↥(MeasureTheory.Lp ℝ 2 MeasureTheory.volume)) (k : Fin 3), (∀ (i : Fin 3), CKN.HasWeakPartialDerivOn Set.univ k ↑↑(g.ofLp i) ↑↑(G.ofLp i)) → ∀ (i : Fin 3), CKN.HasWeakPartialDerivOn Set.univ k ↑↑((P g).ofLp i) ↑↑((P G).ofLp i)) ∧ ∀ (g h : PiLp 2 fun (x : Fin 3) => ↥(MeasureTheory.Lp ℝ 2 MeasureTheory.volume)), inner ℝ (P g) h = inner ℝ g (P h)

The Leray projection used in the proof of prop:lps-smoothing: on L²(ℝ³; ℝ³), realised as three L²(ℝ³) components, there is a bounded operator P (the orthogonal projection onto the weakly divergence-free fields) such that

• P is a contraction;
• P fixes every weakly divergence-free field;
• P g is weakly divergence-free for every g;
• P annihilates the gradient G of every q ∈ L²(ℝ³) whose weak gradient G is square integrable;
• P commutes with weak partial derivatives: if every component of g has weak k-th derivative the corresponding component of G, then every component of P g has weak k-th derivative the corresponding component of P G;
• P is self-adjoint.