Weights and integrability for the local energy inequality

For a smooth compactly supported space-time weight ψ, the spatial first and second partial derivatives and the time derivative of ψ are derivatives of ψ on the product space, hence continuous, compactly supported and vanishing off the support of ψ. The force pressure, which lies in L²_t L⁶_x, times such a weight is square integrable on every slab. These are the integrability inputs of eq:reg-local-energy-forced.

theorem CKN.Leray.contDiff_fderiv_apply_prod {ψ : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (v : Foundation.Parabolic.Vec3 × ℝ) : ContDiff ℝ ↑⊤ fun (z : Foundation.Parabolic.Vec3 × ℝ) => (fderiv ℝ ψ z) v

theorem CKN.Leray.spatialPartial_eq_fderiv_prod {ψ : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (i : Fin 3) (z : Foundation.Parabolic.Vec3 × ℝ) : spatialPartial ψ i z = (fderiv ℝ ψ z) (basisVec i, 0)

theorem CKN.Leray.spatialSecondPartial_eq_fderiv_prod {ψ : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (i : Fin 3) (z : Foundation.Parabolic.Vec3 × ℝ) : spatialSecondPartial ψ i i z = (fderiv ℝ (fun (w : Foundation.Parabolic.Vec3 × ℝ) => (fderiv ℝ ψ w) (basisVec i, 0)) z) (basisVec i, 0)

theorem CKN.Leray.spatialLaplacian_slice_eq {ψ : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (z : Foundation.Parabolic.Vec3 × ℝ) : spatialLaplacian (fun (y : Foundation.Parabolic.Vec3) => ψ (y, z.2)) z.1 = ∑ i : Fin 3, (fderiv ℝ (fun (w : Foundation.Parabolic.Vec3 × ℝ) => (fderiv ℝ ψ w) (basisVec i, 0)) z) (basisVec i, 0)

The spatial Laplacian of a time slice of a smooth weight as a derivative on the product space.

theorem CKN.Leray.continuous_fderiv_apply_prod {ψ : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (v : Foundation.Parabolic.Vec3 × ℝ) : Continuous fun (z : Foundation.Parabolic.Vec3 × ℝ) => (fderiv ℝ ψ z) v

theorem CKN.Leray.continuous_laplacian_prod {ψ : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) : Continuous fun (z : Foundation.Parabolic.Vec3 × ℝ) => ∑ i : Fin 3, (fderiv ℝ (fun (w : Foundation.Parabolic.Vec3 × ℝ) => (fderiv ℝ ψ w) (basisVec i, 0)) z) (basisVec i, 0)

theorem CKN.Leray.hasCompactSupport_laplacian_prod {ψ : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hψc : HasCompactSupport ψ) : HasCompactSupport fun (z : Foundation.Parabolic.Vec3 × ℝ) => ∑ i : Fin 3, (fderiv ℝ (fun (w : Foundation.Parabolic.Vec3 × ℝ) => (fderiv ℝ ψ w) (basisVec i, 0)) z) (basisVec i, 0)

theorem CKN.Leray.exists_abs_le_of_compact {g : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hg : Continuous g) (hgc : HasCompactSupport g) : ∃ (M : ℝ), ∀ (z : Foundation.Parabolic.Vec3 × ℝ), |g z| ≤ M

A continuous compactly supported function is bounded.

theorem CKN.Leray.weights_eq_zero_of_notMem_tsupport {ψ : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) {z : Foundation.Parabolic.Vec3 × ℝ} (hz : z ∉ tsupport ψ) : ψ z = 0 ∧ timePartial ψ z = 0 ∧ (∀ (i : Fin 3), spatialPartial ψ i z = 0) ∧ ∀ (i : Fin 3), spatialSecondPartial ψ i i z = 0

Off the support of the weight, its time derivative and its spatial first and second derivatives vanish.

theorem CKN.Leray.integrable_mul_mul_of_bound {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {a b c : α → ℝ} (ha : MeasureTheory.MemLp a 2 μ) (hb : MeasureTheory.MemLp b 2 μ) (hc : MeasureTheory.AEStronglyMeasurable c μ) {M : ℝ} (hM : ∀ᵐ (x : α) ∂μ, |c x| ≤ M) : MeasureTheory.Integrable (fun (x : α) => a x * (b x * c x)) μ

A product of two square-integrable functions and an essentially bounded measurable weight is integrable.

theorem CKN.Leray.memLp_mul_of_memLp_six {p h : Foundation.Parabolic.Vec3 → ℝ} (hp : MeasureTheory.MemLp p (ENNReal.ofReal 6) MeasureTheory.volume) (hh : Continuous h) (hhc : HasCompactSupport h) : MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => p x * h x) 2 MeasureTheory.volume

An L⁶ function times a continuous compactly supported weight is square integrable.

theorem CKN.Leray.stronglyMeasurable_forcePressure {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hf : IsLocallySquareIntegrableForce f) : MeasureTheory.StronglyMeasurable fun (z : Foundation.Parabolic.Vec3 × ℝ) => forcePressure f hf z

theorem CKN.Leray.ae_memLp_forcePressure_six {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) => forcePressure f hf (x, t)) (ENNReal.ofReal 6) MeasureTheory.volume

On almost every time slice the force pressure lies in L⁶.

theorem CKN.Leray.memLp_forcePressure_mul_prod {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hf : IsLocallySquareIntegrableForce f) {T : ℝ} (hT : 0 < T) {h : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hh : Continuous h) (hhc : HasCompactSupport h) : MeasureTheory.MemLp (fun (z : Foundation.Parabolic.Vec3 × ℝ) => forcePressure f hf z * h z) 2 (MeasureTheory.volume.prod (MeasureTheory.volume.restrict (Set.Ioo 0 T)))

The force pressure times a continuous compactly supported space-time weight is square integrable on every slab.