Uniform Crude Bounds

Supporting results for the Constantin–Ignatova–Vicol axisymmetric regularity theorem.

theorem CIV.parabolicCylinder_subset_unitCylinder {x : CKN.Foundation.Parabolic.Vec3} {s r : ℝ} (hs : s < 0) (hlow : -1 < s - r ^ 2) (hball : CKN.Foundation.Parabolic.vec3Ball x r ⊆ CKN.Foundation.Parabolic.vec3Ball 0 1) : CKN.Foundation.Parabolic.parabolicCylinder x s r ⊆ unitCylinder

A cylinder based at an interior point (x, s) with s before the top time slice, whose backward parabolic scale r keeps s - r ^ 2 inside (-1, 0) and whose spatial ball sits inside the unit ball, is itself contained in the unit cylinder.

theorem CIV.alpha_le_of_globalEnergyClass {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 → ℝ} (henergy : GlobalEnergyClass u Du p) {x : CKN.Foundation.Parabolic.Vec3} {s r : ℝ} (hr : 0 < r) (hs : s < 0) (hlow : -1 < s - r ^ 2) (hball : CKN.Foundation.Parabolic.vec3Ball x r ⊆ CKN.Foundation.Parabolic.vec3Ball 0 1) : CKN.alpha u (x, s) r ≤ (r⁻¹ * (3 * essSup (fun (τ : ℝ) => ∫⁻ (y : CKN.Foundation.Parabolic.Vec3) in CKN.Foundation.Parabolic.vec3Ball 0 1, ‖u (y, τ)‖ₑ ^ 2) (MeasureTheory.volume.restrict (Set.Ioo (-1) 0))).toReal) ^ (1 / 2)

The energy scale-quantity α at an off-centre cylinder based at (x, s), s < 0, is bounded by the same quantity computed from the global enorm-based energy essential supremum over the whole unit cylinder, uniformly in s, up to the factor 3 from the equivalence between vec3EuclideanNorm and the entrywise sup-norm enorm on Vec3.

theorem CIV.beta_le_of_globalEnergyClass {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3} {x : CKN.Foundation.Parabolic.Vec3} {s r : ℝ} (hr : 0 < r) (hs : s < 0) (hlow : -1 < s - r ^ 2) (hball : CKN.Foundation.Parabolic.vec3Ball x r ⊆ CKN.Foundation.Parabolic.vec3Ball 0 1) (hfin : ∫⁻ (w : CKN.Foundation.Parabolic.ParabolicPoint) in unitCylinder, ENNReal.ofReal (CKN.spatialGradientSq u Du w) ≠ ⊤) : CKN.beta u Du (x, s) r ≤ (r⁻¹ * (∫⁻ (w : CKN.Foundation.Parabolic.ParabolicPoint) in unitCylinder, ENNReal.ofReal (CKN.spatialGradientSq u Du w)).toReal) ^ (1 / 2)

The gradient scale-quantity β at an off-centre cylinder based at (x, s), s < 0, is bounded by the same quantity computed from the global spatial-gradient integral over the whole unit cylinder, uniformly in s.

theorem CIV.delta_le_of_globalEnergyClass {p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {x : CKN.Foundation.Parabolic.Vec3} {s r : ℝ} (hr : 0 < r) (hs : s < 0) (hlow : -1 < s - r ^ 2) (hball : CKN.Foundation.Parabolic.vec3Ball x r ⊆ CKN.Foundation.Parabolic.vec3Ball 0 1) (hfin : ∫⁻ (w : CKN.Foundation.Parabolic.ParabolicPoint) in unitCylinder, ENNReal.ofReal |p w| ^ (3 / 2) ≠ ⊤) : CKN.delta p (x, s) r ≤ (r ^ (-2) * (∫⁻ (w : CKN.Foundation.Parabolic.ParabolicPoint) in unitCylinder, ENNReal.ofReal |p w| ^ (3 / 2)).toReal) ^ (1 / 3)

The pressure scale-quantity δ at an off-centre cylinder based at (x, s), s < 0, is bounded by the same quantity computed from the global L^{3/2} pressure integral over the whole unit cylinder, uniformly in s.

theorem CIV.lambda_le_of_forceC2Bounded {f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (q : ℝ) (hq : 5 / 2 < q) (hMf : ForceC2Bounded f) : ∃ (Cf : ℝ), 0 ≤ Cf ∧ ∀ (x : CKN.Foundation.Parabolic.Vec3) (s r : ℝ), 0 < r → s < 0 → -1 < s - r ^ 2 → CKN.Foundation.Parabolic.vec3Ball x r ⊆ CKN.Foundation.Parabolic.vec3Ball 0 1 → CKN.lambda q f (x, s) r ≤ Cf * r ^ 3

The force scale-quantity λ at every off-centre cylinder based at (x, s), s < 0, inside the unit ball is bounded by a constant multiple of r ^ 3, with the constant depending only on the ForceC2Bounded data, uniformly in x, s and r.