CZP1 Unconditional Assembly #
Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.
Unconditional Calderón--Zygmund input assemblies #
The endpoint singular-integral estimate is a fixed-time statement. This file performs the solution-level assembly for the singly centred pressure field consumed by the theta-decay cylinder bridge.
theorem
CKN.pressureP1_thetaDecay_hCZ_of_sws
(C_CZ : ℝ)
(hC_CZ : 0 ≤ C_CZ)
(hoperator : Foundation.Euclidean.czP1OperatorConstant ≤ C_CZ)
{Ω : 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)
(hresidual :
∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (z.2 - ρ ^ 2) z.2), ∃ (C : ℝ),
0 ≤ C ∧ (∀ (R : ℝ),
0 < R →
MeasureTheory.MemLp
(fun (x : Foundation.Parabolic.Vec3) =>
pressureP1 (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 f s x - pressureSecondExtensionOperator Foundation.Euclidean.rieszSecondL2Input
Foundation.Euclidean.rieszSecondL2_weak_type
(fun (i j : Fin 3) (x : Foundation.Parabolic.Vec3) =>
mollifiedBallCutoff z.1 hρ x * pressureUTensor u
(fun (t : ℝ) (j : Fin 3) =>
⨍ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball z.1 ρ, u (y, t) j)
(x, s) i j)
x)
(ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall 0 R))) ∧ ∀ (R : ℝ),
0 < R →
MeasureTheory.lpNorm
(fun (x : Foundation.Parabolic.Vec3) =>
pressureP1 (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 f s x - pressureSecondExtensionOperator Foundation.Euclidean.rieszSecondL2Input
Foundation.Euclidean.rieszSecondL2_weak_type
(fun (i j : Fin 3) (x : Foundation.Parabolic.Vec3) =>
mollifiedBallCutoff z.1 hρ x * pressureUTensor u
(fun (t : ℝ) (j : Fin 3) =>
⨍ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball z.1 ρ, u (y, t) j)
(x, s) i j)
x)
(ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall 0 R)) ≤ C * (1 + R))
:
∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (z.2 - ρ ^ 2) z.2), MeasureTheory.MemLp
(fun (x : Foundation.Parabolic.Vec3) =>
pressureP1 (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 f s x)
(ENNReal.ofReal (3 / 2)) MeasureTheory.volume ∧ MeasureTheory.lpNorm
(fun (x : Foundation.Parabolic.Vec3) =>
pressureP1 (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 f s x)
(ENNReal.ofReal (3 / 2)) MeasureTheory.volume ≤ 9 * C_CZ * (∫ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball z.1 ρ, utensorNorm u z.1 ρ s y ^ (3 / 2)) ^ (2 / 3)