The time derivative of a strong solution is bounded in `L²` after positive time #

prop:lps-smoothing: the Kiselev–Ladyzhenskaya argument. For h > 0 the energy E_h(t) = ∫ |v_h(x, t)|² dx of the time-difference quotient v_h = (u(·, · + h) - u)/h of a strong solution satisfies E_h' ≤ -∫ |∇v_h|² + κ_h E_h with κ_h(t) = 6K (M(t) + M(t + h)), where M(t) is the squared H² norm of u(·, t) and K the constant of the embedding H² ⊂ L^∞. The mean of E_h over [t₀, t₀ + δ] is controlled by the L² norm of ∂ₜu, so Grönwall's inequality bounds E_h on [t₀ + δ, T - h] uniformly in h; letting h → 0 bounds ∫ |∂ₜu(x, t)|² dx for almost every t ∈ (t₀ + δ, T).

source

theorem ESS.lps_kl_energy_inequality {t₀ T h K : ℝ} {M : ℝ → ℝ} (hh : 0 < h) {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3} (hDu : MeasureTheory.MemLp Du 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo t₀ T)))) (hslice : ∀ t ∈ Set.Icc t₀ T, MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, t)) 2 MeasureTheory.volume) (hK : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo t₀ T), ∀ᵐ (x : CKN.Foundation.Parabolic.Vec3), ∀ (i : Fin 3), u (x, t) i ^ 2 ≤ K * M t) :

∀ᵐ (τ : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo t₀ (T - h)), (-2 * ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, ∑ j : Fin 3, (1 / h * (Du (x, τ + h) i j - Du (x, τ) i j)) ^ 2) + 2 * ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, ∑ j : Fin 3, 1 / h * (u (x, τ + h) i * u (x, τ + h) j - u (x, τ) i * u (x, τ) j) * (1 / h * (Du (x, τ + h) i j - Du (x, τ) i j)) ≤ (-∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, ∑ j : Fin 3, (1 / h * (Du (x, τ + h) i j - Du (x, τ) i j)) ^ 2) + 6 * K * (M τ + M (τ + h)) * ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, (1 / h * (u (x, τ + h) i - u (x, τ) i)) ^ 2

The differential inequality for the energy of the time-difference quotients: at almost every time τ of (t₀, T - h), -2 ∫ |∇v|² + 2 ∫ H : ∇v ≤ -∫ |∇v|² + 6K (M(τ) + M(τ + h)) ∫ |v|², given the pointwise bound uᵢ(x, t)² ≤ K M(t) (prop:lps-smoothing).

source

theorem ESS.lps_kl_dissipation_integrable {t₀ T h : ℝ} (hh : 0 < h) {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3} (hDu : MeasureTheory.MemLp Du 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo t₀ T)))) (hH : ∀ (i j : Fin 3), MeasureTheory.MemLp (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => 1 / h * (u (z.1, z.2 + h) i * u (z.1, z.2 + h) j - u z i * u z j)) 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo t₀ (T - h))))) :

MeasureTheory.Integrable (fun (τ : ℝ) => ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, ∑ j : Fin 3, (1 / h * (Du (x, τ + h) i j - Du (x, τ) i j)) ^ 2) (MeasureTheory.volume.restrict (Set.Ioo t₀ (T - h))) ∧ MeasureTheory.Integrable (fun (τ : ℝ) => ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, ∑ j : Fin 3, 1 / h * (u (x, τ + h) i * u (x, τ + h) j - u (x, τ) i * u (x, τ) j) * (1 / h * (Du (x, τ + h) i j - Du (x, τ) i j))) (MeasureTheory.volume.restrict (Set.Ioo t₀ (T - h)))

The dissipation ∫ |∇v|² and the flux pairing ∫ H : ∇v of the time-difference quotient are integrable in time on (t₀, T - h) (prop:lps-smoothing).

source

t ∈ Set.Icc (t₀ + δ) (T - h) → ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, (1 / h * (u (x, t + h) i - u (x, t) i)) ^ 2 ≤ (∫ (σ : ℝ) in t₀..T, ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, Dtu (x, σ) i ^ 2) / δ * Real.exp (12 * K * ∫ (σ : ℝ) in t₀..T, M σ)

The uniform bound of the energy of the time-difference quotients after the initial layer (prop:lps-smoothing): if 0 < h, t₀ + δ ≤ T - h and uᵢ(x, t)² ≤ K M(t) almost everywhere with M ≥ 0 integrable, then ∫ |v_h(x, t)|² dx ≤ (Θ/δ) e^Λ for every t ∈ [t₀ + δ, T - h], where Θ = ∫ₜ₀ᵀ ∫ |∂ₜu|² and Λ = 12K ∫ₜ₀ᵀ M do not depend on h.

source

∃ (B : ℝ), 0 ≤ B ∧ ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo (t₀ + δ) T), ∀ (i : Fin 3), ∫ (x : CKN.Foundation.Parabolic.Vec3), Dtu (x, t) i ^ 2 ≤ B

The time derivative of a strong solution is bounded in L² at almost every time after t₀ + δ (prop:lps-smoothing): the uniform bound of the time-difference quotients passes to the limit h → 0.

Documentation

LeanPool.EscauriazaSereginSverak.LPS.SmoothingKLBound

The time derivative of a strong solution is bounded in `L²` after positive time #

The time derivative of a strong solution is bounded in L² after positive time #

The time derivative of a strong solution is bounded in `L²` after positive time #