Lin34 Slices #
Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.
Almost-everywhere pressure slice integrability on an admissible cylinder.
theorem
CKN.sws_pressure_memLp_slice_ae
{Ω : 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}
(hsol : IsSuitableWeakSolutionIntegrable Ω I q u Du p f)
{z : Foundation.Parabolic.ParabolicPoint}
{ρ : ℝ}
(hρ : 0 < ρ)
(hsub : closure (Foundation.Parabolic.parabolicCylinder z.1 z.2 ρ) ⊆ spaceTimeSet Ω I)
:
∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (z.2 - ρ ^ 2) z.2), MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => p (x, s)) (ENNReal.ofReal (3 / 2))
(MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball z.1 ρ))
The residual is formed before any Calderón--Zygmund estimate is used.
theorem
CKN.pressure_cutoff_pressure_memLp_slice
{p : Foundation.Parabolic.ParabolicPoint → ℝ}
{η : Foundation.Parabolic.Vec3 → ℝ}
{s : ℝ}
{B : Set Foundation.Parabolic.Vec3}
(hp :
MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => p (x, s)) (ENNReal.ofReal (3 / 2))
(MeasureTheory.volume.restrict B))
(hηmeas : MeasureTheory.AEStronglyMeasurable η (MeasureTheory.volume.restrict B))
(hηbound : ∀ᵐ (x : Foundation.Parabolic.Vec3) ∂MeasureTheory.volume.restrict B, ‖η x‖ ≤ 1)
:
MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => η x * p (x, s)) (ENNReal.ofReal (3 / 2))
(MeasureTheory.volume.restrict B)
theorem
CKN.pressure_remainder_eq_on_inner
{u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
{c : ℝ → Foundation.Parabolic.Vec3}
{p : Foundation.Parabolic.ParabolicPoint → ℝ}
{f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
{x₀ : Foundation.Parabolic.Vec3}
{ρ s : ℝ}
(hρ : 0 < ρ)
:
pressureP2 (mollifiedBallCutoff x₀ hρ) u c s + pressureP3 (mollifiedBallCutoff x₀ hρ) u c s + pressureP4 (mollifiedBallCutoff x₀ hρ) u c s + pressureP5 (mollifiedBallCutoff x₀ hρ) p s + pressureP6 (mollifiedBallCutoff x₀ hρ) p s =ᵐ[MeasureTheory.volume.restrict (euclideanBall x₀ (13 * ρ / 20))]
(fun (x : Foundation.Parabolic.Vec3) => p (x, s)) - pressureP1 (mollifiedBallCutoff x₀ hρ) u c p f s - (pressureP7 (mollifiedBallCutoff x₀ hρ) f s + pressureP8 (mollifiedBallCutoff x₀ hρ) f s)
theorem
CKN.pressure_harmonic_potential_data_ae_of_sws_annulus
{Ω : 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}
(hsol : IsSuitableWeakSolutionIntegrable Ω I q u Du p f)
{z : Foundation.Parabolic.ParabolicPoint}
{ρ : ℝ}
(hρ : 0 < ρ)
(hsub : closure (Foundation.Parabolic.parabolicCylinder z.1 z.2 ρ) ⊆ spaceTimeSet Ω I)
(hzero :
∀ y ∉ euclideanBall z.1 (3 * ρ / 4) \ euclideanClosedBall z.1 (13 * ρ / 20),
(∀ (i : Fin 3), spatialDeriv (mollifiedBallCutoff z.1 hρ) i y = 0) ∧ ∀ (i j : Fin 3), mixedSecond (mollifiedBallCutoff z.1 hρ) i j y = 0)
:
∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (z.2 - ρ ^ 2) z.2), PressureHarmonicPotentialData (euclideanBall z.1 (3 * ρ / 4) \ euclideanClosedBall z.1 (13 * ρ / 20))ᶜ
(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