Almost every time slice of the forced regularized solution #
On almost every time of a bounded interval the gradient slices of the forced
regularized solution are square integrable, the force slices are square
integrable and agree with the modification, and the force pressure is locally
integrable with its weak gradient. These are the slice hypotheses of the
momentum identity eq:reg-momentum-forced.
theorem
CKN.Leray.ae_memLp_slice_of_memLp_prod
{F : Foundation.Parabolic.Vec3 × ℝ → ℝ}
(hF : MeasureTheory.StronglyMeasurable F)
{T : ℝ}
(h2 : MeasureTheory.MemLp F 2 (MeasureTheory.volume.prod (MeasureTheory.volume.restrict (Set.Ioo 0 T))))
:
∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 T), MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => F (x, t)) 2 MeasureTheory.volume
Square integrability on a product with a time measure gives square integrable time slices almost everywhere.
theorem
CKN.Leray.ae_memLp_vector_slice_of_memLp_prod
{F : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3}
(hF : MeasureTheory.StronglyMeasurable F)
{T : ℝ}
(h2 : MeasureTheory.MemLp F 2 (MeasureTheory.volume.prod (MeasureTheory.volume.restrict (Set.Ioo 0 T))))
:
∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 T), MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => F (x, t)) 2 MeasureTheory.volume
theorem
CKN.Leray.ae_forcedRegGrad_slice
(ρ : RegMollifierProfile)
(ε : ℝ)
(hε : 0 < ε)
{a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3}
(ha : IsInJ a)
{f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
(hf : IsLocallySquareIntegrableForce f)
{T : ℝ}
(hT : 0 ≤ T)
:
∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 T), ∀ (i j : Fin 3),
MeasureTheory.MemLp
(fun (x : Foundation.Parabolic.Vec3) => forcedMollifiedGrad (forcedRegRep ρ ε hε ha hf) (x, t) i j) 2
MeasureTheory.volume
theorem
CKN.Leray.ae_forcedForceMod_slice
{f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
(hf : IsLocallySquareIntegrableForce f)
{T : ℝ}
(hT : 0 < T)
:
∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 T), MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => forcedForceMod f hf (x, t)) 2 MeasureTheory.volume ∧ (fun (x : Foundation.Parabolic.Vec3) => forcedForceMod f hf (x, t)) =ᵐ[MeasureTheory.volume]
fun (x : Foundation.Parabolic.Vec3) => f (x, t)
theorem
CKN.Leray.ae_forcePressure_slice
{f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
(hf : IsLocallySquareIntegrableForce f)
{T : ℝ}
(hT : 0 < T)
:
∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 T), MeasureTheory.LocallyIntegrable (fun (x : Foundation.Parabolic.Vec3) => forcePressure f hf (x, t))
MeasureTheory.volume ∧ ∃ (hft : MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => f (x, t)) 2 MeasureTheory.volume),
HasWeakGradientOn Set.univ (fun (x : Vec 3) => forcePressure f hf (x, t))
(forcePressureGradientFunction (fun (y : Foundation.Parabolic.Vec3) => f (y, t)) hft)