Harmonic pressure estimates on the fixed gap collars

The collar floor is 1/128. The larger absolute moment coefficient is chosen before the numerical data and the suitable solution.

Pressure Gradient Origin Gap Harmonic Moment

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

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

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

theorem CKN.Core.Step4.exists_gap_harmonic_mass_envelope_coefficient : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (q ε κ ρ R₁ t r : ℝ) (x : Foundation.Parabolic.Vec3) (z : Foundation.Parabolic.ParabolicPoint) (S : Set Foundation.Parabolic.Vec3), 0 < κ → κ ≤ 25 / 9 → ∀ (hρlo : 1 / 128 ≤ ρ), ρ ≤ 1 → 0 < r → r ≤ 1 → MeasurableSet S → S ⊆ Foundation.Parabolic.vec3Ball x r → S ⊆ Foundation.Parabolic.vec3Ball z.1 (ρ / 2) → Set.Ioc (t - r ^ 2) t ∩ Set.Ioc (-R₁ ^ 2) 0 ⊆ Set.Ioc (z.2 - ρ ^ 2) z.2 → ∀ {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {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 → closure (Foundation.Parabolic.parabolicCylinder 0 0 1) ⊆ spaceTimeSet Ω I → closure (Foundation.Parabolic.parabolicCylinder z.1 z.2 ρ) ⊆ spaceTimeSet Ω I → Foundation.Parabolic.parabolicCylinder z.1 z.2 ρ ⊆ Foundation.Parabolic.parabolicCylinder 0 0 1 → ∫⁻ (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 ε → ∀ (i : Fin 3), ∃ (M : ℝ → ENNReal), AEMeasurable M (MeasureTheory.volume.restrict (Set.Ioc (t - r ^ 2) t ∩ Set.Ioc (-R₁ ^ 2) 0)) ∧ (∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (t - r ^ 2) t ∩ Set.Ioc (-R₁ ^ 2) 0), MeasureTheory.eLpNorm (fun (y : Vec 3) => classicalGradient (harmonicPressurePart (mollifiedBallCutoff z.1 ⋯) u (sourceSliceCentredMean z.1 ρ u) p s) y i) (ENNReal.ofReal (6 / 5)) (MeasureTheory.volume.restrict S) ^ (6 / 5) ≤ M s) ∧ ∫⁻ (s : ℝ) in Set.Ioc (t - r ^ 2) t ∩ Set.Ioc (-R₁ ^ 2) 0, M s ≤ ENNReal.ofReal (Real.pi * 4 / 3) * originHarmonicAbsoluteMomentConstant C ^ (4 / 5) * ENNReal.ofReal ε ^ (4 / 5) * ENNReal.ofReal (r ^ (5 * (1 - 6 / 5 / κ)))

The actual harmonic gradient satisfies the affine A-slot estimate on any clipped cell contained in a fixed source collar. All numerical parameters and the absolute harmonic coefficient precede the suitable solution.

noncomputable def CKN.Core.Step4.gapHarmonicEnvelopeCoefficient : ℝ

A fixed absolute coefficient for measurable harmonic mass envelopes.

Equations

• CKN.Core.Step4.gapHarmonicEnvelopeCoefficient = Classical.choose CKN.Core.Step4.exists_gap_harmonic_mass_envelope_coefficient

noncomputable def CKN.Core.Step4.gapHarmonicEnvelopeThreshold : ℝ

The affine threshold of the fixed harmonic mass envelope.

Equations

• CKN.Core.Step4.gapHarmonicEnvelopeThreshold = CKN.Core.Step4.originHarmonicThresholdA CKN.Core.Step4.gapHarmonicEnvelopeCoefficient

theorem CKN.Core.Step4.exists_gap_harmonic_affine_envelope_of_sws (q ε C_CZ κ ρ R₁ t r : ℝ) (x : Foundation.Parabolic.Vec3) (z : Foundation.Parabolic.ParabolicPoint) (KU KD : ENNReal) (S : Set Foundation.Parabolic.Vec3) : gapHarmonicEnvelopeThreshold ≤ C_CZ → 0 < κ → κ ≤ 25 / 9 → ∀ (hρlo : 1 / 128 ≤ ρ), ρ ≤ 1 → 0 < r → r ≤ 1 → MeasurableSet S → S ⊆ Foundation.Parabolic.vec3Ball x r → S ⊆ Foundation.Parabolic.vec3Ball z.1 (ρ / 2) → Set.Ioc (t - r ^ 2) t ∩ Set.Ioc (-R₁ ^ 2) 0 ⊆ Set.Ioc (z.2 - ρ ^ 2) z.2 → ∀ {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {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 → closure (Foundation.Parabolic.parabolicCylinder 0 0 1) ⊆ spaceTimeSet Ω I → closure (Foundation.Parabolic.parabolicCylinder z.1 z.2 ρ) ⊆ spaceTimeSet Ω I → Foundation.Parabolic.parabolicCylinder z.1 z.2 ρ ⊆ Foundation.Parabolic.parabolicCylinder 0 0 1 → ∫⁻ (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 ε → ∀ (i : Fin 3), ∃ (M : ℝ → ENNReal), AEMeasurable M (MeasureTheory.volume.restrict (Set.Ioc (t - r ^ 2) t ∩ Set.Ioc (-R₁ ^ 2) 0)) ∧ (∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (t - r ^ 2) t ∩ Set.Ioc (-R₁ ^ 2) 0), MeasureTheory.eLpNorm (fun (y : Vec 3) => classicalGradient (harmonicPressurePart (mollifiedBallCutoff z.1 ⋯) u (sourceSliceCentredMean z.1 ρ u) p s) y i) (ENNReal.ofReal (6 / 5)) (MeasureTheory.volume.restrict S) ^ (6 / 5) ≤ M s) ∧ ∫⁻ (s : ℝ) in Set.Ioc (t - r ^ 2) t ∩ Set.Ioc (-R₁ ^ 2) 0, M s ≤ originKPAffineASlot q C_CZ ε KU KD * ENNReal.ofReal (r ^ (5 * (1 - 6 / 5 / κ)))

A measurable envelope for the harmonic slice mass fits the affine slot.