Leray Pressure Prop #
Supporting estimates for the Navier–Stokes development.
noncomputable def
CKN.Leray.lerayPressurePropGlue
(q : ℕ → Foundation.Parabolic.Vec3 × ℝ → ℝ)
(z : Foundation.Parabolic.Vec3 × ℝ)
:
Pressure assembled from the local representatives by telescoping their time increments.
Equations
Instances For
theorem
CKN.Leray.lerayPressureProp_of_regularised_pressure_data
(ρ : RegMollifierProfile)
(uε :
(a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) →
IsInJ a → ℝ → Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3)
(pε :
(a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) → IsInJ a → ℝ → Foundation.Parabolic.ParabolicPoint → ℝ)
(hregularised :
∀ (a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (ha : IsInJ a) (ε : ℝ) (hε : 0 < ε),
ContinuousOn (pε a ha ε) (spaceTimeSet Set.univ (Set.Ioi 0)) ∧ ∀ (t : ℝ),
0 < t →
∃ (hF :
∀ (i j : Fin 3),
MeasureTheory.MemLp
(fun (x : Foundation.Parabolic.Vec3) =>
regUniformMollifiedVelocity ρ ε hε (uε a ha ε) (x, t) i * uε a ha ε (x, t) j)
(ENNReal.ofReal 2) MeasureTheory.volume),
(fun (x : Foundation.Parabolic.Vec3) => pε a ha ε (x, t)) =ᵐ[MeasureTheory.volume]
rieszPressureSliceRepresentative 2 lerayPressureProp_of_regularised_pressure_data._proof_1
fun (i j : Fin 3) =>
MeasureTheory.MemLp.toLp
(fun (x : Foundation.Parabolic.Vec3) =>
regUniformMollifiedVelocity ρ ε hε (uε a ha ε) (x, t) i * uε a ha ε (x, t) j)
⋯)
(hlerayLimit :
∀ (a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (ha : IsInJ a) (ε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 (εseq (τ n))) 3
(MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo 0 T))))
(a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3)
(ha : IsInJ a)
(ε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 (ε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 (ε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 pseq := fun (n : ℕ) (z : Foundation.Parabolic.Vec3 × ℝ) =>
pε a ha (εseq (σ n)) (Foundation.Parabolic.parabolicHomeomorph.symm z);
∃ (hu : MeasureTheory.MemLp uST 3 μ),
MeasureTheory.MemLp pST (ENNReal.ofReal (3 / 2)) μ ∧ pST =ᵐ[μ] lerayProductPressureOnSlab T uST uST hu hu ∧ Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (pseq n - pST) (ENNReal.ofReal (3 / 2)) μ) Filter.atTop
(nhds 0)
The regularized pressure clause and the further-subsequence L³
membership clause imply prop:leray-pressure-limit on every finite slab.