Quantitative time bounds for the fixed pressure remainder

The harmonic bound retains the kinetic energy of each time slice rather than replacing it by its essential supremum in time. The calculus and integral estimates are adapted from CKN.Pressure.HarmonicPartBoundsAE.

theorem CKN.Core.Step4.exists_harmonicPressurePart_Ck_slice_energy_of_sws (k : ℕ) : ∃ (C₁₆ : ℝ), 0 ≤ C₁₆ ∧ ∀ {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {q : ℝ} {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3} {p : Foundation.Parabolic.ParabolicPoint → ℝ} {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}, IsSuitableWeakSolutionIntegrable Ω I q u Du p f → ∀ {z : Foundation.Parabolic.ParabolicPoint} {ρ : ℝ} (hρ : 0 < ρ), closure (Foundation.Parabolic.parabolicCylinder z.1 z.2 ρ) ⊆ spaceTimeSet Ω I → ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (z.2 - ρ ^ 2) z.2), ∀ x ∈ Foundation.Parabolic.vec3Ball z.1 (ρ / 2), ‖iteratedFDeriv ℝ k (harmonicPressurePart (mollifiedBallCutoff z.1 hρ) u (fun (t : ℝ) (j : Fin 3) => ⨍ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball z.1 ρ, u (y, t) j) p s) x‖ ≤ C₁₆ * ρ ^ (-(2 + ↑k)) * ((∫ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball z.1 ρ, Foundation.Parabolic.vec3EuclideanNorm (u (y, s)) ^ 2) / ρ + (∫ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball z.1 ρ, |p (y, s)|) / ((Real.pi * 4 / 3) ^ (1 / 3) * ρ))

The harmonic estimate with the actual slice energy, before taking any time supremum.

theorem CKN.Core.Step4.slice_integral_power_bound {B : Set Foundation.Parabolic.Vec3} {J : Set ℝ} {F : Foundation.Parabolic.Vec3 × ℝ → ENNReal} (hF : AEMeasurable F ((MeasureTheory.volume.restrict B).prod (MeasureTheory.volume.restrict J))) (a : ℝ) : AEMeasurable (fun (s : ℝ) => ∫⁻ (y : Foundation.Parabolic.Vec3) in B, F (y, s) ^ a) (MeasureTheory.volume.restrict J) ∧ ∫⁻ (s : ℝ) in J, (∫⁻ (y : Foundation.Parabolic.Vec3) in B, F (y, s) ^ a) ^ (3 / 2) ≤ MeasureTheory.volume B ^ (1 / 2) * ∫⁻ (w : Foundation.Parabolic.Vec3 × ℝ) in B ×ˢ J, F w ^ (a * (3 / 2))

theorem CKN.Core.Step4.three_terms_power_bound (a b c : ENNReal) : (a + b + c) ^ (3 / 2) ≤ 16 * (a ^ (3 / 2) + b ^ (3 / 2) + c ^ (3 / 2))

noncomputable def CKN.Core.Step4.fixedRemainderCoefficients (C ρ : ℝ) : Fin 3 → ENNReal

The three coefficients of the slice-energy, pressure, and force integrals.

Equations

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

noncomputable def CKN.Core.Step4.fixedRemainderSliceMajorant (C ρ : ℝ) (x : Foundation.Parabolic.Vec3) (u f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (p : Foundation.Parabolic.ParabolicPoint → ℝ) (s : ℝ) : ENNReal

A fixed-collar remainder majorant retaining the actual energy of each slice.

Equations

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

noncomputable def CKN.Core.Step4.fixedRemainderMomentConstant (C ρ : ℝ) (x : Foundation.Parabolic.Vec3) : ENNReal

An explicit coefficient for the 3/2 time moment on a fixed collar.

Equations

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

theorem CKN.Core.Step4.three_slice_mass_bound {B : Set Foundation.Parabolic.Vec3} {J : Set ℝ} {U P F : Foundation.Parabolic.Vec3 × ℝ → ENNReal} (hU : AEMeasurable U ((MeasureTheory.volume.restrict B).prod (MeasureTheory.volume.restrict J))) (hP : AEMeasurable P ((MeasureTheory.volume.restrict B).prod (MeasureTheory.volume.restrict J))) (hF : AEMeasurable F ((MeasureTheory.volume.restrict B).prod (MeasureTheory.volume.restrict J))) (a b c D : ENNReal) (hUD : ∫⁻ (w : Foundation.Parabolic.Vec3 × ℝ) in B ×ˢ J, U w ^ 3 ≤ D) (hPD : ∫⁻ (w : Foundation.Parabolic.Vec3 × ℝ) in B ×ˢ J, P w ^ (3 / 2) ≤ D) (hFD : ∫⁻ (w : Foundation.Parabolic.Vec3 × ℝ) in B ×ˢ J, F w ^ (3 / 2) ≤ D) : have M := fun (s : ℝ) => ((a * ∫⁻ (y : Foundation.Parabolic.Vec3) in B, U (y, s) ^ 2) + b * ∫⁻ (y : Foundation.Parabolic.Vec3) in B, P (y, s)) + c * ∫⁻ (y : Foundation.Parabolic.Vec3) in B, F (y, s); AEMeasurable M (MeasureTheory.volume.restrict J) ∧ ∫⁻ (s : ℝ) in J, M s ^ (3 / 2) ≤ 16 * MeasureTheory.volume B ^ (1 / 2) * (a ^ (3 / 2) + b ^ (3 / 2) + c ^ (3 / 2)) * D

theorem CKN.Core.Step4.fixed_remainder_slice_majorant_moment_of_sws (C ε : ℝ) {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {q : ℝ} {u f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3} {p : Foundation.Parabolic.ParabolicPoint → ℝ} (hsol : IsSuitableWeakSolutionIntegrable Ω I q u Du p f) (hdom : closure (Foundation.Parabolic.parabolicCylinder 0 0 1) ⊆ spaceTimeSet Ω I) (hsmall : ∫⁻ (w : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder 0 0 1, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u w)) ^ 3 + ENNReal.ofReal |p w| ^ (3 / 2) + ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (f w)) ^ q ≤ ENNReal.ofReal ε) {z : Foundation.Parabolic.ParabolicPoint} {ρ : ℝ} (hQ : Foundation.Parabolic.parabolicCylinder z.1 z.2 ρ ⊆ Foundation.Parabolic.parabolicCylinder 0 0 1) : AEMeasurable (fixedRemainderSliceMajorant C ρ z.1 u f p) (MeasureTheory.volume.restrict (Set.Ioc (z.2 - ρ ^ 2) z.2)) ∧ ∫⁻ (s : ℝ) in Set.Ioc (z.2 - ρ ^ 2) z.2, fixedRemainderSliceMajorant C ρ z.1 u f p s ^ (3 / 2) ≤ fixedRemainderMomentConstant C ρ z.1 * (ENNReal.ofReal ε + 1)

The refined remainder majorant has an explicit moment linear in the unit data size.

theorem CKN.Core.Step4.exists_fixed_remainder_quantitative_majorant : ∃ (C : ℝ), 0 ≤ C ∧ ∀ {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {q : ℝ} {u f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3} {p : Foundation.Parabolic.ParabolicPoint → ℝ}, IsSuitableWeakSolutionIntegrable Ω I q u Du p f → ∀ {z : Foundation.Parabolic.ParabolicPoint} {ρ : ℝ} (hρ : 0 < ρ), closure (Foundation.Parabolic.parabolicCylinder z.1 z.2 ρ) ⊆ spaceTimeSet Ω I → ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (z.2 - ρ ^ 2) z.2), ∀ (i : Fin 3), ∀ x ∈ Foundation.Parabolic.vec3Ball z.1 (ρ / 2), ‖classicalGradient (harmonicPressurePart (mollifiedBallCutoff z.1 hρ) u (sourceSliceCentredMean z.1 ρ u) p s + pressureP8 (mollifiedBallCutoff z.1 hρ) f s) x i‖ₑ ≤ fixedRemainderSliceMajorant C ρ z.1 u f p s

A universal harmonic constant gives a quantitative majorant for the actual fixed remainder.

theorem CKN.Core.Step4.fixedRemainderMomentConstant_lt_top (C ρ : ℝ) (x : Foundation.Parabolic.Vec3) : fixedRemainderMomentConstant C ρ x < ⊤

The explicit moment coefficient is finite for every fixed real collar radius.

theorem CKN.Core.Step4.fixed_remainder_clipped_moment_of_sws (C ε : ℝ) {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {q : ℝ} {u f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3} {p : Foundation.Parabolic.ParabolicPoint → ℝ} (hsol : IsSuitableWeakSolutionIntegrable Ω I q u Du p f) (hdom : closure (Foundation.Parabolic.parabolicCylinder 0 0 1) ⊆ spaceTimeSet Ω I) (hsmall : ∫⁻ (w : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder 0 0 1, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u w)) ^ 3 + ENNReal.ofReal |p w| ^ (3 / 2) + ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (f w)) ^ q ≤ ENNReal.ofReal ε) {z : Foundation.Parabolic.ParabolicPoint} {ρ : ℝ} (hQ : Foundation.Parabolic.parabolicCylinder z.1 z.2 ρ ⊆ Foundation.Parabolic.parabolicCylinder 0 0 1) (T : Set ℝ) : ∫⁻ (s : ℝ) in Set.Ioc (z.2 - ρ ^ 2) z.2 ∩ T, fixedRemainderSliceMajorant C ρ z.1 u f p s ^ (6 / 5) ≤ (ENNReal.ofReal (ρ ^ 2) + fixedRemainderMomentConstant C ρ z.1) * (ENNReal.ofReal ε + 1)

Every clipped time window obeys the explicit 6/5 remainder bound.