Collar slice masses from the unit data of thm:A

The three slice quantities that control the localized pressure source of eq:pressure-gradient-decomposition on a collar Q(z, ρ) are the cube of the velocity slice norm, the square of the gradient slice norm and the q-th power of the force slice norm. This file identifies each of their time masses with a space-time integral over the collar and bounds it by the unit data of thm:A or by the collar Dirichlet integral.

No estimate here uses velocity or gradient Morrey data.

theorem CKN.Core.Step4.vector_time_slice_norm_power_eq {V : Type u_1} [NormedAddCommGroup V] {P : ℝ} (hP : 0 < P) {G : Foundation.Parabolic.Vec3 × ℝ → V} {E : Set Foundation.Parabolic.Vec3} {J : Set ℝ} (hG : MeasureTheory.AEStronglyMeasurable G (MeasureTheory.volume.restrict (E ×ˢ J))) : ∫⁻ (s : ℝ) in J, MeasureTheory.eLpNorm (fun (y : Foundation.Parabolic.Vec3) => G (y, s)) (ENNReal.ofReal P) (MeasureTheory.volume.restrict E) ^ P = ∫⁻ (w : Foundation.Parabolic.Vec3 × ℝ) in E ×ˢ J, ENNReal.ofReal ‖G w‖ ^ P

The time mass of the powers of a vector slice norm is the space-time power integral of its norm on the product box.

theorem CKN.Core.Step4.vector_time_slice_norm_aemeasurable {V : Type u_1} [NormedAddCommGroup V] {P : ℝ} (hP : 0 < P) {G : Foundation.Parabolic.Vec3 × ℝ → V} {E : Set Foundation.Parabolic.Vec3} {J : Set ℝ} (hG : MeasureTheory.AEStronglyMeasurable G (MeasureTheory.volume.restrict (E ×ˢ J))) : AEMeasurable (fun (s : ℝ) => MeasureTheory.eLpNorm (fun (y : Foundation.Parabolic.Vec3) => G (y, s)) (ENNReal.ofReal P) (MeasureTheory.volume.restrict E)) (MeasureTheory.volume.restrict J)

Vector slice norms are measurable in time on a product box.

theorem CKN.Core.Step4.collar_velocity_slice_cube_mass_le {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {p : Foundation.Parabolic.ParabolicPoint → ℝ} {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {q ε : ℝ} {E : Set Foundation.Parabolic.Vec3} {J : Set ℝ} (hsub : E ×ˢ J ⊆ Foundation.Parabolic.parabolicCylinder 0 0 1) (hu : MeasureTheory.AEStronglyMeasurable u (MeasureTheory.volume.restrict (E ×ˢ J))) (hsize : ∫⁻ (z : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder 0 0 1, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u z)) ^ 3 + ENNReal.ofReal |p z| ^ (3 / 2) + ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (f z)) ^ q ≤ ENNReal.ofReal ε) : ∫⁻ (s : ℝ) in J, MeasureTheory.eLpNorm (fun (y : Foundation.Parabolic.Vec3) => u (y, s)) (ENNReal.ofReal 3) (MeasureTheory.volume.restrict E) ^ 3 ≤ ENNReal.ofReal ε

The cube mass of the velocity slice norms on a collar is at most the unit data of thm:A.

theorem CKN.Core.Step4.collar_gradient_slice_square_mass_le {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3} {E : Set Foundation.Parabolic.Vec3} {J : Set ℝ} (hDu : MeasureTheory.AEStronglyMeasurable Du (MeasureTheory.volume.restrict (E ×ˢ J))) : ∫⁻ (s : ℝ) in J, MeasureTheory.eLpNorm (fun (y : Foundation.Parabolic.Vec3) => Du (y, s)) (ENNReal.ofReal 2) (MeasureTheory.volume.restrict E) ^ 2 ≤ ∫⁻ (w : Foundation.Parabolic.Vec3 × ℝ) in E ×ˢ J, ENNReal.ofReal (spatialGradientSq u Du w)

The square mass of the gradient slice norms on a collar is at most the collar Dirichlet integral.

theorem CKN.Core.Step4.collar_force_slice_power_mass_le {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {p : Foundation.Parabolic.ParabolicPoint → ℝ} {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {q ε : ℝ} (hq : 0 < q) {E : Set Foundation.Parabolic.Vec3} {J : Set ℝ} (hsub : E ×ˢ J ⊆ Foundation.Parabolic.parabolicCylinder 0 0 1) (hf : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.volume.restrict (E ×ˢ J))) (hsize : ∫⁻ (z : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder 0 0 1, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u z)) ^ 3 + ENNReal.ofReal |p z| ^ (3 / 2) + ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (f z)) ^ q ≤ ENNReal.ofReal ε) : ∫⁻ (s : ℝ) in J, MeasureTheory.eLpNorm (fun (y : Foundation.Parabolic.Vec3) => f (y, s)) (ENNReal.ofReal q) (MeasureTheory.volume.restrict E) ^ q ≤ ENNReal.ofReal ε

The q-th power mass of the force slice norms on a collar is at most the unit data of thm:A.