A bilinear bound for the centered tensor source #
The source paired with eq:Uij contains the mean-free velocity in its second
factor. Spatial Hölder bounds this factor separately, retaining the cutoff
cost needed for the time estimate of eq:pressure-gradient-morrey.
The scalar Hölder proofs follow PressureGradientSourceBounds.
theorem
CKN.Core.Step4.origin_centered_tensor_source_slice_bound
{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}
{c : Foundation.Parabolic.Vec3}
{i : Fin 3}
{Cη Cdη : ℝ}
{KU KD KW : ENNReal}
(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 :
MeasureTheory.eLpNorm (fun (x : Foundation.Parabolic.Vec3) => u x i) (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)
(hW :
∀ (j : Fin 3),
MeasureTheory.eLpNorm (fun (x : Foundation.Parabolic.Vec3) => u x j - c j) (ENNReal.ofReal 3)
(MeasureTheory.volume.restrict B) ≤ KW)
(hUm :
∀ (j : Fin 3),
MeasureTheory.AEStronglyMeasurable (fun (x : Foundation.Parabolic.Vec3) => u x j) (MeasureTheory.volume.restrict B))
(hDm :
∀ (j : Fin 3),
MeasureTheory.AEStronglyMeasurable (fun (x : Foundation.Parabolic.Vec3) => Du x i j)
(MeasureTheory.volume.restrict B))
:
MeasureTheory.eLpNorm
(fun (x : Foundation.Parabolic.Vec3) => pressureDivergenceCutoffSourceCentredTensor η dη u Du c x i)
(ENNReal.ofReal (6 / 5)) (MeasureTheory.volume.restrict B) ≤ 3 * (ENNReal.ofReal Cη * KD * KW + ENNReal.ofReal Cdη * (KU * KW * MeasureTheory.volume B ^ (1 / 6)))
A centered tensor source component is controlled by a gradient product and a cutoff-weighted quadratic product, with no force contribution.