Leray Hopf Limit Prop Energy

Supporting estimates for the Navier–Stokes development.

theorem CKN.Leray.lerayHopfLimit_ae_slice_memLp_of_spaceTime_memLp (T : ℝ) (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (hu : MeasureTheory.MemLp u 2 (MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo 0 T)))) : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 T), MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => WithLp.toLp 2 (u (x, t))) 2 MeasureTheory.volume

Space-time L² membership gives spatial L² membership on almost every time slice of a finite slab.

theorem CKN.Leray.lerayHopfLimit_regSlice_uniformBound (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (U : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (D : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3) (ha : MeasureTheory.MemLp (regUniformSpatialField a) 2 MeasureTheory.volume) (hUslice : ∀ (t : ℝ), 0 ≤ t → MeasureTheory.MemLp (regUniformVelocitySlice U t) 2 MeasureTheory.volume) (hR5 : ∀ (t : ℝ), 0 ≤ t → MeasureTheory.eLpNorm (regUniformVelocitySlice U t) 2 MeasureTheory.volume ^ 2 + 2 * regUniformDissipation U D t = MeasureTheory.eLpNorm (regMollifyVector ρ ε hε (regUniformSpatialField a)) 2 MeasureTheory.volume ^ 2) (t : ℝ) (ht : 0 ≤ t) : MeasureTheory.eLpNorm (fun (x : Foundation.Parabolic.Vec3) => WithLp.toLp 2 (U (x, t))) 2 MeasureTheory.volume ≤ MeasureTheory.eLpNorm (regUniformSpatialField a) 2 MeasureTheory.volume

The exact regularized energy identity and convolution contraction give a uniform spatial L² bound for every regularized slice.

theorem CKN.Leray.lerayHopfLimit_initialField_memLp (a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (ha : MeasureTheory.MemLp a 2 MeasureTheory.volume) : MeasureTheory.MemLp (regUniformSpatialField a) 2 MeasureTheory.volume

The coordinate L² datum has the Hilbert-carrier representative used by the regularized mollifier.

theorem CKN.Leray.lerayHopfLimit_slice_energy_essSup (T : ℝ) (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (U : ℕ → Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (B : ENNReal) (hB : B < ⊤) (hslice : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 T), MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => WithLp.toLp 2 (u (x, t))) 2 MeasureTheory.volume) (hU : ∀ (n : ℕ), ∀ t ∈ Set.Ioo 0 T, MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => WithLp.toLp 2 (U n (x, t))) 2 MeasureTheory.volume) (hUbound : ∀ (n : ℕ), ∀ t ∈ Set.Ioo 0 T, MeasureTheory.eLpNorm (fun (x : Foundation.Parabolic.Vec3) => WithLp.toLp 2 (U n (x, t))) 2 MeasureTheory.volume ≤ B) (hweak : ∀ (t : ℝ), 0 < t → ∀ (w : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3), MeasureTheory.MemLp w 2 MeasureTheory.volume → Filter.Tendsto (fun (n : ℕ) => ∫ (x : Foundation.Parabolic.Vec3), ∑ i : Fin 3, U n (x, t) i * w x i) Filter.atTop (nhds (∫ (x : Foundation.Parabolic.Vec3), ∑ i : Fin 3, u (x, t) i * w x i))) : essSup (fun (t : ℝ) => ∫⁻ (x : Foundation.Parabolic.Vec3), ‖u (x, t)‖ₑ ^ 2) (MeasureTheory.volume.restrict (Set.Ioo 0 T)) < ⊤

Uniform spatial L² bounds pass through weak convergence of every time slice, giving the essential supremum bound in (LH1).