Blowup Ten Thirds Eventually

Space-time integrability of the rescaled velocity at exponent 10/3.

theorem ESS.blowupRescale_eventually_component_tenThirds_of_gradient_bound (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 → ℝ) (hSuitable : CKN.IsSuitableWeakSolution (CKN.Foundation.Parabolic.vec3Ball 0 (3 / 4)) (Set.Ioo (-1) 0) 3 u Du p 0) (hu : MeasureTheory.AEStronglyMeasurable (goodPointDomain.indicator u) MeasureTheory.volume) (M : ENNReal) (hM : M < ⊤) (hsource : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo (-1) 0), MeasureTheory.AEStronglyMeasurable (fun (x : CKN.Foundation.Parabolic.Vec3) => goodPointDomain.indicator u (x, s)) MeasureTheory.volume ∧ MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => CKN.Foundation.Parabolic.vec3EuclideanNorm (goodPointDomain.indicator u (x, s))) 3 MeasureTheory.volume ≤ M) (x₀ : CKN.Foundation.Parabolic.Vec3) (t₀ : ℝ) (r : ℕ → ℝ) (hx₀ : x₀ ∈ closure (CKN.Foundation.Parabolic.vec3Ball 0 (1 / 2))) (ht₀ : t₀ ∈ Set.Icc (-(1 / 4)) 0) (hr : ∀ (k : ℕ), 0 < r k) (hr0 : Filter.Tendsto r Filter.atTop (nhds 0)) (R a : ℝ) (hR : 0 < R) (ha : a < 0) (C : ℝ) (hgrad : ∀ᶠ (k : ℕ) in Filter.atTop, MeasureTheory.IntegrableOn (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.spatialGradientSq (parabolicRescaleVelocity x₀ t₀ (r k) u) (parabolicRescaleGradient x₀ t₀ (r k) Du) z) (CKN.spaceTimeSet (CKN.euclideanBall 0 R) (Set.Ioo a 0)) MeasureTheory.volume ∧ 2 * ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet (CKN.euclideanBall 0 R) (Set.Ioo a 0), CKN.spatialGradientSq (parabolicRescaleVelocity x₀ t₀ (r k) u) (parabolicRescaleGradient x₀ t₀ (r k) Du) z ≤ C) (i : Fin 3) : have B := blowupTenThirdsBound M (C / 2) R a ^ (10 / 3)⁻¹; B < ⊤ ∧ ∀ᶠ (k : ℕ) in Filter.atTop, MeasureTheory.MemLp (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => parabolicRescaleVelocity x₀ t₀ (r k) u z i) (ENNReal.ofReal (10 / 3)) (MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.vec3Ball 0 R ×ˢ Set.Ioo a 0)) ∧ MeasureTheory.eLpNorm (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => parabolicRescaleVelocity x₀ t₀ (r k) u z i) (ENNReal.ofReal (10 / 3)) (MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.vec3Ball 0 R ×ˢ Set.Ioo a 0)) ≤ B

A common Dirichlet bound for suitable rescalings gives a common local L^(10/3) bound for each velocity component up to time zero.

theorem ESS.blowupRescale_eventually_tenThirds_of_gradient_bound (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 → ℝ) (hSuitable : CKN.IsSuitableWeakSolution (CKN.Foundation.Parabolic.vec3Ball 0 (3 / 4)) (Set.Ioo (-1) 0) 3 u Du p 0) (hu : MeasureTheory.AEStronglyMeasurable (goodPointDomain.indicator u) MeasureTheory.volume) (M : ENNReal) (hM : M < ⊤) (hsource : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo (-1) 0), MeasureTheory.AEStronglyMeasurable (fun (x : CKN.Foundation.Parabolic.Vec3) => goodPointDomain.indicator u (x, s)) MeasureTheory.volume ∧ MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => CKN.Foundation.Parabolic.vec3EuclideanNorm (goodPointDomain.indicator u (x, s))) 3 MeasureTheory.volume ≤ M) (x₀ : CKN.Foundation.Parabolic.Vec3) (t₀ : ℝ) (r : ℕ → ℝ) (hx₀ : x₀ ∈ closure (CKN.Foundation.Parabolic.vec3Ball 0 (1 / 2))) (ht₀ : t₀ ∈ Set.Icc (-(1 / 4)) 0) (hr : ∀ (k : ℕ), 0 < r k) (hr0 : Filter.Tendsto r Filter.atTop (nhds 0)) (R a : ℝ) (hR : 0 < R) (ha : a < 0) (C : ℝ) (hgrad : ∀ᶠ (k : ℕ) in Filter.atTop, MeasureTheory.IntegrableOn (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.spatialGradientSq (parabolicRescaleVelocity x₀ t₀ (r k) u) (parabolicRescaleGradient x₀ t₀ (r k) Du) z) (CKN.spaceTimeSet (CKN.euclideanBall 0 R) (Set.Ioo a 0)) MeasureTheory.volume ∧ 2 * ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet (CKN.euclideanBall 0 R) (Set.Ioo a 0), CKN.spatialGradientSq (parabolicRescaleVelocity x₀ t₀ (r k) u) (parabolicRescaleGradient x₀ t₀ (r k) Du) z ≤ C) : ∃ B < ⊤, ∀ᶠ (k : ℕ) in Filter.atTop, MeasureTheory.MemLp (parabolicRescaleVelocity x₀ t₀ (r k) u) (ENNReal.ofReal (10 / 3)) (MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.vec3Ball 0 R ×ˢ Set.Ioo a 0)) ∧ MeasureTheory.eLpNorm (parabolicRescaleVelocity x₀ t₀ (r k) u) (ENNReal.ofReal (10 / 3)) (MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.vec3Ball 0 R ×ˢ Set.Ioo a 0)) ≤ B

The rescaled velocity has a uniform vector L^(10/3) bound on each fixed bounded open past cylinder.