The force pressure

This file proves lem:force-pressure in the form used by the forced Leray existence assembly: for a force that is square integrable on every finite slab, there is a jointly measurable pressure p_f with p_f(·, t) ∈ L⁶ and weak gradient (I - ℙ) f(·, t) for almost every time, with p_f ∈ L²_t L⁶_x on every slab and the local bound eq:force-pressure-local.

theorem CKN.Leray.eLpNorm_realVectorL2OfCoordinateFunction_le (a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (ha : MeasureTheory.MemLp a 2 MeasureTheory.volume) : MeasureTheory.eLpNorm (↑↑(realVectorL2OfCoordinateFunction a ha)) 2 MeasureTheory.volume ≤ 2 * MeasureTheory.eLpNorm a 2 MeasureTheory.volume

The Hilbert field transferred from a coordinate L² field has at most twice its L² norm.

theorem CKN.Leray.forcePressureSliceOfField_eLpNorm_le (F : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3) (t : ℝ) : MeasureTheory.eLpNorm (forcePressureSliceOfField F t) 6 MeasureTheory.volume ≤ 4 * gagliardoNirenbergSobolevConstant * MeasureTheory.eLpNorm (fun (x : Foundation.Parabolic.Vec3) => F (x, t)) 2 MeasureTheory.volume

The slice force pressure of a field is bounded in L⁶ by the L² norm of the time slice.

theorem CKN.Leray.lintegral_eLpNorm_slice_sq_eq {μt : MeasureTheory.Measure ℝ} [MeasureTheory.SFinite μt] {F : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3} (hF : MeasureTheory.StronglyMeasurable F) : ∫⁻ (t : ℝ), MeasureTheory.eLpNorm (fun (x : Foundation.Parabolic.Vec3) => F (x, t)) 2 MeasureTheory.volume ^ 2 ∂μt = MeasureTheory.eLpNorm F 2 (MeasureTheory.volume.prod μt) ^ 2

Tonelli's formula for the squared L² norm on a product with a time measure, slice by slice.

theorem CKN.Leray.exists_forcePressure (f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (hf : IsLocallySquareIntegrableForce f) : ∃ (P : Foundation.Parabolic.Vec3 × ℝ → ℝ), MeasureTheory.StronglyMeasurable P ∧ ∀ (T : ℝ), 0 < T → ∫⁻ (t : ℝ) in Set.Ioo 0 T, MeasureTheory.eLpNorm (fun (x : Foundation.Parabolic.Vec3) => P (x, t)) (ENNReal.ofReal 6) MeasureTheory.volume ^ 2 < ⊤ ∧ ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 T), ∃ (hft : MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => f (x, t)) 2 MeasureTheory.volume), HasWeakGradientOn Set.univ (fun (x : Foundation.Parabolic.Vec3) => P (x, t)) fun (x : Vec 3) (i : Fin 3) => forcePressureGradientFunction (fun (y : Foundation.Parabolic.Vec3) => f (y, t)) hft x i

Existence in lem:force-pressure: a strongly measurable pressure whose time slices lie in L²_t L⁶_x on every slab and have weak gradient (I - ℙ) f(·, t) for almost every time.

noncomputable def CKN.Leray.forcePressure (f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (hf : IsLocallySquareIntegrableForce f) : Foundation.Parabolic.ParabolicPoint → ℝ

The force pressure p_f of lem:force-pressure: a jointly measurable pressure whose time slices are the L⁶ pressures with weak gradient (I - ℙ) f(·, t).

Equations

• CKN.Leray.forcePressure f hf = Classical.choose ⋯

theorem CKN.Leray.forcePressure_spec (f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (hf : IsLocallySquareIntegrableForce f) (T : ℝ) : 0 < T → MeasureTheory.AEStronglyMeasurable (forcePressure f hf) (MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo 0 T))) ∧ ∫⁻ (t : ℝ) in Set.Ioo 0 T, MeasureTheory.eLpNorm (fun (x : Foundation.Parabolic.Vec3) => forcePressure f hf (x, t)) (ENNReal.ofReal 6) MeasureTheory.volume ^ 2 < ⊤ ∧ (∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 T), ∃ (hft : MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => f (x, t)) 2 MeasureTheory.volume), HasWeakGradientOn Set.univ (fun (x : Foundation.Parabolic.Vec3) => forcePressure f hf (x, t)) fun (x : Vec 3) (i : Fin 3) => forcePressureGradientFunction (fun (y : Foundation.Parabolic.Vec3) => f (y, t)) hft x i) ∧ ∀ (K : Set Foundation.Parabolic.Vec3) (I : Set ℝ), MeasurableSet K → MeasurableSet I → I ⊆ Set.Ioo 0 T → MeasureTheory.eLpNorm (forcePressure f hf) (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (spaceTimeSet K I)) ≤ MeasureTheory.volume K ^ (1 / 2) * MeasureTheory.volume I ^ (1 / 6) * (∫⁻ (t : ℝ) in Set.Ioo 0 T, MeasureTheory.eLpNorm (fun (x : Foundation.Parabolic.Vec3) => forcePressure f hf (x, t)) (ENNReal.ofReal 6) MeasureTheory.volume ^ 2) ^ (1 / 2)

lem:force-pressure, with eq:force-pressure-identities and eq:force-pressure-local, in the form of the force-pressure input of the forced Leray existence assembly: on every slab the force pressure is measurable, lies in L²_t L⁶_x, has weak gradient (I - ℙ) f(·, t) for almost every time, and satisfies the local L^{3/2} bound on every cylinder.