Reg Equicontinuity

Supporting estimates for the Navier–Stokes development.

theorem CKN.Leray.regEqui_pairing_equation_ibp (f : Fin 3 → Foundation.Parabolic.Vec3 → ℝ) (g : Fin 3 → Fin 3 → Foundation.Parabolic.Vec3 → ℝ) (h : Fin 3 → Fin 3 → Fin 3 → Foundation.Parabolic.Vec3 → ℝ) (P : Foundation.Parabolic.Vec3 → ℝ) (q J F w : Fin 3 → Foundation.Parabolic.Vec3 → ℝ) (hf : ∀ (i : Fin 3), Continuous (f i)) (hfdiff : ∀ (i : Fin 3) (x : Foundation.Parabolic.Vec3), DifferentiableAt ℝ (f i) x) (hfd : ∀ (i j : Fin 3) (x : Foundation.Parabolic.Vec3), (fderiv ℝ (f i) x) (basisVec j) = g i j x) (hg : ∀ (i j : Fin 3), Continuous (g i j)) (hgdiff : ∀ (i j : Fin 3) (x : Foundation.Parabolic.Vec3), DifferentiableAt ℝ (g i j) x) (hgd : ∀ (i j k : Fin 3) (x : Foundation.Parabolic.Vec3), (fderiv ℝ (g i j) x) (basisVec k) = h i j k x) (hh : ∀ (i j k : Fin 3), Continuous (h i j k)) (hP : Continuous P) (hPdiff : ∀ (x : Foundation.Parabolic.Vec3), DifferentiableAt ℝ P x) (hPd : ∀ (i : Fin 3) (x : Foundation.Parabolic.Vec3), (fderiv ℝ P x) (basisVec i) = q i x) (hq : ∀ (i : Fin 3), Continuous (q i)) (hJ : ∀ (j : Fin 3), ContDiff ℝ 1 (J j)) (hdivJ : ∀ (x : Foundation.Parabolic.Vec3), ∑ j : Fin 3, (fderiv ℝ (J j) x) (basisVec j) = 0) (hF : ∀ (i : Fin 3) (x : Foundation.Parabolic.Vec3), F i x = ∑ j : Fin 3, h i j j x - ∑ j : Fin 3, J j x * g i j x - q i x) (hw : ∀ (i : Fin 3), ContDiff ℝ (↑⊤) (w i)) (hwc : ∀ (i : Fin 3), HasCompactSupport (w i)) : ∫ (x : Foundation.Parabolic.Vec3), ∑ i : Fin 3, F i x * w i x = (∫ (x : Foundation.Parabolic.Vec3), ∑ i : Fin 3, ∑ j : Fin 3, (f i x * spatialDeriv (spatialDeriv (w i) j) j x + f i x * J j x * spatialDeriv (w i) j x)) + ∫ (x : Foundation.Parabolic.Vec3), P x * ∑ i : Fin 3, spatialDeriv (w i) i x

theorem CKN.Leray.regEquicontinuity_pressure_mul_memLp_one (p g : Foundation.Parabolic.ParabolicPoint → ℝ) (Q : Set Foundation.Parabolic.ParabolicPoint) (hp : MeasureTheory.MemLp p (ENNReal.ofReal (5 / 3)) regUniformPositiveTimeMeasure) (hg : MeasureTheory.MemLp g (ENNReal.ofReal (5 / 2)) (regUniformPositiveTimeMeasure.restrict Q)) : MeasureTheory.MemLp (fun (z : Foundation.Parabolic.ParabolicPoint) => p z * g z) 1 (regUniformPositiveTimeMeasure.restrict Q) ∧ MeasureTheory.eLpNorm (fun (z : Foundation.Parabolic.ParabolicPoint) => p z * g z) 1 (regUniformPositiveTimeMeasure.restrict Q) ≤ MeasureTheory.eLpNorm p (ENNReal.ofReal (5 / 3)) regUniformPositiveTimeMeasure * MeasureTheory.eLpNorm g (ENNReal.ofReal (5 / 2)) (regUniformPositiveTimeMeasure.restrict Q)

The positive-time pressure bound can be localized to a measurable space-time set before it is paired with a test derivative.

theorem CKN.Leray.regEquicontinuity_pressure_memLp_fiveThirds (F : Fin 3 → Fin 3 → Foundation.Parabolic.Vec3 × ℝ → ℝ) (hF : ∀ (i j : Fin 3), MeasureTheory.MemLp (F i j) (ENNReal.ofReal (5 / 3)) MeasureTheory.volume) (M : ℝ) (hM : 0 ≤ M) (hFbound : ∀ (i j : Fin 3), MeasureTheory.eLpNorm (F i j) (ENNReal.ofReal (5 / 3)) MeasureTheory.volume ≤ ENNReal.ofReal M) (p : Foundation.Parabolic.ParabolicPoint → ℝ) (hpMeasurable : Measurable p) (hR4 : ∀ (t : ℝ), 0 < t → ∃ (hFt : ∀ (i j : Fin 3), MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => F i j (x, t)) (ENNReal.ofReal 2) MeasureTheory.volume), (fun (x : Foundation.Parabolic.Vec3) => p (x, t)) =ᵐ[MeasureTheory.volume] rieszPressureSliceRepresentative 2 regEquicontinuity_pressure_memLp_fiveThirds._proof_1 fun (i j : Fin 3) => MeasureTheory.MemLp.toLp (fun (x : Foundation.Parabolic.Vec3) => F i j (x, t)) ⋯) : ∃ (hp : MeasureTheory.MemLp p (ENNReal.ofReal (5 / 3)) regUniformPositiveTimeMeasure), ‖MeasureTheory.MemLp.toLp p hp‖ ≤ 9 * rieszPressureOperatorBound (5 / 3) regEquicontinuity_pressure_memLp_fiveThirds._proof_2 * M

The exponent-two pressure slice formula identifies the pressure with the space-time Riesz representative at exponent five-thirds whenever the regularized tensor has its global five-thirds bound. This is the pressure input to lem:reg-equicontinuity.