Documentation

LeanPool.EscauriazaSereginSverak.LPS.H1Estimate

Serrin control of the H¹ norm of a strong solution #

The gradient energy of a strong solution with finite mixed Serrin norm obeys the Grönwall bound of lem:lps-H1-estimate, with a constant depending only on the Serrin exponent.

source
theorem ESS.lps_h1_laplacian_energy_integrable {a b : ℝ} {D2u : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3} (hMD2 : MeasureTheory.MemLp D2u 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo a b)))) :
MeasureTheory.Integrable (fun (t : ℝ) => ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, (∑ j : Fin 3, D2u (x, t) i j j) ^ 2) (MeasureTheory.volume.restrict (Set.Ioo a b))

The Laplacian energy of a strong solution is integrable in time.

source
theorem ESS.lps_h1_estimate_finite {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 → ℝ} {D2u : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3} {Dtu : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}, IsLpsStrongSolution t₀ t₁ u Du p → 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₁))) → (∀ (s t : ℝ), s ∈ Set.Icc t₀ t₁ → t ∈ Set.Icc t₀ t₁ → s ≤ t → ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, ∑ j : Fin 3, Du (x, t) i j ^ 2 = (∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, ∑ j : Fin 3, Du (x, s) i j ^ 2) - 2 * ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo s t), ∑ i : Fin 3, Dtu z i * ∑ j : Fin 3, D2u z i j j) → ∫⁻ (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) < ⊤ → ∀ 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)))

Serrin control of the H¹ norm in the finite branch (lem:lps-H1-estimate): for a strong solution on [t₀, t₁] with finite mixed Serrin integral, the gradient energy plus the integrated Laplacian energy is bounded by the initial gradient energy times exp (C ∫ ‖u‖ₛ^ℓ), ℓ = 2s/(s-3), with C depending only on s. The chain-rule identity of the strong class enters as an explicit hypothesis.

source
theorem ESS.lps_h1_estimate_infinite :
∃ (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 → ℝ} {D2u : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3} {Dtu : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}, IsLpsStrongSolution t₀ t₁ u Du p → 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₁))) → (∀ (s t : ℝ), s ∈ Set.Icc t₀ t₁ → t ∈ Set.Icc t₀ t₁ → s ≤ t → ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, ∑ j : Fin 3, Du (x, t) i j ^ 2 = (∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, ∑ j : Fin 3, Du (x, s) i j ^ 2) - 2 * ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo s t), ∑ i : Fin 3, Dtu z i * ∑ j : Fin 3, D2u z i j j) → ∫⁻ (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 < ⊤ → ∀ 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)

Serrin control of the H¹ norm in the endpoint branch s = ∞ (lem:lps-H1-estimate): the gradient energy plus the integrated Laplacian energy is bounded by the initial gradient energy times exp (C ∫ ‖u‖∞²) with an absolute constant C.