The H¹ estimate for strong solutions #
Source-facing forms of lem:lps-H1-estimate: a strong solution with finite
Serrin norm has its gradient energy plus the integrated Laplacian energy
bounded by the initial gradient energy times an exponential of the Serrin
norm. The chain-rule identity is supplied by the H¹ energy identity of
prop:lps-local-strong.
theorem
ESS.lps_h1_estimate
{s : ℝ}
(hs : 3 < s)
:
∃ (C : ℝ),
0 ≤ C ∧ ∀ {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 → ℝ},
IsLpsStrongSolution t₀ t₁ u Du p →
∫⁻ (t : ℝ) in Set.Ioo t₀ t₁, (∫⁻ (x : CKN.Foundation.Parabolic.Vec3), ENNReal.ofReal (CKN.Foundation.Parabolic.vec3EuclideanNorm (u (x, t))) ^ s) ^ (2 * s / (s - 3) / s) < ⊤ →
∃ (D2u : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3) (Dtu :
CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3),
CKN.HasSpaceTimeWeakDerivs Set.univ (Set.Ioo t₀ t₁) u Du D2u Dtu ∧ MeasureTheory.MemLp D2u 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo t₀ t₁))) ∧ MeasureTheory.MemLp Dtu 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo t₀ t₁))) ∧ ∀ t ∈ Set.Icc t₀ t₁,
(∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, ∑ j : Fin 3, Du (x, t) i j ^ 2) + ∫ (τ : ℝ) in t₀..t, ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, (∑ j : Fin 3, D2u (x, τ) i j j) ^ 2 ≤ (∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, ∑ j : Fin 3, Du (x, t₀) i j ^ 2) * Real.exp
(C * ∫ (τ : ℝ) in t₀..t, (MeasureTheory.eLpNorm
(fun (x : CKN.Foundation.Parabolic.Vec3) =>
CKN.Foundation.Parabolic.vec3EuclideanNorm (u (x, τ)))
(ENNReal.ofReal s) MeasureTheory.volume).toReal ^ (2 * s / (s - 3)))
The H¹ estimate for a strong solution with finite Serrin norm of order
s > 3 (lem:lps-H1-estimate), with a constant depending only on s.
theorem
ESS.lps_h1_estimate_endpoint :
∃ (C : ℝ),
0 ≤ C ∧ ∀ {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 → ℝ},
IsLpsStrongSolution t₀ t₁ u Du p →
∫⁻ (t : ℝ) in Set.Ioo t₀ t₁, essSup
(fun (x : CKN.Foundation.Parabolic.Vec3) =>
ENNReal.ofReal (CKN.Foundation.Parabolic.vec3EuclideanNorm (u (x, t))))
MeasureTheory.volume ^ 2 < ⊤ →
∃ (D2u : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3) (Dtu :
CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3),
CKN.HasSpaceTimeWeakDerivs Set.univ (Set.Ioo t₀ t₁) u Du D2u Dtu ∧ MeasureTheory.MemLp D2u 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo t₀ t₁))) ∧ MeasureTheory.MemLp Dtu 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo t₀ t₁))) ∧ ∀ t ∈ Set.Icc t₀ t₁,
(∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, ∑ j : Fin 3, Du (x, t) i j ^ 2) + ∫ (τ : ℝ) in t₀..t, ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, (∑ j : Fin 3, D2u (x, τ) i j j) ^ 2 ≤ (∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, ∑ j : Fin 3, Du (x, t₀) i j ^ 2) * Real.exp
(C * ∫ (τ : ℝ) in t₀..t, (MeasureTheory.eLpNorm
(fun (x : CKN.Foundation.Parabolic.Vec3) =>
CKN.Foundation.Parabolic.vec3EuclideanNorm (u (x, τ)))
⊤ MeasureTheory.volume).toReal ^ 2)
The endpoint H¹ estimate for a strong solution with finite L²_t L∞_x
norm (lem:lps-H1-estimate, case s = ∞), with absolute constant.