Energy Integrable

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

theorem CIV.ofReal_spatialGradientSq_le_nine (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3) (z : CKN.Foundation.Parabolic.ParabolicPoint) : ENNReal.ofReal (CKN.spatialGradientSq u Du z) ≤ 9 * ‖Du z‖ₑ ^ 2

The squared spatial-gradient density is dominated by nine times the square of the gradient's enorm, the entrywise sup norm of the 3 × 3 gradient tensor.

theorem CIV.lintegral_pressure_lt_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 → ℝ) (h : GlobalEnergyClass u Du p) : ∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in unitCylinder, ENNReal.ofReal |p z| ^ (3 / 2) < ⊤

The pressure integrand of Theorem A is finite over Q, directly from the L^{3/2} membership conjunct of the energy class.

theorem CIV.lintegral_force_lt_top (f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hf : ForceC2Bounded f) (q : ℝ) (hq : 0 ≤ q) : ∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in unitCylinder, ENNReal.ofReal (CKN.Foundation.Parabolic.vec3EuclideanNorm (f z)) ^ q < ⊤

The force integrand of Theorem A is finite over Q: ForceC2Bounded gives a pointwise bound on Q, which integrates over the finite-measure cylinder.

theorem CIV.lintegral_cube_lt_top (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 → ℝ) (f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hsol : CKN.IsSuitableWeakSolution (CKN.Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0) q u Du p f) (h : GlobalEnergyClass u Du p) : ∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in unitCylinder, ‖u z‖ₑ ^ 3 < ⊤

The velocity integrand of Theorem A is finite over Q.

theorem CIV.tendsto_lintegral_top_slab (F : CKN.Foundation.Parabolic.ParabolicPoint → ENNReal) (hF : ∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in unitCylinder, F z < ⊤) : Filter.Tendsto (fun (δ : ℝ) => ∫⁻ (z : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball 0 1 ×ˢ Set.Ioo (-δ) 0, F z) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

The integral of a fixed finite-total-mass nonnegative function over the shrinking backward time slabs B(0,1) × (-δ, 0) tends to 0 as δ ↓ 0.