Bounds for the source of the mollified velocity

The source of the mollified forced regularized velocity is jointly measurable, and on almost every time slice it is bounded uniformly in space by the L² norms of the transport-minus-viscous tensor, the quadratic pressure and the force, which are integrable in time. These bounds justify the exchanges of integrals in the local energy inequality eq:reg-local-energy-forced.

theorem CKN.Leray.integral_mul_reflect_eq_convolution (g κ : Foundation.Parabolic.Vec3 → ℝ) (x : Foundation.Parabolic.Vec3) : ∫ (y : Foundation.Parabolic.Vec3), g y * κ (x - y) = MeasureTheory.convolution κ g (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume x

The integral of a field against a translated reflected kernel is a convolution.

theorem CKN.Leray.abs_integral_mul_reflect_le {g κ : Foundation.Parabolic.Vec3 → ℝ} (hg : MeasureTheory.MemLp g 2 MeasureTheory.volume) (hκ : MeasureTheory.MemLp κ 2 MeasureTheory.volume) (x : Foundation.Parabolic.Vec3) : |∫ (y : Foundation.Parabolic.Vec3), g y * κ (x - y)| ≤ (MeasureTheory.eLpNorm κ 2 MeasureTheory.volume).toReal * (MeasureTheory.eLpNorm g 2 MeasureTheory.volume).toReal

The L² pairing of a field with a translated reflected kernel.

theorem CKN.Leray.integrableOn_eLpNorm_slice {X : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hX : MeasureTheory.StronglyMeasurable X) {T : ℝ} (h2 : MeasureTheory.MemLp X 2 (MeasureTheory.volume.prod (MeasureTheory.volume.restrict (Set.Ioo 0 T)))) : MeasureTheory.IntegrableOn (fun (t : ℝ) => (MeasureTheory.eLpNorm (fun (x : Foundation.Parabolic.Vec3) => X (x, t)) 2 MeasureTheory.volume).toReal) (Set.Ioo 0 T) MeasureTheory.volume

The time integral of the slice L² norms of a field that is square integrable on a bounded slab.

theorem CKN.Leray.integrableOn_eLpNorm_vector_slice {X : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3} (hX : MeasureTheory.StronglyMeasurable X) {T : ℝ} (h2 : MeasureTheory.MemLp X 2 (MeasureTheory.volume.prod (MeasureTheory.volume.restrict (Set.Ioo 0 T)))) : MeasureTheory.IntegrableOn (fun (t : ℝ) => (MeasureTheory.eLpNorm (fun (x : Foundation.Parabolic.Vec3) => X (x, t)) 2 MeasureTheory.volume).toReal) (Set.Ioo 0 T) MeasureTheory.volume

The vector version of integrableOn_eLpNorm_slice.

theorem CKN.Leray.memLp_reflect {κ : Foundation.Parabolic.Vec3 → ℝ} (hκ : Continuous κ) (hκc : HasCompactSupport κ) (x : Foundation.Parabolic.Vec3) : MeasureTheory.MemLp (fun (y : Foundation.Parabolic.Vec3) => κ (x - y)) 2 MeasureTheory.volume

theorem CKN.Leray.integrable_mul_reflect {g κ : Foundation.Parabolic.Vec3 → ℝ} (hg : MeasureTheory.MemLp g 2 MeasureTheory.volume) (hκ : Continuous κ) (hκc : HasCompactSupport κ) (x : Foundation.Parabolic.Vec3) : MeasureTheory.Integrable (fun (y : Foundation.Parabolic.Vec3) => g y * κ (x - y)) MeasureTheory.volume

noncomputable def CKN.Leray.leSourceBound (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) {a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (ha : IsInJ a) {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hf : IsLocallySquareIntegrableForce f) (η : Foundation.Parabolic.Vec3 → ℝ) (k : Fin 3) (t : ℝ) : ℝ

The uniform bound of the source on one time slice.

Equations

• One or more equations did not get rendered due to their size.

theorem CKN.Leray.integral_forcePressure_mul_reflect {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hf : IsLocallySquareIntegrableForce f) {η : Foundation.Parabolic.Vec3 → ℝ} (hη : ContDiff ℝ (↑⊤) η) (hηc : HasCompactSupport η) {t : ℝ} {hft : MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => f (x, t)) 2 MeasureTheory.volume} (hpf : HasWeakGradientOn Set.univ (fun (x : Vec 3) => forcePressure f hf (x, t)) (forcePressureGradientFunction (fun (x : Foundation.Parabolic.Vec3) => f (x, t)) hft)) (x : Foundation.Parabolic.Vec3) (k : Fin 3) : ∫ (y : Foundation.Parabolic.Vec3), forcePressure f hf (y, t) * spatialDeriv η k (x - y) = ∫ (y : Foundation.Parabolic.Vec3), forcePressureGradientFunction (fun (x : Foundation.Parabolic.Vec3) => f (x, t)) hft y k * η (x - y)

The force-pressure pairing with a reflected kernel is the pairing of its gradient with the undifferentiated kernel.

theorem CKN.Leray.eLpNorm_forcePressureGradient_le {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {t : ℝ} (hft : MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => f (x, t)) 2 MeasureTheory.volume) (k : Fin 3) : (MeasureTheory.eLpNorm (fun (y : Foundation.Parabolic.Vec3) => forcePressureGradientFunction (fun (x : Foundation.Parabolic.Vec3) => f (x, t)) hft y k) 2 MeasureTheory.volume).toReal ≤ 4 * (MeasureTheory.eLpNorm (fun (x : Foundation.Parabolic.Vec3) => f (x, t)) 2 MeasureTheory.volume).toReal

theorem CKN.Leray.abs_leSF_le (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) {a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (ha : IsInJ a) {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hf : IsLocallySquareIntegrableForce f) {η : Foundation.Parabolic.Vec3 → ℝ} (hη : ContDiff ℝ (↑⊤) η) (hηc : HasCompactSupport η) {t : ℝ} (k : Fin 3) (hA : ∀ (j : Fin 3), MeasureTheory.MemLp (fun (y : Foundation.Parabolic.Vec3) => leTensor ρ ε hε ha hf j k (y, t)) 2 MeasureTheory.volume) (hF2 : MeasureTheory.MemLp (fun (y : Foundation.Parabolic.Vec3) => forcedForceMod f hf (y, t)) 2 MeasureTheory.volume) (hFf : (fun (y : Foundation.Parabolic.Vec3) => forcedForceMod f hf (y, t)) =ᵐ[MeasureTheory.volume] fun (y : Foundation.Parabolic.Vec3) => f (y, t)) (hft : MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => f (x, t)) 2 MeasureTheory.volume) (hpf : HasWeakGradientOn Set.univ (fun (x : Vec 3) => forcePressure f hf (x, t)) (forcePressureGradientFunction (fun (x : Foundation.Parabolic.Vec3) => f (x, t)) hft)) (hpfl : MeasureTheory.LocallyIntegrable (fun (x : Foundation.Parabolic.Vec3) => forcePressure f hf (x, t)) MeasureTheory.volume) (x : Foundation.Parabolic.Vec3) : |leSF ρ ε hε ha hf η x t k| ≤ leSourceBound ρ ε hε ha hf η k t

The uniform bound of the source on a good time slice.

theorem CKN.Leray.stronglyMeasurable_leTensor (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) {a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (ha : IsInJ a) {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hf : IsLocallySquareIntegrableForce f) (j k : Fin 3) : MeasureTheory.StronglyMeasurable (leTensor ρ ε hε ha hf j k)

theorem CKN.Leray.memLp_leTensor_prod (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) {a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (ha : IsInJ a) {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hf : IsLocallySquareIntegrableForce f) (j k : Fin 3) {T : ℝ} (hT : 0 ≤ T) : MeasureTheory.MemLp (leTensor ρ ε hε ha hf j k) 2 (MeasureTheory.volume.prod (MeasureTheory.volume.restrict (Set.Ioo 0 T)))

theorem CKN.Leray.integrableOn_leSourceBound (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) {a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (ha : IsInJ a) {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hf : IsLocallySquareIntegrableForce f) {η : Foundation.Parabolic.Vec3 → ℝ} (k : Fin 3) {T : ℝ} (hT : 0 < T) : MeasureTheory.IntegrableOn (leSourceBound ρ ε hε ha hf η k) (Set.Ioo 0 T) MeasureTheory.volume