Lin34 Centred Source

Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.

noncomputable def CKN.lin34CentredSource (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (x₀ : Foundation.Parabolic.Vec3) {ρ : ℝ} (hρ : 0 < ρ) (s : ℝ) (i j : Fin 3) : Foundation.Parabolic.Vec3 → ℝ

The cut-off, doubly centred velocity tensor that enters the Calderón--Zygmund estimate of prop:lin34 as its source: with η the mollified cut-off of B_ρ and Û the centred tensor eq:Uhat, at the time s and in the entries i, j it is the function

x ↦ η(x) · Û_{ij}(x, s).

Equations

• CKN.lin34CentredSource u x₀ hρ s i j x = CKN.mollifiedBallCutoff x₀ hρ x * CKN.pressureUTensor (CKN.lin34CentredVelocity u x₀ ρ) 0 (x, s) i j

theorem CKN.lin34CentredSource_eq_zero_of_notMem (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (x₀ : Foundation.Parabolic.Vec3) {ρ : ℝ} (hρ : 0 < ρ) (s : ℝ) (i j : Fin 3) {y : Foundation.Parabolic.Vec3} (hy : y ∉ euclideanBall x₀ ρ) : lin34CentredSource u x₀ hρ s i j y = 0

The cut-off is supported well inside B_ρ, so the centred source tensor vanishes off the ball carrying the velocity oscillation of eq:Chat.

theorem CKN.lin34CentredSource_hasCompactSupport (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (x₀ : Foundation.Parabolic.Vec3) {ρ : ℝ} (hρ : 0 < ρ) (s : ℝ) (i j : Fin 3) : HasCompactSupport (lin34CentredSource u x₀ hρ s i j)

The centred source tensor is compactly supported: it vanishes outside the closed ball of radius 3ρ/4, which carries the support of the mollified cut-off.

theorem CKN.lin34CentredSource_memLp_and_lpNorm_le {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {x₀ : Foundation.Parabolic.Vec3} {ρ : ℝ} (hρ : 0 < ρ) {s : ℝ} (hu : MeasureTheory.AEStronglyMeasurable (fun (y : Foundation.Parabolic.Vec3) => u (y, s)) (MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball x₀ ρ))) (hv : MeasureTheory.IntegrableOn (fun (y : Foundation.Parabolic.Vec3) => Foundation.Parabolic.vec3EuclideanNorm (meanFreeVec u x₀ ρ s y) ^ 3) (euclideanBall x₀ ρ) MeasureTheory.volume) (i j : Fin 3) : MeasureTheory.MemLp (lin34CentredSource u x₀ hρ s i j) (ENNReal.ofReal (3 / 2)) MeasureTheory.volume ∧ MeasureTheory.lpNorm (lin34CentredSource u x₀ hρ s i j) (ENNReal.ofReal (3 / 2)) MeasureTheory.volume ≤ (∫ (y : Vec 3) in euclideanBall x₀ ρ, Foundation.Parabolic.vec3EuclideanNorm (meanFreeVec u x₀ ρ s y) ^ 3) ^ (2 / 3)

The L^{3/2} source estimate of prop:lin34: each entry of the cut-off centred velocity tensor lies in L^{3/2}(ℝ³), with norm at most (∫_{B_ρ} |v(·,s)|³)^{2/3}, the square of the L³(B_ρ) norm of the mean-free velocity. These are the source facts the Calderón--Zygmund input ext:CZ consumes.

theorem CKN.lin34CentredSource_sum_lpNorm_le {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {x₀ : Foundation.Parabolic.Vec3} {ρ : ℝ} (hρ : 0 < ρ) {s : ℝ} (hu : MeasureTheory.AEStronglyMeasurable (fun (y : Foundation.Parabolic.Vec3) => u (y, s)) (MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball x₀ ρ))) (hv : MeasureTheory.IntegrableOn (fun (y : Foundation.Parabolic.Vec3) => Foundation.Parabolic.vec3EuclideanNorm (meanFreeVec u x₀ ρ s y) ^ 3) (euclideanBall x₀ ρ) MeasureTheory.volume) : ∑ i : Fin 3, ∑ j : Fin 3, MeasureTheory.lpNorm (lin34CentredSource u x₀ hρ s i j) (ENNReal.ofReal (3 / 2)) MeasureTheory.volume ≤ 9 * (∫ (y : Vec 3) in euclideanBall x₀ ρ, Foundation.Parabolic.vec3EuclideanNorm (meanFreeVec u x₀ ρ s y) ^ 3) ^ (2 / 3)

The nine-entry form of the source estimate, as the tensor pressure operator of prop:pressure-decomposition consumes it: the sum of the L^{3/2} norms of the entries of the cut-off centred velocity tensor is at most nine times the square of the L³(B_ρ) norm of the mean-free velocity.