Pressure Gradient Origin KPHarmonic Moment

Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.

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

The harmonic slice majorant keeps only kinetic energy and pressure mass.

Equations

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

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

The explicit coefficient of the harmonic majorant's time moment.

Equations

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

theorem CKN.Core.Step4.origin_harmonic_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 (originHarmonicSliceMajorant C ρ z.1 u p) (MeasureTheory.volume.restrict (Set.Ioc (z.2 - ρ ^ 2) z.2)) ∧ ∫⁻ (s : ℝ) in Set.Ioc (z.2 - ρ ^ 2) z.2, originHarmonicSliceMajorant C ρ z.1 u p s ^ (3 / 2) ≤ originHarmonicMomentConstant C ρ z.1 * ENNReal.ofReal ε

The harmonic time moment is linear in the unit data size and vanishes with it; no additive constant is needed for the pressure and energy terms.

theorem CKN.Core.Step4.exists_origin_harmonic_gradient_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) x i‖ₑ ≤ originHarmonicSliceMajorant C ρ z.1 u p s

One absolute harmonic coefficient controls every component of the actual harmonic gradient by its slice-energy majorant.

theorem CKN.Core.Step4.origin_harmonic_majorant_clipped_time_of_sws (C ε t r : ℝ) (hr : 0 < r) {Ω : 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) : ∫⁻ (s : ℝ) in Set.Ioc (t - r ^ 2) t ∩ Set.Ioc (z.2 - ρ ^ 2) z.2, originHarmonicSliceMajorant C ρ z.1 u p s ^ (6 / 5) ≤ originHarmonicMomentConstant C ρ z.1 ^ (4 / 5) * ENNReal.ofReal ε ^ (4 / 5) * ENNReal.ofReal r ^ (2 / 5)

Temporal Hölder gives the small-cell power with its vanishing data-size factor retained explicitly. The source collar and the tested cell are separate.

noncomputable def CKN.Core.Step4.originHarmonicAbsoluteMomentConstant (C : ℝ) : ENNReal

A collar-independent moment coefficient for source radii between 1/8 and 1. It is an explicit function of the absolute harmonic coefficient.

Equations

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

theorem CKN.Core.Step4.origin_harmonic_moment_constant_le_absolute (C ρ : ℝ) (x : Foundation.Parabolic.Vec3) (hC : 0 ≤ C) (hρlo : 1 / 8 ≤ ρ) (hρhi : ρ ≤ 1) : originHarmonicMomentConstant C ρ x ≤ originHarmonicAbsoluteMomentConstant C

The harmonic moment coefficient is uniform on the admissible fixed collars.

theorem CKN.Core.Step4.origin_harmonic_clipped_slice_norm_bound (C ε : ℝ) (S : Set Foundation.Parabolic.Vec3) (J : Set ℝ) (t r : ℝ) (hr : 0 < r) {M : ℝ → ENNReal} {F : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hJ : MeasurableSet J) (hm : AEMeasurable M (MeasureTheory.volume.restrict J)) (hMass : ∫⁻ (s : ℝ) in J, M s ^ (3 / 2) ≤ originHarmonicAbsoluteMomentConstant C * ENNReal.ofReal ε) (hf : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict J, MeasureTheory.AEStronglyMeasurable (fun (y : Foundation.Parabolic.Vec3) => F (y, s)) (MeasureTheory.volume.restrict S)) (hb : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict J, ∀ᵐ (y : Foundation.Parabolic.Vec3) ∂MeasureTheory.volume.restrict S, ‖F (y, s)‖ₑ ≤ M s) : ∫⁻ (s : ℝ) in Set.Ioc (t - r ^ 2) t ∩ J, MeasureTheory.eLpNorm (fun (y : Foundation.Parabolic.Vec3) => F (y, s)) (ENNReal.ofReal (6 / 5)) (MeasureTheory.volume.restrict S) ^ (6 / 5) ≤ MeasureTheory.volume S * originHarmonicAbsoluteMomentConstant C ^ (4 / 5) * ENNReal.ofReal ε ^ (4 / 5) * ENNReal.ofReal r ^ (2 / 5)

A spatial majorant with the harmonic time bound controls the literal clipped slice norm; spatial clipping contributes only its volume.