Strip bounds and slab integrability of the regularized velocity

On every strip ℝ³ × [δ,T] the pointwise velocity of thm:regularised and its first and second spatial partial derivatives are bounded, and on every slab ℝ³ × (δ,T) they are square integrable (R2).

noncomputable def CKN.Leray.regR12CoordBound : ℝ

A common bound for the coordinate functionals.

Equations

• CKN.Leray.regR12CoordBound = ∑ i : Fin 3, ‖CKN.Leray.regR12CoordCLM i‖

theorem CKN.Leray.regR12CoordCLM_norm_le (i : Fin 3) : ‖regR12CoordCLM i‖ ≤ regR12CoordBound

theorem CKN.Leray.regR12CoordBound_nonneg : 0 ≤ regR12CoordBound

noncomputable def CKN.Leray.regR12VelocityBound (T : ℝ) (v : C(↑(RegularizedMildTimeInterval T), BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexVec3 (↑(2 * 2)) 2)) : ℝ

The common strip bound of the velocity and its spatial derivatives.

Equations

• CKN.Leray.regR12VelocityBound T v = CKN.Leray.regR12CoordBound * ((2 * Real.pi) ^ 2 + 2 * Real.pi + 1) * (MeasureTheory.eLpNorm CKN.Leray.regR12Kernel 2 MeasureTheory.volume).toReal * ‖v‖

theorem CKN.Leray.regR12VelocityBound_nonneg (T : ℝ) (v : C(↑(RegularizedMildTimeInterval T), BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexVec3 (↑(2 * 2)) 2)) : 0 ≤ regR12VelocityBound T v

theorem CKN.Leray.regR12_model_abs_le (T : ℝ) (hT : 0 ≤ T) (v : C(↑(RegularizedMildTimeInterval T), BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexVec3 (↑(2 * 2)) 2)) (i : Fin 3) (M : Foundation.Parabolic.L2Vec3 → ℂ) (hM : MeasureTheory.AEStronglyMeasurable M MeasureTheory.volume) (C : ℝ) (hC : 0 ≤ C) (hCle : C ≤ (2 * Real.pi) ^ 2 + 2 * Real.pi + 1) (hMC : ∀ (ξ : Foundation.Parabolic.L2Vec3), ‖M ξ‖ ≤ C * (1 + ‖ξ‖ ^ 2)) (z : Foundation.Parabolic.ParabolicPoint) : |regR12SpaceTimeField (regR12CoordCLM i) M (regR12LiftFreq T hT v) z| ≤ regR12VelocityBound T v

A space-time field of the lift with multiplier constant at most (2π)² + 2π + 1 is bounded by the common strip bound.

theorem CKN.Leray.regR12_mult_const_le_one : 1 ≤ (2 * Real.pi) ^ 2 + 2 * Real.pi + 1

theorem CKN.Leray.regR12_mult_const_le_first : 2 * Real.pi ≤ (2 * Real.pi) ^ 2 + 2 * Real.pi + 1

theorem CKN.Leray.regR12_mult_const_le_second : (2 * Real.pi) ^ 2 ≤ (2 * Real.pi) ^ 2 + 2 * Real.pi + 1

theorem CKN.Leray.regR12Velocity_strip_bounds (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (ha : IsInJ a) (hPath : ∀ (T : ℝ), 0 ≤ T → ∃ (v : C(↑(RegularizedMildTimeInterval T), BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexVec3 (↑(2 * 2)) 2)), ∀ (t : ↑(RegularizedMildTimeInterval T)), (regularisedBesselSobolevToL2CLM (↑(2 * 2)) regR12_besselOrder_nonneg) (v t) = complexifyVectorL2 (regR12Curve ρ ε hε a ha ↑t)) (δ T : ℝ) (hδ : 0 < δ) (hδT : δ < T) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ z ∈ spaceTimeSet Set.univ (Set.Icc δ T), Foundation.Parabolic.vec3EuclideanNorm (regR12Velocity ρ ε hε a ha z) ≤ C ∧ (∀ (i j : Fin 3), |spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => regR12Velocity ρ ε hε a ha y i) j z| ≤ C) ∧ ∀ (i j k : Fin 3), |spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => spatialPartial (fun (x : Foundation.Parabolic.ParabolicPoint) => regR12Velocity ρ ε hε a ha x i) j y) k z| ≤ C

Strip bounds for the velocity and its first and second spatial partial derivatives.

theorem CKN.Leray.regR12Velocity_slab_memLp (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (ha : IsInJ a) (hPath : ∀ (T : ℝ), 0 ≤ T → ∃ (v : C(↑(RegularizedMildTimeInterval T), BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexVec3 (↑(2 * 2)) 2)), ∀ (t : ↑(RegularizedMildTimeInterval T)), (regularisedBesselSobolevToL2CLM (↑(2 * 2)) regR12_besselOrder_nonneg) (v t) = complexifyVectorL2 (regR12Curve ρ ε hε a ha ↑t)) (δ T : ℝ) (hδ : 0 < δ) (hδT : δ < T) : (∀ (i : Fin 3), MeasureTheory.MemLp (fun (z : Foundation.Parabolic.ParabolicPoint) => regR12Velocity ρ ε hε a ha z i) 2 (MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo δ T)))) ∧ (∀ (i j : Fin 3), MeasureTheory.MemLp (fun (z : Foundation.Parabolic.ParabolicPoint) => spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => regR12Velocity ρ ε hε a ha y i) j z) 2 (MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo δ T)))) ∧ ∀ (i j k : Fin 3), MeasureTheory.MemLp (fun (z : Foundation.Parabolic.ParabolicPoint) => spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => spatialPartial (fun (x : Foundation.Parabolic.ParabolicPoint) => regR12Velocity ρ ε hε a ha x i) j y) k z) 2 (MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo δ T)))

Square integrability of the velocity and its first and second spatial partial derivatives on slabs.