Documentation

LeanPool.EscauriazaSereginSverak.Endpoint.BlowupEnergyDensity

Blowup Energy Density #

Local energy bounds for the rescaled sequence in the endpoint regularity argument.

source
theorem ESS.blowupEnergyCutoff_localEnergyRhs_le (R : ℝ) (hR : 0 < R) :
∃ (C : ℝ), 0 ≤ C ∧ ∀ (a b : ℝ), b < 0 → ∀ (u : CKN.Foundation.Parabolic.Vec3 × ℝ → CKN.Foundation.Parabolic.Vec3) (p : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) (z : CKN.Foundation.Parabolic.Vec3 × ℝ), CKN.localEnergyRhs u p 0 (blowupEnergyCutoff R a b) z ≤ CKN.Foundation.Parabolic.vec3EuclideanNorm (u z) ^ 2 * (8 + 3 * C) + |CKN.Foundation.Parabolic.vec3EuclideanNorm (u z) ^ 2 + 2 * p z| * (3 * C * CKN.Foundation.Parabolic.vec3EuclideanNorm (u z))

The local-energy right-hand density for the fixed spatial cutoff is bounded by the velocity and pressure densities with one coefficient that does not depend on the upper time cutoff.

source
theorem ESS.blowupEnergyCutoff_localEnergyRhs_power_le (R : ℝ) (hR : 0 < R) :
∃ (C : ℝ), 0 ≤ C ∧ ∀ (a b : ℝ), b < 0 → ∀ (u : CKN.Foundation.Parabolic.Vec3 × ℝ → CKN.Foundation.Parabolic.Vec3) (p : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) (z : CKN.Foundation.Parabolic.Vec3 × ℝ), CKN.localEnergyRhs u p 0 (blowupEnergyCutoff R a b) z ≤ (8 + 3 * C) * CKN.Foundation.Parabolic.vec3EuclideanNorm (u z) ^ 2 + 3 * C * CKN.Foundation.Parabolic.vec3EuclideanNorm (u z) ^ 3 + 6 * C * |p z| * CKN.Foundation.Parabolic.vec3EuclideanNorm (u z)

The same density bound in the power form used with slice L³ and pressure L^(3/2) estimates.