CZCylinder Bridge #
Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.
The product-cylinder part of the solution-level bridge.
theorem
CKN.Foundation.Euclidean.eLpNorm'_cylinder_le_of_ae_slice_bound
{P : Parabolic.Vec3 × ℝ → ℝ}
{B : ℝ → ENNReal}
{x₀ : Parabolic.Vec3}
{t r q : ℝ}
:
0 < r →
∀ (hq : 0 < q)
(hP : MeasureTheory.AEStronglyMeasurable P (MeasureTheory.volume.restrict (Parabolic.parabolicCylinder x₀ t r)))
(hB :
∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (t - r ^ 2) t), MeasureTheory.MemLp (fun (x : Parabolic.Vec3) => P (x, s)) (ENNReal.ofReal q) MeasureTheory.volume ∧ MeasureTheory.eLpNorm (fun (x : Parabolic.Vec3) => P (x, s)) (ENNReal.ofReal q) MeasureTheory.volume ≤ B s),
MeasureTheory.eLpNorm' P q (MeasureTheory.volume.restrict (Parabolic.parabolicCylinder x₀ t r)) ≤ (∫⁻ (s : ℝ) in Set.Ioc (t - r ^ 2) t, B s ^ q) ^ (1 / q)
The temporal source estimate needed by the p₁ bridge. Its right hand side
is the slice form of eq:slice-norm-bounds: the factor 9 is the concrete
U-tensor constant, and the numerical coefficient is fixed before the fields.
theorem
CKN.Foundation.Euclidean.utensor_slice_scale_bound
{Ω : Set Parabolic.Vec3}
{I : Set ℝ}
{q : ℝ}
{u : Parabolic.ParabolicPoint → Parabolic.Vec3}
{Du : Parabolic.ParabolicPoint → Fin 3 → Parabolic.Vec3}
{p : Parabolic.ParabolicPoint → ℝ}
{f : Parabolic.ParabolicPoint → Parabolic.Vec3}
(hsol : IsSuitableWeakSolutionIntegrable Ω I q u Du p f)
{z : Parabolic.ParabolicPoint}
{ρ r : ℝ}
(hρ : 0 < ρ)
(hr : 0 < r)
(hhalf : r ≤ ρ / 2)
(hsub : closure (Parabolic.parabolicCylinder z.1 z.2 ρ) ⊆ spaceTimeSet Ω I)
{C : ℝ}
(hC : 0 ≤ C)
:
The solution-level export below is the exact cylinder shape consumed by
thetaDecay_T_of_inputs. The hypothesis is the global L^(3/2) slice estimate;
the preceding two lemmas perform the product-measure and time-scaling steps.
theorem
CKN.Foundation.Euclidean.hCZ_p1_cylinder_of_global_slice
(C_CZ : ℝ)
(hC_CZ : 0 ≤ C_CZ)
{Ω : Set Parabolic.Vec3}
{I : Set ℝ}
{q : ℝ}
{u : Parabolic.ParabolicPoint → Parabolic.Vec3}
{Du : Parabolic.ParabolicPoint → Fin 3 → Parabolic.Vec3}
{p : Parabolic.ParabolicPoint → ℝ}
{f : Parabolic.ParabolicPoint → Parabolic.Vec3}
(hsol : IsSuitableWeakSolutionIntegrable Ω I q u Du p f)
{z : Parabolic.ParabolicPoint}
{ρ r : ℝ}
(hρ : 0 < ρ)
(hr : 0 < r)
(hhalf : r ≤ ρ / 2)
(hsub : closure (Parabolic.parabolicCylinder z.1 z.2 ρ) ⊆ spaceTimeSet Ω I)
(hCZ_p1 :
∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (z.2 - ρ ^ 2) z.2), MeasureTheory.MemLp
(fun (x : Parabolic.Vec3) =>
pressureP1 (mollifiedBallCutoff z.1 hρ) u
(fun (t : ℝ) (j : Fin 3) => ⨍ (y : Parabolic.Vec3) in Parabolic.vec3Ball z.1 ρ, u (y, t) j) p f s x)
(ENNReal.ofReal (3 / 2)) MeasureTheory.volume ∧ MeasureTheory.lpNorm
(fun (x : Parabolic.Vec3) =>
pressureP1 (mollifiedBallCutoff z.1 hρ) u
(fun (t : ℝ) (j : Fin 3) => ⨍ (y : Parabolic.Vec3) in Parabolic.vec3Ball z.1 ρ, u (y, t) j) p f s x)
(ENNReal.ofReal (3 / 2)) MeasureTheory.volume ≤ C_CZ * (∫ (y : Parabolic.Vec3) in Parabolic.vec3Ball z.1 ρ, utensorNorm u z.1 ρ s y ^ (3 / 2)) ^ (2 / 3))
:
ENNReal.ofReal (r ^ (-4 / 3)) * MeasureTheory.eLpNorm'
(fun (w : Parabolic.ParabolicPoint) =>
pressureP1 (mollifiedBallCutoff z.1 hρ) u
(fun (t : ℝ) (j : Fin 3) => ⨍ (y : Parabolic.Vec3) in Parabolic.vec3Ball z.1 ρ, u (y, t) j) p f w.2 w.1)
(3 / 2) (MeasureTheory.volume.restrict (Parabolic.parabolicCylinder z.1 z.2 r)) ≤ ENNReal.ofReal (C_CZ * (9 * sobolevPoincareL6Constant.toReal) * (r / ρ)⁻¹ * alpha u z ρ * beta u Du z ρ)
A comparison adapter lets the fixed coefficient used by the provider be chosen before the solution fields, as required by the theorem-A/B consumers.
theorem
CKN.Foundation.Euclidean.hCZ_p1_cylinder_of_global_slice_le
(C₁₂_p1 C_CZ : ℝ)
(hC_CZ : 0 ≤ C_CZ)
(hconst : C_CZ * (9 * sobolevPoincareL6Constant.toReal) ≤ C₁₂_p1)
{Ω : Set Parabolic.Vec3}
{I : Set ℝ}
{q : ℝ}
{u : Parabolic.ParabolicPoint → Parabolic.Vec3}
{Du : Parabolic.ParabolicPoint → Fin 3 → Parabolic.Vec3}
{p : Parabolic.ParabolicPoint → ℝ}
{f : Parabolic.ParabolicPoint → Parabolic.Vec3}
(hsol : IsSuitableWeakSolutionIntegrable Ω I q u Du p f)
{z : Parabolic.ParabolicPoint}
{ρ r : ℝ}
(hρ : 0 < ρ)
(hr : 0 < r)
(hhalf : r ≤ ρ / 2)
(hsub : closure (Parabolic.parabolicCylinder z.1 z.2 ρ) ⊆ spaceTimeSet Ω I)
(hCZ_p1 :
∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (z.2 - ρ ^ 2) z.2), MeasureTheory.MemLp
(fun (x : Parabolic.Vec3) =>
pressureP1 (mollifiedBallCutoff z.1 hρ) u
(fun (t : ℝ) (j : Fin 3) => ⨍ (y : Parabolic.Vec3) in Parabolic.vec3Ball z.1 ρ, u (y, t) j) p f s x)
(ENNReal.ofReal (3 / 2)) MeasureTheory.volume ∧ MeasureTheory.lpNorm
(fun (x : Parabolic.Vec3) =>
pressureP1 (mollifiedBallCutoff z.1 hρ) u
(fun (t : ℝ) (j : Fin 3) => ⨍ (y : Parabolic.Vec3) in Parabolic.vec3Ball z.1 ρ, u (y, t) j) p f s x)
(ENNReal.ofReal (3 / 2)) MeasureTheory.volume ≤ C_CZ * (∫ (y : Parabolic.Vec3) in Parabolic.vec3Ball z.1 ρ, utensorNorm u z.1 ρ s y ^ (3 / 2)) ^ (2 / 3))
:
ENNReal.ofReal (r ^ (-4 / 3)) * MeasureTheory.eLpNorm'
(fun (w : Parabolic.ParabolicPoint) =>
pressureP1 (mollifiedBallCutoff z.1 hρ) u
(fun (t : ℝ) (j : Fin 3) => ⨍ (y : Parabolic.Vec3) in Parabolic.vec3Ball z.1 ρ, u (y, t) j) p f w.2 w.1)
(3 / 2) (MeasureTheory.volume.restrict (Parabolic.parabolicCylinder z.1 z.2 r)) ≤ ENNReal.ofReal (C₁₂_p1 * (r / ρ)⁻¹ * alpha u z ρ * beta u Du z ρ)