CZStart Bridge Source #
Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.
theorem
CKN.memLp_three_halves_of_velocity_square_bound
{g : Foundation.Parabolic.Vec3 → ℝ}
{v : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3}
{x₀ : Foundation.Parabolic.Vec3}
{ρ : ℝ}
(hg : MeasureTheory.AEStronglyMeasurable g MeasureTheory.volume)
(hv :
MeasureTheory.IntegrableOn (fun (y : Foundation.Parabolic.Vec3) => Foundation.Parabolic.vec3EuclideanNorm (v y) ^ 3)
(euclideanBall x₀ ρ) MeasureTheory.volume)
(hzero : ∀ y ∉ euclideanBall x₀ ρ, g y = 0)
(hbound : ∀ (y : Foundation.Parabolic.Vec3), |g y| ≤ Foundation.Parabolic.vec3EuclideanNorm (v y) ^ 2)
:
MeasureTheory.MemLp g (ENNReal.ofReal (3 / 2)) MeasureTheory.volume
A function g that vanishes off the ball B(x₀,ρ) and satisfies
|g| ≤ |v| ^ 2 there lies in L^{3/2} whenever the velocity cube
|v| ^ 3 is integrable on that ball. This is the exponent bookkeeping for the
L^{3/2} pressure energy in the oscillation estimate eq:Chat.
theorem
CKN.lpNorm_three_halves_le_of_velocity_square_bound
{g : Foundation.Parabolic.Vec3 → ℝ}
{v : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3}
{x₀ : Foundation.Parabolic.Vec3}
{ρ : ℝ}
(hg : MeasureTheory.AEStronglyMeasurable g MeasureTheory.volume)
(hv :
MeasureTheory.IntegrableOn (fun (y : Foundation.Parabolic.Vec3) => Foundation.Parabolic.vec3EuclideanNorm (v y) ^ 3)
(euclideanBall x₀ ρ) MeasureTheory.volume)
(hzero : ∀ y ∉ euclideanBall x₀ ρ, g y = 0)
(hbound : ∀ (y : Foundation.Parabolic.Vec3), |g y| ≤ Foundation.Parabolic.vec3EuclideanNorm (v y) ^ 2)
:
MeasureTheory.lpNorm g (ENNReal.ofReal (3 / 2)) MeasureTheory.volume ≤ (∫ (y : Vec 3) in euclideanBall x₀ ρ, Foundation.Parabolic.vec3EuclideanNorm (v y) ^ 3) ^ (2 / 3)
Quantitative L^{3/2} pressure bound: if g vanishes off the ball
B(x₀,ρ) and |g| ≤ |v| ^ 2 there, then the L^{3/2} norm of g is at most
(∫_{B(x₀,ρ)} |v| ^ 3) ^ (2/3). This is the scale-invariant form in which the
velocity enters the pressure oscillation estimate eq:Chat.