Finite Serrin control of a strong solution #
A strong solution has uniformly bounded gradient L² norms on its closed time
interval, so the whole-space Sobolev inequality bounds the L⁶ norm of the
velocity uniformly in time. This is the finite Serrin condition with s = 6,
ℓ = 4 used to compare two strong solutions (prop:lps-local-strong).
theorem
ESS.lps_strong_solution_slice_h1
{t₀ T t : ℝ}
{u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
{Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3}
{p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ}
(hU : IsLpsStrongSolution t₀ T u Du p)
(ht : t ∈ Set.Icc t₀ T)
:
MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, t)) 2 MeasureTheory.volume ∧ MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => Du (x, t)) 2 MeasureTheory.volume ∧ ∀ (i : Fin 3),
∃ (h : CKN.H1Function Set.univ),
(h.toFun = fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, t) i) ∧ h.grad = fun (x : CKN.Foundation.Parabolic.Vec3) (j : Fin 3) => Du (x, t) i j
Each time slice of a strong solution has square-integrable velocity and
gradient, with the componentwise H¹ representation.
theorem
ESS.lps_strong_solution_gradient_bound
{t₀ T : ℝ}
{u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
{Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3}
{p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ}
(hU : IsLpsStrongSolution t₀ T u Du p)
:
∃ (M : ℝ),
∀ t ∈ Set.Icc t₀ T,
(MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => Du (x, t)) 2 MeasureTheory.volume).toReal ≤ M
The gradient L² norms of a strong solution are bounded on its closed
time interval.
theorem
ESS.lps_strong_solution_l6_bound
{t₀ T : ℝ}
{u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
{Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3}
{p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ}
(hU : IsLpsStrongSolution t₀ T u Du p)
:
∃ (C : ENNReal),
C ≠ ⊤ ∧ ∀ t ∈ Set.Icc t₀ T,
∫⁻ (x : CKN.Foundation.Parabolic.Vec3), ENNReal.ofReal (CKN.Foundation.Parabolic.vec3EuclideanNorm (u (x, t))) ^ 6 ≤ C
The L⁶ norms of the velocity of a strong solution are bounded on its
closed time interval.
theorem
ESS.lps_strong_solution_serrin_finite
{t₀ T σ : ℝ}
{u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
{Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3}
{p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ}
(hU : IsLpsStrongSolution t₀ T u Du p)
(hσT : σ ≤ T - t₀)
:
A strong solution satisfies the finite Serrin condition with s = 6 on
every time interval inside its lifespan (prop:lps-local-strong and
thm:lps).