The Leray projection acting on triples of functions

prop:lps-smoothing: the projection of lps_leray_exists, fixed once and for all, acting on a vector field given by three square-integrable functions on ℝ³.

noncomputable def ESS.lpsLerayP : LpsL2Field →L[ℝ] LpsL2Field

The Leray projection of L²(ℝ³;ℝ³), a fixed choice from lps_leray_exists (prop:lps-smoothing).

Equations

• ESS.lpsLerayP = Classical.choose ESS.lps_leray_exists

theorem ESS.lpsLerayP_norm_le (g : LpsL2Field) : ‖lpsLerayP g‖ ≤ ‖g‖

theorem ESS.lpsLerayP_eq_self {g : LpsL2Field} (hg : ∀ (φ : CKN.Foundation.Parabolic.Vec3 → ℝ), ContDiff ℝ (↑⊤) φ → HasCompactSupport φ → ∑ i : Fin 3, ∫ (x : CKN.Foundation.Parabolic.Vec3), ↑↑(g.ofLp i) x * CKN.spatialDeriv φ i x = 0) : lpsLerayP g = g

theorem ESS.lpsLerayP_mem (g : LpsL2Field) (φ : CKN.Foundation.Parabolic.Vec3 → ℝ) (hφ : ContDiff ℝ (↑⊤) φ) (hφc : HasCompactSupport φ) : ∑ i : Fin 3, ∫ (x : CKN.Foundation.Parabolic.Vec3), ↑↑((lpsLerayP g).ofLp i) x * CKN.spatialDeriv φ i x = 0

theorem ESS.lpsLerayP_gradient {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)) : lpsLerayP G = 0

theorem ESS.lpsLerayP_weakPartial {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 ↑↑((lpsLerayP g).ofLp i) ↑↑((lpsLerayP G).ofLp i)

noncomputable def ESS.lpsFieldOf (g : Fin 3 → CKN.Foundation.Parabolic.Vec3 → ℝ) (hg : ∀ (j : Fin 3), MeasureTheory.MemLp (g j) 2 MeasureTheory.volume) : LpsL2Field

The field of three square-integrable functions as an element of L²(ℝ³;ℝ³).

Equations

• ESS.lpsFieldOf g hg = WithLp.toLp 2 fun (j : Fin 3) => MeasureTheory.MemLp.toLp (g j) ⋯

noncomputable def ESS.lpsLerayApply (g : Fin 3 → CKN.Foundation.Parabolic.Vec3 → ℝ) (hg : ∀ (j : Fin 3), MeasureTheory.MemLp (g j) 2 MeasureTheory.volume) (i : Fin 3) : CKN.Foundation.Parabolic.Vec3 → ℝ

The Leray projection of a vector field given by three square-integrable functions, as functions.

Equations

• ESS.lpsLerayApply g hg i = ↑↑((ESS.lpsLerayP (ESS.lpsFieldOf g hg)).ofLp i)

theorem ESS.lps_hasWeakPartialDerivOn_congr {U : Set CKN.Foundation.Parabolic.Vec3} {i : Fin 3} {f f' df df' : CKN.Foundation.Parabolic.Vec3 → ℝ} (hf : CKN.HasWeakPartialDerivOn U i f df) (hff' : f =ᵐ[MeasureTheory.volume.restrict U] f') (hdd : df =ᵐ[MeasureTheory.volume.restrict U] df') : CKN.HasWeakPartialDerivOn U i f' df'

Weak partial derivatives are insensitive to almost-everywhere changes of the function and of its derivative (prop:lps-smoothing).

theorem ESS.lpsLerayApply_eq {g : Fin 3 → CKN.Foundation.Parabolic.Vec3 → ℝ} (hg : ∀ (j : Fin 3), MeasureTheory.MemLp (g j) 2 MeasureTheory.volume) (i : Fin 3) : lpsLerayApply g hg i = ↑↑((lpsLerayP (lpsFieldOf g hg)).ofLp i)

theorem ESS.lpsLerayApply_memLp {g : Fin 3 → CKN.Foundation.Parabolic.Vec3 → ℝ} (hg : ∀ (j : Fin 3), MeasureTheory.MemLp (g j) 2 MeasureTheory.volume) (i : Fin 3) : MeasureTheory.MemLp (lpsLerayApply g hg i) 2 MeasureTheory.volume

theorem ESS.lpsLerayApply_congr_ae {g g' : Fin 3 → CKN.Foundation.Parabolic.Vec3 → ℝ} (hg : ∀ (j : Fin 3), MeasureTheory.MemLp (g j) 2 MeasureTheory.volume) (hg' : ∀ (j : Fin 3), MeasureTheory.MemLp (g' j) 2 MeasureTheory.volume) (hgg' : ∀ (j : Fin 3), g j =ᵐ[MeasureTheory.volume] g' j) (i : Fin 3) : lpsLerayApply g hg i =ᵐ[MeasureTheory.volume] lpsLerayApply g' hg' i

The projection only depends on the almost-everywhere class of the components.

theorem ESS.lpsLp_norm_sq_eq_integral (f : ↥(MeasureTheory.Lp ℝ 2 MeasureTheory.volume)) : ‖f‖ ^ 2 = ∫ (x : CKN.Foundation.Parabolic.Vec3), ↑↑f x ^ 2

Square integral of an L² class equals its squared norm.

theorem ESS.lpsLerayApply_normSq_le {g : Fin 3 → CKN.Foundation.Parabolic.Vec3 → ℝ} (hg : ∀ (j : Fin 3), MeasureTheory.MemLp (g j) 2 MeasureTheory.volume) : ∑ i : Fin 3, ∫ (x : CKN.Foundation.Parabolic.Vec3), lpsLerayApply g hg i x ^ 2 ≤ ∑ i : Fin 3, ∫ (x : CKN.Foundation.Parabolic.Vec3), g i x ^ 2

The projection is a contraction on square integrals of the components.

theorem ESS.lpsLerayApply_eq_self {g : Fin 3 → CKN.Foundation.Parabolic.Vec3 → ℝ} (hg : ∀ (j : Fin 3), MeasureTheory.MemLp (g j) 2 MeasureTheory.volume) (hdiv : ∀ (φ : CKN.Foundation.Parabolic.Vec3 → ℝ), ContDiff ℝ (↑⊤) φ → HasCompactSupport φ → ∑ i : Fin 3, ∫ (x : CKN.Foundation.Parabolic.Vec3), g i x * CKN.spatialDeriv φ i x = 0) (i : Fin 3) : lpsLerayApply g hg i =ᵐ[MeasureTheory.volume] g i

The projection fixes weakly divergence-free fields.

theorem ESS.lpsLerayApply_gradient {q : CKN.Foundation.Parabolic.Vec3 → ℝ} {G : Fin 3 → CKN.Foundation.Parabolic.Vec3 → ℝ} (hG : ∀ (j : Fin 3), MeasureTheory.MemLp (G j) 2 MeasureTheory.volume) (hq : MeasureTheory.MemLp q 2 MeasureTheory.volume) (hw : ∀ (i : Fin 3), CKN.HasWeakPartialDerivOn Set.univ i q (G i)) (i : Fin 3) : lpsLerayApply G hG i =ᵐ[MeasureTheory.volume] 0

The projection annihilates gradients of H¹ functions.

theorem ESS.lpsLerayApply_weakPartial {g G : Fin 3 → CKN.Foundation.Parabolic.Vec3 → ℝ} (hg : ∀ (j : Fin 3), MeasureTheory.MemLp (g j) 2 MeasureTheory.volume) (hG : ∀ (j : Fin 3), MeasureTheory.MemLp (G j) 2 MeasureTheory.volume) (k : Fin 3) (h : ∀ (j : Fin 3), CKN.HasWeakPartialDerivOn Set.univ k (g j) (G j)) (i : Fin 3) : CKN.HasWeakPartialDerivOn Set.univ k (lpsLerayApply g hg i) (lpsLerayApply G hG i)

The projection commutes with weak spatial derivatives.