The pressure limit for the forced regularized problems

The forced regularized pressure is the quadratic Riesz pressure of the regularized transport tensor plus the fixed force pressure of lem:force-pressure. The force part is the same field for every ε, so the pressure limit of thm:leray-forced reduces to the quadratic part: on every finite slab the quadratic pressures converge in L^{3/2} to the Riesz pressure of u ⊗ u (prop:leray-pressure-limit), and the limit pressure is that glued quadratic pressure plus the force pressure.

theorem CKN.Leray.forcedPressureLimit_quadratic_eq_product (P : Foundation.Parabolic.ParabolicPoint → ℝ) (U J : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (T : ℝ) (hPmeas : MeasureTheory.AEStronglyMeasurable (fun (z : Foundation.Parabolic.Vec3 × ℝ) => P (Foundation.Parabolic.parabolicHomeomorph.symm z)) (MeasureTheory.volume.restrict (lerayPressureLimitSlab T))) (hR4 : ∀ (t : ℝ), 0 < t → ∃ (hF : ∀ (i j : Fin 3), MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => J (x, t) i * U (x, t) j) (ENNReal.ofReal 2) MeasureTheory.volume), (fun (x : Foundation.Parabolic.Vec3) => P (x, t)) =ᵐ[MeasureTheory.volume] rieszPressureSliceRepresentative 2 forcedPressureLimit_quadratic_eq_product._proof_1 fun (i j : Fin 3) => MeasureTheory.MemLp.toLp (fun (x : Foundation.Parabolic.Vec3) => J (x, t) i * U (x, t) j) ⋯) (hU : MeasureTheory.MemLp (fun (z : Foundation.Parabolic.Vec3 × ℝ) => U (Foundation.Parabolic.parabolicHomeomorph.symm z)) 3 (MeasureTheory.volume.restrict (lerayPressureLimitSlab T))) (hJ : MeasureTheory.MemLp (fun (z : Foundation.Parabolic.Vec3 × ℝ) => J (Foundation.Parabolic.parabolicHomeomorph.symm z)) 3 (MeasureTheory.volume.restrict (lerayPressureLimitSlab T))) : (fun (z : Foundation.Parabolic.Vec3 × ℝ) => P (Foundation.Parabolic.parabolicHomeomorph.symm z)) =ᵐ[MeasureTheory.volume.restrict (lerayPressureLimitSlab T)] lerayProductPressureOnSlab T (fun (z : Foundation.Parabolic.Vec3 × ℝ) => J (Foundation.Parabolic.parabolicHomeomorph.symm z)) (fun (z : Foundation.Parabolic.Vec3 × ℝ) => U (Foundation.Parabolic.parabolicHomeomorph.symm z)) hJ hU

A quadratic pressure that is almost everywhere measurable on a finite slab and is the Riesz pressure of J ⊗ U on every positive time slice agrees almost everywhere on the slab with the space-time product pressure.

theorem CKN.Leray.forcedPressureLimit_of_regularised_pressure_data (ρ : RegMollifierProfile) (pF : (f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) → IsLocallySquareIntegrableForce f → Foundation.Parabolic.ParabolicPoint → ℝ) (uε : (a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) → IsInJ a → (f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) → IsLocallySquareIntegrableForce f → ℝ → Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (pε : (a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) → IsInJ a → (f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) → IsLocallySquareIntegrableForce f → ℝ → Foundation.Parabolic.ParabolicPoint → ℝ) (hregularised : ∀ (a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (ha : IsInJ a) (f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (hf : IsLocallySquareIntegrableForce f) (ε : ℝ) (hε : 0 < ε), (∀ (T : ℝ), 0 < T → MeasureTheory.MemLp (fun (z : Foundation.Parabolic.ParabolicPoint) => pε a ha f hf ε z - pF f hf z) 2 (MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo 0 T)))) ∧ ∀ (t : ℝ), 0 < t → ∃ (hF : ∀ (i j : Fin 3), MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => regUniformMollifiedVelocity ρ ε hε (uε a ha f hf ε) (x, t) i * uε a ha f hf ε (x, t) j) (ENNReal.ofReal 2) MeasureTheory.volume), (fun (x : Foundation.Parabolic.Vec3) => pε a ha f hf ε (x, t) - pF f hf (x, t)) =ᵐ[MeasureTheory.volume] rieszPressureSliceRepresentative 2 forcedPressureLimit_quadratic_eq_product._proof_1 fun (i j : Fin 3) => MeasureTheory.MemLp.toLp (fun (x : Foundation.Parabolic.Vec3) => regUniformMollifiedVelocity ρ ε hε (uε a ha f hf ε) (x, t) i * uε a ha f hf ε (x, t) j) ⋯) (hlerayLimit : ∀ (a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (ha : IsInJ a) (f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (hf : IsLocallySquareIntegrableForce f) (εseq : ℕ → ℝ), (∀ (n : ℕ), 0 < εseq n ∧ εseq n ≤ 1) → Filter.Tendsto εseq Filter.atTop (nhds 0) → ∃ (τ : ℕ → ℕ), StrictMono τ ∧ Filter.Tendsto τ Filter.atTop Filter.atTop ∧ ∀ (T : ℝ), 0 < T → ∀ (n : ℕ), MeasureTheory.MemLp (uε a ha f hf (εseq (τ n))) 3 (MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo 0 T)))) (a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (ha : IsInJ a) (f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (hf : IsLocallySquareIntegrableForce f) (εseq : ℕ → ℝ) (hseq : ∀ (n : ℕ), 0 < εseq n ∧ εseq n ≤ 1) (σ : ℕ → ℕ) (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (hεsubseq : Filter.Tendsto (fun (n : ℕ) => εseq (σ n)) Filter.atTop (nhds 0)) (hUseqLthree : ∀ (T : ℝ), 0 < T → Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (uε a ha f hf (εseq (σ n)) - u) (ENNReal.ofReal 3) (MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo 0 T)))) Filter.atTop (nhds 0)) (hJseqLthree : ∀ (T : ℝ), 0 < T → Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (regUniformMollifiedVelocity ρ (εseq (σ n)) ⋯ (uε a ha f hf (εseq (σ n))) - u) (ENNReal.ofReal 3) (MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo 0 T)))) Filter.atTop (nhds 0)) : ∃ (p : Foundation.Parabolic.ParabolicPoint → ℝ), ∀ (T : ℝ), 0 < T → let μ := MeasureTheory.volume.restrict (lerayPressureLimitSlab T); let uST := fun (z : Foundation.Parabolic.Vec3 × ℝ) => u (Foundation.Parabolic.parabolicHomeomorph.symm z); have pST := fun (z : Foundation.Parabolic.Vec3 × ℝ) => p (Foundation.Parabolic.parabolicHomeomorph.symm z); have pFST := fun (z : Foundation.Parabolic.Vec3 × ℝ) => pF f hf (Foundation.Parabolic.parabolicHomeomorph.symm z); have pseq := fun (n : ℕ) (z : Foundation.Parabolic.Vec3 × ℝ) => pε a ha f hf (εseq (σ n)) (Foundation.Parabolic.parabolicHomeomorph.symm z); ∃ (hu : MeasureTheory.MemLp uST 3 μ), MeasureTheory.MemLp (pST - pFST) (ENNReal.ofReal (3 / 2)) μ ∧ pST - pFST =ᵐ[μ] lerayProductPressureOnSlab T uST uST hu hu ∧ Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (pseq n - pST) (ENNReal.ofReal (3 / 2)) μ) Filter.atTop (nhds 0)

The pressure limit of thm:leray-forced. The quadratic parts p_ε − p_f of the forced regularized pressures are almost everywhere measurable on finite slabs and are the Riesz pressures of the regularized tensors on positive time slices (lem:regularised-forced); along every sequence ε → 0 a further subsequence of the forced regularized velocities lies in L³ on finite slabs (prop:forced-limit). Then, whenever the velocities and their mollifications converge in L³ on finite slabs to u, the pressures converge in L^{3/2} on finite slabs to p, where p − p_f is the Riesz pressure of u ⊗ u (prop:leray-pressure-limit).