Blowup Ten Thirds Finite

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

noncomputable def ESS.blowupTenThirdsBound (M : ENNReal) (Cg R a : ℝ) : ENNReal

The ball-time interpolation bound determined by the source slice norm, Dirichlet integral, and cylinder size.

Equations

• One or more equations did not get rendered due to their size.

theorem ESS.blowupTenThirdsBound_lt_top (M : ENNReal) (hM : M < ⊤) (Cg R a : ℝ) : blowupTenThirdsBound M Cg R a < ⊤

The interpolation bound is finite when the source slice bound is finite.

theorem ESS.blowupRescale_component_tenThirds_uniform_finite_past (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)) (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 < ⊤ ∧ ∀ (b : ℝ), a < b → b < 0 → 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 b)) ∧ 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 b)) ^ (10 / 3) ≤ blowupTenThirdsBound M Cg R a

One suitable rescaling has a uniform L^(10/3) bound for each velocity component on all finite past subcylinders with the same lower time.