Local energy data for the viscous shear

The velocity and its gradient are bounded by one on the positive time interval. Compact local boxes therefore have finite energy and slice bounds.

theorem CKN.shearFlow_norm_le_one (x : Foundation.Parabolic.Vec3) (s : ℝ) (hs : 0 ≤ s) : ‖shearFlow (x, s)‖ ≤ 1

Uniform velocity bound in nonnegative time.

theorem CKN.shearFlowGrad_norm_le_one (x : Foundation.Parabolic.Vec3) (s : ℝ) (hs : 0 ≤ s) : ‖shearFlowGrad (x, s)‖ ≤ 1

Uniform explicit-gradient bound in nonnegative time.

theorem CKN.shearFlow_localData (Ω' : Set Foundation.Parabolic.Vec3) (J : Set ℝ) (hbox : localBox Set.univ (Set.Ioo 0 1) Ω' J) : MeasureTheory.AEStronglyMeasurable shearFlow (MeasureTheory.volume.restrict (spaceTimeSet Ω' J)) ∧ MeasureTheory.AEStronglyMeasurable shearFlowGrad (MeasureTheory.volume.restrict (spaceTimeSet Ω' J)) ∧ MeasureTheory.AEStronglyMeasurable (fun (x : Foundation.Parabolic.ParabolicPoint) => 0) (MeasureTheory.volume.restrict (spaceTimeSet Ω' J)) ∧ MeasureTheory.AEStronglyMeasurable (fun (x : Foundation.Parabolic.ParabolicPoint) => 0) (MeasureTheory.volume.restrict (spaceTimeSet Ω' J)) ∧ essSup (fun (s : ℝ) => ∫⁻ (x : Foundation.Parabolic.Vec3) in Ω', ‖shearFlow (x, s)‖ₑ ^ 2) (MeasureTheory.volume.restrict J) < ⊤ ∧ ∫⁻ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Ω' J, ‖shearFlow z‖ₑ ^ 2 + ‖shearFlowGrad z‖ₑ ^ 2 < ⊤ ∧ MeasureTheory.MemLp (fun (x : Foundation.Parabolic.ParabolicPoint) => 0) (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (spaceTimeSet Ω' J)) ∧ MeasureTheory.MemLp (fun (x : Foundation.Parabolic.ParabolicPoint) => 0) (ENNReal.ofReal 3) (MeasureTheory.volume.restrict (spaceTimeSet Ω' J)) ∧ ∀ (i : Fin 3), ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict J, HasWeakGradientOn Ω' (fun (x : Vec 3) => shearFlow (x, s) i) fun (x : Vec 3) => shearFlowGrad (x, s) i

All local measurability, finite-energy, and weak-gradient clauses.