Lin34Faithful #
Supporting estimates for the Navier–Stokes development.
The absolute constant controlling both solenoidal clauses of
prop:lin34.
Equations
Instances For
theorem
CKN.pressure_force_eq_zero_of_sws_spaceTimeDivergenceFree
{Ω : Set Foundation.Parabolic.Vec3}
{I : Set ℝ}
{q : ℝ}
{u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
{Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3}
{p : Foundation.Parabolic.ParabolicPoint → ℝ}
{f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
(hsol : IsSuitableWeakSolutionIntegrable Ω I q u Du p f)
{z : Foundation.Parabolic.ParabolicPoint}
{ρ : ℝ}
(hρ : 0 < ρ)
(hsub : closure (Foundation.Parabolic.parabolicCylinder z.1 z.2 ρ) ⊆ spaceTimeSet Ω I)
(hdiv :
∀ ψ ∈ spaceTimeTestFunction Ω I,
MeasureTheory.IntegrableOn
(fun (w : Foundation.Parabolic.ParabolicPoint) => ∑ i : Fin 3, f w i * spatialPartial ψ i w) (tsupport ψ)
MeasureTheory.volume ∧ ∫ (w : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Ω I, ∑ i : Fin 3, f w i * spatialPartial ψ i w = 0)
:
∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (z.2 - ρ ^ 2) z.2), lin34ForcePart f z.1 ρ hρ s =ᵐ[MeasureTheory.volume] 0
For almost every slice of a suitable weak solution, local distributional divergence on the spatial domain cancels the cutoff force potentials.
theorem
CKN.lin34_slice_pointwise_bound_ae_of_sws_spaceTimeDivergenceFree
{Ω : Set Foundation.Parabolic.Vec3}
{I : Set ℝ}
{q : ℝ}
{u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
{Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3}
{p : Foundation.Parabolic.ParabolicPoint → ℝ}
{f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
(hsol : IsSuitableWeakSolutionIntegrable Ω I q u Du p f)
{z : Foundation.Parabolic.ParabolicPoint}
{ρ r : ℝ}
(hρ : 0 < ρ)
(hr : 0 < r)
(hhalf : r ≤ ρ / 2)
(hsub : closure (Foundation.Parabolic.parabolicCylinder z.1 z.2 ρ) ⊆ spaceTimeSet Ω I)
(hdiv :
∀ ψ ∈ spaceTimeTestFunction Ω I,
MeasureTheory.IntegrableOn
(fun (w : Foundation.Parabolic.ParabolicPoint) => ∑ i : Fin 3, f w i * spatialPartial ψ i w) (tsupport ψ)
MeasureTheory.volume ∧ ∫ (w : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Ω I, ∑ i : Fin 3, f w i * spatialPartial ψ i w = 0)
:
The pointwise estimate of prop:lin34 follows from local divergence
because the force cutoff is supported inside the spatial domain.
theorem
CKN.pressure_lin34_of_sws
(q : ℝ)
{Ω : Set Foundation.Parabolic.Vec3}
{I : Set ℝ}
{u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
{Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3}
{p : Foundation.Parabolic.ParabolicPoint → ℝ}
{f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
:
IsSuitableWeakSolutionIntegrable Ω I q u Du p f →
∀ {z : Foundation.Parabolic.ParabolicPoint} {r ρ : ℝ},
0 < ρ →
0 < r →
r ≤ ρ / 2 →
closure (Foundation.Parabolic.parabolicCylinder z.1 z.2 ρ) ⊆ spaceTimeSet Ω I →
((∀ ψ ∈ spaceTimeTestFunction Ω I,
MeasureTheory.IntegrableOn
(fun (w : Foundation.Parabolic.ParabolicPoint) => ∑ i : Fin 3, f w i * spatialPartial ψ i w)
(tsupport ψ) MeasureTheory.volume ∧ ∫ (w : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Ω I, ∑ i : Fin 3, f w i * spatialPartial ψ i w = 0) →
(∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (z.2 - ρ ^ 2) z.2), r⁻¹ ^ 2 * ∫ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball z.1 r, |p (y, t)| ^ (3 / 2) ≤ lin34AbsoluteConstant * ((ρ / r) ^ 2 * (ρ⁻¹ ^ 2 * ∫ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball z.1 ρ, Foundation.Parabolic.vec3EuclideanNorm (meanFreeVec u z.1 ρ t y) ^ 3) + r / ρ * (ρ⁻¹ ^ 2 * ∫ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball z.1 ρ, |p (y, t)| ^ (3 / 2)))) ∧ pressureD p z r ≤ lin34AbsoluteConstant * ((ρ / r) ^ 2 * pressureChat u z ρ + r / ρ * pressureD p z ρ)) ∧ pressureD p z r ≤ Core.Endgame.theoremALin34Constant q * ((ρ / r) ^ 2 * pressureChat u z ρ + r / ρ * pressureD p z ρ + (r / ρ) ^ (3 / 2) * lambda q f z ρ ^ (3 / 2))
The three clauses of prop:lin34. The solenoidal clauses use the
local slice form of div f = 0 on Ω; the final clause is unconditional and
has the q-dependent force constant.