Leray Hopf Limit Prop Class

Supporting estimates for the Navier–Stokes development.

theorem CKN.Leray.lerayHopfLimit_joint_lintegral_finite {α : Type u_1} {E : Type u_2} {F : Type u_3} [MeasurableSpace α] [NormedAddCommGroup E] [NormedAddCommGroup F] (μ : MeasureTheory.Measure α) (u : α → E) (D : α → F) (hu : MeasureTheory.MemLp u 2 μ) (hD : MeasureTheory.MemLp D 2 μ) : ∫⁻ (x : α), ‖u x‖ₑ ^ 2 + ‖D x‖ₑ ^ 2 ∂μ < ⊤

Space-time L² membership of the velocity and gradient gives the joint energy integrability in (LH1) of def:leray-hopf.

theorem CKN.Leray.lerayHopfLimit_divergence_of_weakSlice (U : ℕ → Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (u : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (hdiv : ∀ (n : ℕ), IsWeakDivFreeL2 (U n)) (hweak : ∀ (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 i * w x i) Filter.atTop (nhds (∫ (x : Foundation.Parabolic.Vec3), ∑ i : Fin 3, u x i * w x i))) (ψ : WeakTestFunction Set.univ) : ∫ (x : Foundation.Parabolic.Vec3), ∑ i : Fin 3, u x i * ψ.partialDeriv i x = 0

The divergence condition in (LH1) is closed under the all-time weak slice convergence in prop:leray-limit.

theorem CKN.Leray.lerayHopfLimit_LH1_core (T : ℝ) (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3) (U : ℕ → Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (humeas : MeasureTheory.AEStronglyMeasurable u (MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo 0 T)))) (hDmeas : MeasureTheory.AEStronglyMeasurable Du (MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo 0 T)))) (hu : MeasureTheory.MemLp u 2 (MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo 0 T)))) (hDu : MeasureTheory.MemLp Du 2 (MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo 0 T)))) (hgradient : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 T), ∀ (i : Fin 3), HasWeakGradientOn Set.univ (fun (x : Vec 3) => u (x, s) i) fun (x : Vec 3) => Du (x, s) i) (hdivU : ∀ (n : ℕ) (t : ℝ), 0 ≤ t → IsWeakDivFreeL2 fun (x : Foundation.Parabolic.Vec3) => U n (x, t)) (hweakSlice : ∀ (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))) : MeasureTheory.AEStronglyMeasurable u (MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo 0 T))) ∧ MeasureTheory.AEStronglyMeasurable Du (MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo 0 T))) ∧ ∫⁻ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Set.univ (Set.Ioo 0 T), ‖u z‖ₑ ^ 2 + ‖Du z‖ₑ ^ 2 < ⊤ ∧ (∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 T), ∀ (i : Fin 3), HasWeakGradientOn Set.univ (fun (x : Vec 3) => u (x, s) i) fun (x : Vec 3) => Du (x, s) i) ∧ ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 T), ∀ (ψ : WeakTestFunction Set.univ), ∫ (x : Foundation.Parabolic.Vec3), ∑ i : Fin 3, u (x, s) i * ψ.partialDeriv i x = 0

The measurable, finite-energy, weak-gradient, and divergence clauses of (LH1) follow from the space-time limit and its all-time weak slice pairings.