Blowup Ten Thirds Source

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

theorem ESS.blowupRescale_component_tenThirds_uniform_top (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 → ℝ) (x₀ : CKN.Foundation.Parabolic.Vec3) (t₀ r : ℝ) (hr : 0 < r) (R a : ℝ) (hR : 0 < R) (hsol : CKN.IsSuitableWeakSolutionIntegrable (CKN.euclideanBall 0 (R + 1)) (Set.Ioo (a - 2) 0) 3 (parabolicRescaleVelocity x₀ t₀ r u) (parabolicRescaleGradient x₀ t₀ r Du) (parabolicRescalePressure x₀ t₀ r p) 0) (hdom : CKN.Foundation.Parabolic.vec3Ball 0 R ×ˢ Set.Ioo a 0 ⊆ blowupDomain x₀ t₀ r) (htime : Set.Ioo a 0 ⊆ CKN.rescaledTime r t₀ (Set.Ioo (-1) 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) (Cg : ℝ) (hgradInt : MeasureTheory.IntegrableOn (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.spatialGradientSq (parabolicRescaleVelocity x₀ t₀ r u) (parabolicRescaleGradient x₀ t₀ r Du) z) (CKN.Foundation.Parabolic.vec3Ball 0 R ×ˢ Set.Ioo a 0) MeasureTheory.volume) (hgradBound : ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.Foundation.Parabolic.vec3Ball 0 R ×ˢ Set.Ioo a 0, CKN.spatialGradientSq (parabolicRescaleVelocity x₀ t₀ r u) (parabolicRescaleGradient x₀ t₀ r Du) z ≤ Cg) (i : Fin 3) : blowupTenThirdsBound M Cg R a < ⊤ ∧ MeasureTheory.MemLp (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => parabolicRescaleVelocity x₀ t₀ r 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 u z i) (ENNReal.ofReal (10 / 3)) (MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.vec3Ball 0 R ×ˢ Set.Ioo a 0)) ^ (10 / 3) ≤ blowupTenThirdsBound M Cg R a

The finite-past interpolation estimate holds on the entire open terminal-time cylinder for one suitable rescaling.