Slice estimates for regularized Leray tails

Almost every positive-time Sobolev slice has the interpolation and pressure bounds needed for the quantitative flux estimate in lem:reg-tails.

theorem CKN.Leray.regTails_h1_component_L4 (v : H1Function Set.univ) : MeasureTheory.eLpNorm v.toFun (ENNReal.ofReal 4) MeasureTheory.volume ≤ gagliardoNirenbergSobolevConstant ^ (3 / 4) * MeasureTheory.eLpNorm v.toFun 2 MeasureTheory.volume ^ (1 / 4) * MeasureTheory.eLpNorm (fun (x : Vec 3) => Foundation.Parabolic.vec3EuclideanNorm (v.grad x)) 2 MeasureTheory.volume ^ (3 / 4)

Whole-space L⁴ control for an H¹ scalar component, obtained by interpolating the global Sobolev L⁶ estimate with L². This is used in the quantitative error bound in lem:reg-tails.

theorem CKN.Leray.regTails_gradient_slice_norm_eq_profile (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (D : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3) (t : ℝ) (ht : 0 < t) (hDcont : ∀ (i j : Fin 3), ContinuousOn (fun (z : Foundation.Parabolic.ParabolicPoint) => D z i j) (spaceTimeSet Set.univ (Set.Ioi 0))) (h : Fin 3 → H1Function Set.univ) (hGradients : ∀ (i : Fin 3) (x : Vec 3) (j : Fin 3), (h i).grad x j = D (x, t) i j) : (MeasureTheory.eLpNorm (fun (x : Foundation.Parabolic.Vec3) => √(spatialGradientSq u D (x, t))) 2 MeasureTheory.volume).toReal = √(∫⁻ (x : Foundation.Parabolic.Vec3), ENNReal.ofReal (spatialGradientSq u D (x, t))).toReal

On almost every Sobolev slice, the global gradient norm used in the time-integrated dissipation is the square-integrable size supplied by the explicit weak gradient.

theorem CKN.Leray.regTails_vector_slice_L4 (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (D : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3) (t : ℝ) (h : Fin 3 → H1Function Set.univ) (hValues : ∀ (i : Fin 3) (x : Vec 3), (h i).toFun x = u (x, t) i) (hGradients : ∀ (i : Fin 3) (x : Vec 3) (j : Fin 3), (h i).grad x j = D (x, t) i j) (hU : MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => u (x, t)) 2 MeasureTheory.volume) : MeasureTheory.eLpNorm (fun (x : Foundation.Parabolic.Vec3) => Foundation.Parabolic.vec3EuclideanNorm (u (x, t))) (ENNReal.ofReal 4) MeasureTheory.volume ≤ 3 * gagliardoNirenbergSobolevConstant ^ (3 / 4) * MeasureTheory.eLpNorm (fun (x : Foundation.Parabolic.Vec3) => Foundation.Parabolic.vec3EuclideanNorm (u (x, t))) 2 MeasureTheory.volume ^ (1 / 4) * MeasureTheory.eLpNorm (fun (x : Foundation.Parabolic.Vec3) => √(spatialGradientSq u D (x, t))) 2 MeasureTheory.volume ^ (3 / 4)

Almost every regularized velocity slice satisfies the L⁴ Gagliardo–Nirenberg bound needed for the convection and pressure terms in lem:reg-tails.

theorem CKN.Leray.regTails_mollified_velocity_slice_L4 (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (t : ℝ) (hU2 : MeasureTheory.MemLp (regUniformVelocitySlice u t) 2 MeasureTheory.volume) (hU4 : MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => Foundation.Parabolic.vec3EuclideanNorm (u (x, t))) (ENNReal.ofReal 4) MeasureTheory.volume) : MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => Foundation.Parabolic.vec3EuclideanNorm (regUniformMollifiedVelocity ρ ε hε u (x, t))) (ENNReal.ofReal 4) MeasureTheory.volume ∧ MeasureTheory.eLpNorm (fun (x : Foundation.Parabolic.Vec3) => Foundation.Parabolic.vec3EuclideanNorm (regUniformMollifiedVelocity ρ ε hε u (x, t))) (ENNReal.ofReal 4) MeasureTheory.volume ≤ MeasureTheory.eLpNorm (fun (x : Foundation.Parabolic.Vec3) => Foundation.Parabolic.vec3EuclideanNorm (u (x, t))) (ENNReal.ofReal 4) MeasureTheory.volume

The Riesz pressure representative has a slice L² estimate controlled by the fourth-power velocity norms.

theorem CKN.Leray.regTails_mollified_velocity_slice_L2 (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (t : ℝ) (hU2 : MeasureTheory.MemLp (regUniformVelocitySlice u t) 2 MeasureTheory.volume) : MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => Foundation.Parabolic.vec3EuclideanNorm (regUniformMollifiedVelocity ρ ε hε u (x, t))) 2 MeasureTheory.volume ∧ MeasureTheory.eLpNorm (fun (x : Foundation.Parabolic.Vec3) => Foundation.Parabolic.vec3EuclideanNorm (regUniformMollifiedVelocity ρ ε hε u (x, t))) 2 MeasureTheory.volume ≤ MeasureTheory.eLpNorm (fun (x : Foundation.Parabolic.Vec3) => Foundation.Parabolic.vec3EuclideanNorm (u (x, t))) 2 MeasureTheory.volume

Convolution does not increase the Euclidean slice L² norm of the regularized velocity.

theorem CKN.Leray.regTails_pressure_slice_norm_bound (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (p : Foundation.Parabolic.ParabolicPoint → ℝ) (hU2 : ∀ (t : ℝ), 0 ≤ t → MeasureTheory.MemLp (regUniformVelocitySlice u t) 2 MeasureTheory.volume) (hUbound : ∀ (t : ℝ), 0 < t → ∃ (B : ℝ), 0 ≤ B ∧ ∀ (x : Foundation.Parabolic.Vec3), Foundation.Parabolic.vec3EuclideanNorm (u (x, t)) ≤ B) (hR4 : ∀ (t : ℝ), 0 < t → ∃ (hF : ∀ (i j : Fin 3), MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => regUniformMollifiedVelocity ρ ε hε u (x, t) i * u (x, t) j) (ENNReal.ofReal 2) MeasureTheory.volume), (fun (x : Foundation.Parabolic.Vec3) => p (x, t)) =ᵐ[MeasureTheory.volume] rieszPressureSliceRepresentative 2 regTails_pressure_slice_norm_bound._proof_1 fun (i j : Fin 3) => MeasureTheory.MemLp.toLp (fun (x : Foundation.Parabolic.Vec3) => regUniformMollifiedVelocity ρ ε hε u (x, t) i * u (x, t) j) ⋯) (t : ℝ) : 0 < t → (MeasureTheory.eLpNorm (fun (x : Foundation.Parabolic.Vec3) => p (x, t)) (ENNReal.ofReal 2) MeasureTheory.volume).toReal ≤ 9 * rieszPressureOperatorBound 2 regTails_pressure_slice_norm_bound._proof_1 * (MeasureTheory.eLpNorm (fun (x : Foundation.Parabolic.Vec3) => Foundation.Parabolic.vec3EuclideanNorm (regUniformMollifiedVelocity ρ ε hε u (x, t))) (ENNReal.ofReal 4) MeasureTheory.volume).toReal * (MeasureTheory.eLpNorm (fun (x : Foundation.Parabolic.Vec3) => Foundation.Parabolic.vec3EuclideanNorm (u (x, t))) (ENNReal.ofReal 4) MeasureTheory.volume).toReal

The Riesz pressure representative has a slice L² estimate controlled by the fourth-power velocity norms.