The force pressure on one time slice

For a real spatial L² field f, the gradient field (I - ℙ) f of lem:force-pressure is an L² limit of test gradients. The homogeneous Sobolev inequality makes the test functions Cauchy in L⁶, and their limit is an L⁶ pressure with weak gradient (I - ℙ) f. The L⁶ function with a given weak gradient is unique: an L⁶ function with zero weak gradient vanishes almost everywhere.

theorem CKN.Leray.forcePressureTest_integral_mul_partialDeriv (φ ψ : WeakTestFunction Set.univ) (i : Fin 3) : ∫ (x : Vec 3), φ.toFun x * ψ.partialDeriv i x = -∫ (x : Vec 3), φ.partialDeriv i x * ψ.toFun x

Integration by parts between two whole-space test functions.

theorem CKN.Leray.forcePressureTest_hasWeakGradientOn (φ : WeakTestFunction Set.univ) : HasWeakGradientOn Set.univ φ.toFun (forcePressureTestGradient φ)

A whole-space test function has its classical gradient as weak gradient.

theorem CKN.Leray.forcePressureTest_eLpNorm_six_le (φ : WeakTestFunction Set.univ) : MeasureTheory.eLpNorm φ.toFun 6 MeasureTheory.volume ≤ gagliardoNirenbergSobolevConstant * MeasureTheory.eLpNorm (forcePressureTestGradient φ) 2 MeasureTheory.volume

The homogeneous Sobolev inequality for whole-space test functions.

theorem CKN.Leray.forcePressure_tendsto_integral_mul {p q : ENNReal} [p.HolderTriple q 1] {F : ℕ → Foundation.Parabolic.Vec3 → ℝ} {f h : Foundation.Parabolic.Vec3 → ℝ} (hF : ∀ (n : ℕ), MeasureTheory.MemLp (F n) p MeasureTheory.volume) (hf : MeasureTheory.MemLp f p MeasureTheory.volume) (hh : MeasureTheory.MemLp h q MeasureTheory.volume) (hlim : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (F n - f) p MeasureTheory.volume) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (n : ℕ) => ∫ (x : Foundation.Parabolic.Vec3), F n x * h x) Filter.atTop (nhds (∫ (x : Foundation.Parabolic.Vec3), f x * h x))

Pairings with a fixed L^q function pass to the limit along a sequence converging in the dual exponent.

theorem CKN.Leray.holderTriple_six_ofReal_sixFifths : ENNReal.HolderTriple 6 (ENNReal.ofReal (6 / 5)) 1

The exponents 6 and 6/5 are Hölder conjugate.

theorem CKN.Leray.gagliardoNirenbergSobolevConstant_ne_top : gagliardoNirenbergSobolevConstant ≠ ⊤

The chosen homogeneous Sobolev constant is finite.

theorem CKN.Leray.exists_forcePressureSlice (v : ↥RealVectorL2) : ∃ (p : Foundation.Parabolic.Vec3 → ℝ), MeasureTheory.MemLp p 6 MeasureTheory.volume ∧ MeasureTheory.eLpNorm p 6 MeasureTheory.volume ≤ gagliardoNirenbergSobolevConstant * MeasureTheory.eLpNorm (↑↑(forcePressureGradientL2 v)) 2 MeasureTheory.volume ∧ HasWeakGradientOn Set.univ p (realVectorL2Representative (forcePressureGradientL2 v))

Existence in lem:force-pressure on one time slice: for every real spatial L² field there is an L⁶ pressure whose weak gradient is the field (I - ℙ) f, with the homogeneous Sobolev bound.