Lin34 Slice Core #
Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.
The centred pressure decomposition on one time slice #
This file runs the local pressure decomposition of prop:pressure-decomposition
(paper/ckn.tex) with the doubly centred nonlinearity eq:Uhat of
lem:delta-p-centred in place of the raw one, which is the form the oscillation
estimate prop:lin34 uses: the velocity then enters only through the mean-free
field u - ⨍_{B_ρ} u of eq:Chat.
noncomputable def
CKN.lin34CentredVelocity
(u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3)
(x₀ : Foundation.Parabolic.Vec3)
(ρ : ℝ)
:
The mean-free velocity field w = u - ⨍_{B_ρ} u of eq:Uhat in
paper/ckn.tex, seen as a field on space-time.
Equations
- CKN.lin34CentredVelocity u x₀ ρ w = CKN.meanFreeVec u x₀ ρ w.2 w.1
Instances For
theorem
CKN.lin34_pressureUTensor_centred
(u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3)
(x₀ : Foundation.Parabolic.Vec3)
(ρ s : ℝ)
(y : Foundation.Parabolic.Vec3)
(i j : Fin 3)
:
pressureUTensor (lin34CentredVelocity u x₀ ρ) 0 (y, s) i j = -meanFreeVec u x₀ ρ s y i * meanFreeVec u x₀ ρ s y j
The centred tensor Û_{ij} = -(u_i - ⨍u_i)(u_j - ⨍u_j) of eq:Uhat is the
tensor of the decomposition run with the mean-free field and a zero average.
theorem
CKN.lin34_pressureUTensorNorm_centred
(u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3)
(x₀ : Foundation.Parabolic.Vec3)
(ρ s : ℝ)
(y : Foundation.Parabolic.Vec3)
:
pressureUTensorNorm (lin34CentredVelocity u x₀ ρ) 0 s y = Foundation.Parabolic.vec3EuclideanNorm (meanFreeVec u x₀ ρ s y) ^ 2
The pointwise norm of the centred tensor is the square of the mean-free
velocity, which is the identity |Û| ≤ |w|² of prop:lin34 in equality form.
theorem
CKN.lin34_centredVelocity_slice_eq
(u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3)
(x₀ : Foundation.Parabolic.Vec3)
(ρ s : ℝ)
:
(fun (y : Foundation.Parabolic.Vec3) => lin34CentredVelocity u x₀ ρ (y, s)) = (fun (y : Foundation.Parabolic.Vec3) => u (y, s)) - fun (x : Foundation.Parabolic.Vec3) (j : Fin 3) =>
⨍ (w : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball x₀ ρ, u (w, s) j
The mean-free field of a time slice is the slice minus a constant vector.
theorem
CKN.lin34_centredVelocity_memLp
{u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
{x₀ : Foundation.Parabolic.Vec3}
{ρ s : ℝ}
(hu :
MeasureTheory.MemLp (fun (y : Foundation.Parabolic.Vec3) => u (y, s)) 2
(MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball x₀ ρ)))
:
MeasureTheory.MemLp (fun (y : Foundation.Parabolic.Vec3) => lin34CentredVelocity u x₀ ρ (y, s)) 2
(MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball x₀ ρ))
The mean-free slice inherits the square integrability of the velocity slice.
theorem
CKN.lin34_centred_P234_sup_bound
{u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
{x₀ : Foundation.Parabolic.Vec3}
{ρ r s : ℝ}
(hρ : 0 < ρ)
(hr : 0 < r)
(hhalf : r ≤ ρ / 2)
(hu :
MeasureTheory.MemLp (fun (y : Foundation.Parabolic.Vec3) => u (y, s)) 2
(MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball x₀ ρ)))
:
AEMeasurable (fun (y : Foundation.Parabolic.Vec3) => u (y, s))
(MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball x₀ ρ)) →
∀ x ∈ Foundation.Parabolic.vec3Ball x₀ r,
|pressureP2 (mollifiedBallCutoff x₀ hρ) (lin34CentredVelocity u x₀ ρ) 0 s x| + |pressureP3 (mollifiedBallCutoff x₀ hρ) (lin34CentredVelocity u x₀ ρ) 0 s x| + |pressureP4 (mollifiedBallCutoff x₀ hρ) (lin34CentredVelocity u x₀ ρ) 0 s x| ≤ (18 * cutoffSecondDerivativeConstant + 720 * cutoffGradientConstant) / ρ ^ 3 * ∫ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball x₀ ρ, Foundation.Parabolic.vec3EuclideanNorm (meanFreeVec u x₀ ρ s y) ^ 2
The far-field bound of lem:pk-bounds(b) for the centred potentials
p₂, p₃, p₄ of prop:lin34: on the inner ball they are dominated by the
L¹ norm of the centred tensor eq:Uhat.
theorem
CKN.lin34_P56_sup_bound
{p : Foundation.Parabolic.ParabolicPoint → ℝ}
{x₀ : Foundation.Parabolic.Vec3}
{ρ r s : ℝ}
(hρ : 0 < ρ)
(hr : 0 < r)
(hhalf : r ≤ ρ / 2)
(hp :
MeasureTheory.Integrable (fun (y : Foundation.Parabolic.Vec3) => |p (y, s)|)
(MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball x₀ ρ)))
(hpm :
MeasureTheory.AEStronglyMeasurable (fun (y : Foundation.Parabolic.Vec3) => p (y, s))
(MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball x₀ ρ)))
(x : Foundation.Parabolic.Vec3)
:
x ∈ Foundation.Parabolic.vec3Ball x₀ r →
|pressureP5 (mollifiedBallCutoff x₀ hρ) p s x| + |pressureP6 (mollifiedBallCutoff x₀ hρ) p s x| ≤ (18 * cutoffSecondDerivativeConstant + 240 * cutoffGradientConstant) / ρ ^ 3 * ∫ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball x₀ ρ, |p (y, s)|
The far-field bound of lem:pk-bounds(c) for p₅, p₆ on the inner ball,
in the form used by prop:lin34.
The constant of the far-field potential bounds of lem:pk-bounds(b)--(c)
used in prop:lin34.
Equations
Instances For
noncomputable def
CKN.lin34CentredRemainder
(u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3)
(p : Foundation.Parabolic.ParabolicPoint → ℝ)
(x₀ : Foundation.Parabolic.Vec3)
(ρ : ℝ)
(hρ : 0 < ρ)
(s : ℝ)
:
The group p₂ + p₃ + p₄ + p₅ + p₆ of the decomposition
prop:pressure-decomposition, run with the centred tensor eq:Uhat: this is
the part of the pressure that carries the factor r/ρ in
eq:lin34-pointwise.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CKN.lin34_centred_remainder_sup_bound
{u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
{p : Foundation.Parabolic.ParabolicPoint → ℝ}
{x₀ : Foundation.Parabolic.Vec3}
{ρ s : ℝ}
(hρ : 0 < ρ)
(hu :
MeasureTheory.MemLp (fun (y : Foundation.Parabolic.Vec3) => u (y, s)) 2
(MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball x₀ ρ)))
(humeas :
AEMeasurable (fun (y : Foundation.Parabolic.Vec3) => u (y, s))
(MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball x₀ ρ)))
(hpint :
MeasureTheory.Integrable (fun (y : Foundation.Parabolic.Vec3) => |p (y, s)|)
(MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball x₀ ρ)))
(hpm :
MeasureTheory.AEStronglyMeasurable (fun (y : Foundation.Parabolic.Vec3) => p (y, s))
(MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball x₀ ρ)))
(x : Foundation.Parabolic.Vec3)
:
x ∈ Foundation.Parabolic.vec3Ball x₀ (ρ / 2) →
|lin34CentredRemainder u p x₀ ρ hρ s x| ≤ lin34CutoffConstant / ρ ^ 3 * ((∫ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball x₀ ρ, Foundation.Parabolic.vec3EuclideanNorm (meanFreeVec u x₀ ρ s y) ^ 2) + ∫ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball x₀ ρ, |p (y, s)|)
The far-field bounds of lem:pk-bounds(b)--(c) combined: on the half ball
the group p₂ + ⋯ + p₆ is bounded by ρ⁻³ times the L¹ norms of the centred
tensor and of the pressure.
theorem
CKN.lin34_centred_remainder_sup_bound_rpow
{u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
{p : Foundation.Parabolic.ParabolicPoint → ℝ}
{x₀ : Foundation.Parabolic.Vec3}
{ρ s : ℝ}
(hρ : 0 < ρ)
(hu :
MeasureTheory.MemLp (fun (y : Foundation.Parabolic.Vec3) => u (y, s)) 2
(MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball x₀ ρ)))
(humeas :
AEMeasurable (fun (y : Foundation.Parabolic.Vec3) => u (y, s))
(MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball x₀ ρ)))
(hpint :
MeasureTheory.Integrable (fun (y : Foundation.Parabolic.Vec3) => |p (y, s)|)
(MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball x₀ ρ)))
(hpm :
MeasureTheory.AEStronglyMeasurable (fun (y : Foundation.Parabolic.Vec3) => p (y, s))
(MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball x₀ ρ)))
(hVint :
MeasureTheory.Integrable
(fun (y : Foundation.Parabolic.Vec3) => Foundation.Parabolic.vec3EuclideanNorm (meanFreeVec u x₀ ρ s y) ^ 3)
(MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball x₀ ρ)))
(hPint :
MeasureTheory.Integrable (fun (y : Foundation.Parabolic.Vec3) => |p (y, s)| ^ (3 / 2))
(MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball x₀ ρ)))
(x : Foundation.Parabolic.Vec3)
:
x ∈ Foundation.Parabolic.vec3Ball x₀ (ρ / 2) →
|lin34CentredRemainder u p x₀ ρ hρ s x| ≤ (4 * Real.pi / 3) ^ (1 / 3) * lin34CutoffConstant * (ρ ^ 2)⁻¹ * ((∫ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball x₀ ρ, Foundation.Parabolic.vec3EuclideanNorm (meanFreeVec u x₀ ρ s y) ^ 3) ^ (2 / 3) + (∫ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball x₀ ρ, |p (y, s)| ^ (3 / 2)) ^ (2 / 3))
The far-field bound of lem:pk-bounds(b)--(c) after the Hölder step of
prop:lin34: the group p₂ + ⋯ + p₆ is bounded on the half ball by
ρ⁻² times the oscillation and pressure quantities of eq:Chat.
theorem
CKN.lin34_centred_remainder_integral_bound
{u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
{p : Foundation.Parabolic.ParabolicPoint → ℝ}
{x₀ : Foundation.Parabolic.Vec3}
{ρ r s : ℝ}
(hρ : 0 < ρ)
(hr : 0 < r)
(hhalf : r ≤ ρ / 2)
(hu :
MeasureTheory.MemLp (fun (y : Foundation.Parabolic.Vec3) => u (y, s)) 2
(MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball x₀ ρ)))
(humeas :
AEMeasurable (fun (y : Foundation.Parabolic.Vec3) => u (y, s))
(MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball x₀ ρ)))
(hpint :
MeasureTheory.Integrable (fun (y : Foundation.Parabolic.Vec3) => |p (y, s)|)
(MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball x₀ ρ)))
(hpm :
MeasureTheory.AEStronglyMeasurable (fun (y : Foundation.Parabolic.Vec3) => p (y, s))
(MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball x₀ ρ)))
(hVint :
MeasureTheory.Integrable
(fun (y : Foundation.Parabolic.Vec3) => Foundation.Parabolic.vec3EuclideanNorm (meanFreeVec u x₀ ρ s y) ^ 3)
(MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball x₀ ρ)))
(hPint :
MeasureTheory.Integrable (fun (y : Foundation.Parabolic.Vec3) => |p (y, s)| ^ (3 / 2))
(MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball x₀ ρ)))
(hHmem :
MeasureTheory.MemLp (lin34CentredRemainder u p x₀ ρ hρ s) (ENNReal.ofReal (3 / 2))
(MeasureTheory.volume.restrict (euclideanBall x₀ r)))
:
∫ (x : Vec 3) in euclideanBall x₀ r, |lin34CentredRemainder u p x₀ ρ hρ s x| ^ (3 / 2) ≤ lin34RemainderConstant * (r / ρ) ^ 3 * ((∫ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball x₀ ρ, Foundation.Parabolic.vec3EuclideanNorm (meanFreeVec u x₀ ρ s y) ^ 3) + ∫ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball x₀ ρ, |p (y, s)| ^ (3 / 2))
The L^{3/2} bound on the inner ball for the group p₂ + ⋯ + p₆: this is
the second term of eq:lin34-pointwise, with its decay factor (r/ρ)³.
noncomputable def
CKN.lin34CentredP1
(u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3)
(p : Foundation.Parabolic.ParabolicPoint → ℝ)
(f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3)
(x₀ : Foundation.Parabolic.Vec3)
(ρ : ℝ)
(hρ : 0 < ρ)
(s : ℝ)
:
The Calderón--Zygmund part p₁ of prop:pressure-decomposition, run with
the centred tensor eq:Uhat. This is the object the external input
ext:CZ bounds in the proof of prop:lin34.
Equations
- CKN.lin34CentredP1 u p f x₀ ρ hρ s = CKN.pressureP1 (CKN.mollifiedBallCutoff x₀ hρ) (CKN.lin34CentredVelocity u x₀ ρ) 0 p f s
Instances For
noncomputable def
CKN.lin34ForcePart
(f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3)
(x₀ : Foundation.Parabolic.Vec3)
(ρ : ℝ)
(hρ : 0 < ρ)
(s : ℝ)
:
The force group p₇ + p₈ of prop:pressure-decomposition.
Equations
- CKN.lin34ForcePart f x₀ ρ hρ s = CKN.pressureP7 (CKN.mollifiedBallCutoff x₀ hρ) f s + CKN.pressureP8 (CKN.mollifiedBallCutoff x₀ hρ) f s
Instances For
theorem
CKN.lin34_centred_decomposition_on_inner
{u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
{p : Foundation.Parabolic.ParabolicPoint → ℝ}
{f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
{x₀ : Foundation.Parabolic.Vec3}
{ρ s : ℝ}
(hρ : 0 < ρ)
:
(fun (x : Foundation.Parabolic.Vec3) => p (x, s)) =ᵐ[MeasureTheory.volume.restrict (euclideanBall x₀ (13 * ρ / 20))]
lin34CentredP1 u p f x₀ ρ hρ s + lin34CentredRemainder u p x₀ ρ hρ s + lin34ForcePart f x₀ ρ hρ s
On the inner ball B_{13ρ/20} the pressure splits as
p = p₁ + (p₂ + ⋯ + p₆) + (p₇ + p₈); this is
prop:pressure-decomposition with the cutoff equal to one.