Pressure Gradient Source Bounds

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

def CKN.Core.Step4.pressureDivergenceCutoffSource (η : Foundation.Parabolic.Vec3 → ℝ) (dη : Fin 3 → Foundation.Parabolic.Vec3 → ℝ) (u : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (Du : Foundation.Parabolic.Vec3 → Fin 3 → Foundation.Parabolic.Vec3) (f : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3

The product-rule source obtained after inserting a spatial cutoff into the quadratic tensor. The field dη j is the j-th spatial derivative of the cutoff; its analytic derivative estimate is passed at the use site.

Equations

• CKN.Core.Step4.pressureDivergenceCutoffSource η dη u Du f x i = ∑ j : Fin 3, (η x * Du x i j * u x j + dη j x * u x i * u x j) - η x * f x i

A cutoff does not change the product exponents. The two cutoff bounds are kept as separate parameters so that the spatial derivative contribution can be instantiated with C₁₀ / ρ.

theorem CKN.Core.Step4.pressure_divergence_cutoff_source_slice_component_le {B : Set Foundation.Parabolic.Vec3} {η : Foundation.Parabolic.Vec3 → ℝ} {dη : Fin 3 → Foundation.Parabolic.Vec3 → ℝ} {u : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} {Du : Foundation.Parabolic.Vec3 → Fin 3 → Foundation.Parabolic.Vec3} {f : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} {i : Fin 3} {q Cη Cdη : ℝ} {KU KD KF : ENNReal} (hq : 5 / 2 < q) (hμ : (MeasureTheory.volume.restrict B) Set.univ < ⊤) (hCη : 0 ≤ Cη) (hCdη : 0 ≤ Cdη) (hη : MeasureTheory.AEStronglyMeasurable η (MeasureTheory.volume.restrict B)) (hηbound : ∀ᵐ (x : Foundation.Parabolic.Vec3) ∂MeasureTheory.volume.restrict B, |η x| ≤ Cη) (hdη : ∀ (j : Fin 3), MeasureTheory.AEStronglyMeasurable (dη j) (MeasureTheory.volume.restrict B)) (hdηbound : ∀ (j : Fin 3), ∀ᵐ (x : Foundation.Parabolic.Vec3) ∂MeasureTheory.volume.restrict B, |dη j x| ≤ Cdη) (hU : ∀ (j : Fin 3), MeasureTheory.eLpNorm (fun (x : Foundation.Parabolic.Vec3) => u x j) (ENNReal.ofReal 3) (MeasureTheory.volume.restrict B) ≤ KU) (hD : ∀ (j : Fin 3), MeasureTheory.eLpNorm (fun (x : Foundation.Parabolic.Vec3) => Du x i j) (ENNReal.ofReal 2) (MeasureTheory.volume.restrict B) ≤ KD) (hF : MeasureTheory.eLpNorm (fun (x : Foundation.Parabolic.Vec3) => f x i) (ENNReal.ofReal q) (MeasureTheory.volume.restrict B) ≤ KF) (hUmeas : ∀ (j : Fin 3), MeasureTheory.AEStronglyMeasurable (fun (x : Foundation.Parabolic.Vec3) => u x j) (MeasureTheory.volume.restrict B)) (hDmeas : ∀ (j : Fin 3), MeasureTheory.AEStronglyMeasurable (fun (x : Foundation.Parabolic.Vec3) => Du x i j) (MeasureTheory.volume.restrict B)) (hFmeas : MeasureTheory.AEStronglyMeasurable (fun (x : Foundation.Parabolic.Vec3) => f x i) (MeasureTheory.volume.restrict B)) : MeasureTheory.eLpNorm (fun (x : Foundation.Parabolic.Vec3) => pressureDivergenceCutoffSource η dη u Du f x i) (ENNReal.ofReal (6 / 5)) (MeasureTheory.volume.restrict B) ≤ 3 * (ENNReal.ofReal Cη * KD * KU + ENNReal.ofReal Cdη * (KU * KU * (MeasureTheory.volume.restrict B) Set.univ ^ (1 / 6))) + ENNReal.ofReal Cη * (KF * (MeasureTheory.volume.restrict B) Set.univ ^ (5 / 6 - 1 / q))

theorem CKN.Core.Step4.pressure_divergence_cutoff_source_slice_le {B : Set Foundation.Parabolic.Vec3} {η : Foundation.Parabolic.Vec3 → ℝ} {dη : Fin 3 → Foundation.Parabolic.Vec3 → ℝ} {u : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} {Du : Foundation.Parabolic.Vec3 → Fin 3 → Foundation.Parabolic.Vec3} {f : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} {q Cη Cdη : ℝ} {KU KD KF : ENNReal} (hq : 5 / 2 < q) (hμ : (MeasureTheory.volume.restrict B) Set.univ < ⊤) (hCη : 0 ≤ Cη) (hCdη : 0 ≤ Cdη) (hη : MeasureTheory.AEStronglyMeasurable η (MeasureTheory.volume.restrict B)) (hηbound : ∀ᵐ (x : Foundation.Parabolic.Vec3) ∂MeasureTheory.volume.restrict B, |η x| ≤ Cη) (hdη : ∀ (j : Fin 3), MeasureTheory.AEStronglyMeasurable (dη j) (MeasureTheory.volume.restrict B)) (hdηbound : ∀ (j : Fin 3), ∀ᵐ (x : Foundation.Parabolic.Vec3) ∂MeasureTheory.volume.restrict B, |dη j x| ≤ Cdη) (hU : ∀ (j : Fin 3), MeasureTheory.eLpNorm (fun (x : Foundation.Parabolic.Vec3) => u x j) (ENNReal.ofReal 3) (MeasureTheory.volume.restrict B) ≤ KU) (hD : ∀ (i j : Fin 3), MeasureTheory.eLpNorm (fun (x : Foundation.Parabolic.Vec3) => Du x i j) (ENNReal.ofReal 2) (MeasureTheory.volume.restrict B) ≤ KD) (hF : ∀ (i : Fin 3), MeasureTheory.eLpNorm (fun (x : Foundation.Parabolic.Vec3) => f x i) (ENNReal.ofReal q) (MeasureTheory.volume.restrict B) ≤ KF) (hUmeas : ∀ (j : Fin 3), MeasureTheory.AEStronglyMeasurable (fun (x : Foundation.Parabolic.Vec3) => u x j) (MeasureTheory.volume.restrict B)) (hDmeas : ∀ (i j : Fin 3), MeasureTheory.AEStronglyMeasurable (fun (x : Foundation.Parabolic.Vec3) => Du x i j) (MeasureTheory.volume.restrict B)) (hFmeas : ∀ (i : Fin 3), MeasureTheory.AEStronglyMeasurable (fun (x : Foundation.Parabolic.Vec3) => f x i) (MeasureTheory.volume.restrict B)) : MeasureTheory.eLpNorm (fun (x : Foundation.Parabolic.Vec3) => pressureDivergenceCutoffSource η dη u Du f x) (ENNReal.ofReal (6 / 5)) (MeasureTheory.volume.restrict B) ≤ 3 * (3 * (ENNReal.ofReal Cη * KD * KU + ENNReal.ofReal Cdη * (KU * KU * (MeasureTheory.volume.restrict B) Set.univ ^ (1 / 6))) + ENNReal.ofReal Cη * (KF * (MeasureTheory.volume.restrict B) Set.univ ^ (5 / 6 - 1 / q)))