Reg Tails Slice Flux #
Supporting estimates for the Navier–Stokes development.
theorem
CKN.Leray.regTails_slice_flux_density_integrable
(u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3)
(D : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3)
(p : Foundation.Parabolic.ParabolicPoint → ℝ)
(J : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3)
(t : ℝ)
(q : Foundation.Parabolic.Vec3 → ℝ)
(hq : ContDiff ℝ (↑⊤) q)
(hqc : HasCompactSupport q)
(hUcont : ∀ (i : Fin 3), Continuous fun (x : Foundation.Parabolic.Vec3) => u (x, t) i)
(hDcont : ∀ (i j : Fin 3), Continuous fun (x : Foundation.Parabolic.Vec3) => D (x, t) i j)
(hPcont : Continuous fun (x : Foundation.Parabolic.Vec3) => p (x, t))
(hJcont : ∀ (j : Fin 3), Continuous fun (x : Foundation.Parabolic.Vec3) => J (x, t) j)
:
MeasureTheory.Integrable
(fun (x : Foundation.Parabolic.Vec3) =>
2 * ∑ i : Fin 3, ∑ j : Fin 3, |u (x, t) i| * |D (x, t) i j| * |spatialDeriv q j x| + ∑ j : Fin 3,
(Foundation.Parabolic.vec3EuclideanNorm (u (x, t)) ^ 2 * |J (x, t) j| + 2 * |p (x, t)| * |u (x, t) j|) * |spatialDeriv q j x|)
MeasureTheory.volume
A compact smooth spatial weight makes the nonnegative localized flux density integrable on each positive-time slice.
theorem
CKN.Leray.regTails_slice_flux_bound
(ρ : RegMollifierProfile)
(ε : ℝ)
(hε : 0 < ε)
(u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3)
(p : Foundation.Parabolic.ParabolicPoint → ℝ)
(hU2 : ∀ (s : ℝ), 0 ≤ s → MeasureTheory.MemLp (regUniformVelocitySlice u s) 2 MeasureTheory.volume)
(hUbound :
∀ (s : ℝ),
0 < s → ∃ (K : ℝ), 0 ≤ K ∧ ∀ (x : Foundation.Parabolic.Vec3), Foundation.Parabolic.vec3EuclideanNorm (u (x, s)) ≤ K)
(hR4 :
∀ (s : ℝ),
0 < s →
∃ (hF :
∀ (i j : Fin 3),
MeasureTheory.MemLp
(fun (x : Foundation.Parabolic.Vec3) => regUniformMollifiedVelocity ρ ε hε u (x, s) i * u (x, s) j)
(ENNReal.ofReal 2) MeasureTheory.volume),
(fun (x : Foundation.Parabolic.Vec3) => p (x, s)) =ᵐ[MeasureTheory.volume]
rieszPressureSliceRepresentative 2 regTails_slice_flux_bound._proof_1 fun (i j : Fin 3) =>
MeasureTheory.MemLp.toLp
(fun (x : Foundation.Parabolic.Vec3) => regUniformMollifiedVelocity ρ ε hε u (x, s) i * u (x, s) j) ⋯)
(t : ℝ)
(ht : 0 < t)
(hU : MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => u (x, t)) 2 MeasureTheory.volume)
(hH1 :
∃ (h : Fin 3 → H1Function Set.univ),
(∀ (i : Fin 3) (x : Vec 3), (h i).toFun x = u (x, t) i) ∧ ∀ (i : Fin 3) (x : Vec 3) (j : Fin 3),
(h i).grad x j = spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => u y i) j (x, t))
(B G M : ℝ)
(hB : 0 ≤ B)
(hG : 0 ≤ G)
(hM : 0 ≤ M)
(hUboundL2 :
(MeasureTheory.eLpNorm (fun (x : Foundation.Parabolic.Vec3) => Foundation.Parabolic.vec3EuclideanNorm (u (x, t))) 2
MeasureTheory.volume).toReal ≤ B)
(hGdef :
(MeasureTheory.eLpNorm
(fun (x : Foundation.Parabolic.Vec3) =>
√(spatialGradientSq u
(fun (z : Foundation.Parabolic.ParabolicPoint) (i j : Fin 3) =>
spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => u y i) j z)
(x, t)))
2 MeasureTheory.volume).toReal = G)
(q : Foundation.Parabolic.Vec3 → ℝ)
(hq : ContDiff ℝ (↑⊤) q)
(hDq : ∀ (x : Foundation.Parabolic.Vec3) (j : Fin 3), |spatialDeriv q j x| ≤ M)
:
∫ (x : Foundation.Parabolic.Vec3), 2 * ∑ i : Fin 3,
∑ j : Fin 3,
|u (x, t) i| * |spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => u y i) j (x, t)| * |spatialDeriv q j x| + ∑ j : Fin 3,
(Foundation.Parabolic.vec3EuclideanNorm (u (x, t)) ^ 2 * |regUniformMollifiedVelocity ρ ε hε u (x, t) j| + 2 * |p (x, t)| * |u (x, t) j|) * |spatialDeriv q j x| ≤ 18 * M * B * G + (27 * gagliardoNirenbergSobolevConstant.toReal ^ (3 / 2) + 486 * rieszPressureOperatorBound 2 regTails_slice_flux_bound._proof_1 * gagliardoNirenbergSobolevConstant.toReal ^ (3 / 2)) * M * B ^ (3 / 2) * G ^ (3 / 2)
The localized flux density in lem:reg-tails is controlled by the
slice energy and dissipation profiles.