Blowup Energy Weighted

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

theorem ESS.blowupEnergyCutoff_weighted_gradient_bound (R : ℝ) (hR : 0 < R) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (a b : ℝ), b < 0 → ∀ {q : ℝ} {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 → ℝ}, CKN.IsSuitableWeakSolutionIntegrable (CKN.euclideanBall 0 (R + 1)) (Set.Ioo (a - 2) 0) q u Du p 0 → MeasureTheory.IntegrableOn (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => (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)) (CKN.spaceTimeSet (CKN.euclideanBall 0 (R + 1)) (Set.Ioo (a - 2) 0)) MeasureTheory.volume → 2 * ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet (CKN.euclideanBall 0 (R + 1)) (Set.Ioo (a - 2) 0), CKN.spatialGradientSq u Du z * blowupEnergyCutoff R a b z ≤ ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet (CKN.euclideanBall 0 (R + 1)) (Set.Ioo (a - 2) 0), (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 local energy inequality bounds the cutoff-weighted gradient by the three standard velocity-pressure terms, uniformly in the upper time cutoff.

theorem ESS.blowupEnergyCutoff_inner_gradient_le (R a b : ℝ) (hR : 0 < R) (hb : b < 0) {q : ℝ} {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 → ℝ} (hsol : CKN.IsSuitableWeakSolutionIntegrable (CKN.euclideanBall 0 (R + 1)) (Set.Ioo (a - 2) 0) q u Du p 0) : ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet (CKN.euclideanBall 0 R) (Set.Ioo a b), CKN.spatialGradientSq u Du z ≤ ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet (CKN.euclideanBall 0 (R + 1)) (Set.Ioo (a - 2) 0), CKN.spatialGradientSq u Du z * blowupEnergyCutoff R a b z

The gradient energy on the inner past cylinder is dominated by the cutoff-weighted energy on the larger cylinder.

theorem ESS.blowupEnergyCutoff_gradient_bound_of_majorant (R : ℝ) (hR : 0 < R) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (a b : ℝ), b < 0 → ∀ {q : ℝ} {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 → ℝ} (M : ℝ), CKN.IsSuitableWeakSolutionIntegrable (CKN.euclideanBall 0 (R + 1)) (Set.Ioo (a - 2) 0) q u Du p 0 → MeasureTheory.IntegrableOn (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => (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)) (CKN.spaceTimeSet (CKN.euclideanBall 0 (R + 1)) (Set.Ioo (a - 2) 0)) MeasureTheory.volume → ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet (CKN.euclideanBall 0 (R + 1)) (Set.Ioo (a - 2) 0), (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) ≤ M → 2 * ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet (CKN.euclideanBall 0 R) (Set.Ioo a b), CKN.spatialGradientSq u Du z ≤ M

A bound for the three velocity-pressure terms gives the same bound, up to the energy factor two, for the gradient on the inner cylinder.