Pressure Gradient

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

The selector is scalar. This wrapper applies it to the three spatial components and packages the resulting representatives as one native Vec3 field. All analytic work is deliberately left in the slice hypothesis: the wrapper only performs the finite-dimensional measurable assembly.

theorem CKN.Core.Step4.pressure_gradient_spacetime_selection_with_slice_bounds {B B' : Set Foundation.Parabolic.Vec3} {J : Set ℝ} {p : Foundation.Parabolic.ParabolicPoint → ℝ} {K : Fin 3 → ℝ → ENNReal} (hB : IsOpen B) (hB' : MeasurableSet B') (hB'c : IsCompact (closure B')) (hB'B : closure B' ⊆ B) (hp : MeasureTheory.IntegrableOn p (B ×ˢ J) MeasureTheory.volume) (hslice : ∀ (k : Fin 3), ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict J, ∃ (g : Foundation.Parabolic.Vec3 → ℝ), MeasureTheory.LocallyIntegrableOn g B MeasureTheory.volume ∧ HasWeakPartialDerivOn B k (fun (x : Vec 3) => p (x, t)) g ∧ MeasureTheory.eLpNorm g (ENNReal.ofReal (6 / 5)) (MeasureTheory.volume.restrict B') ≤ K k t) : ∃ (Dp : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3), (∀ (k : Fin 3), AEMeasurable (fun (z : Foundation.Parabolic.ParabolicPoint) => Dp z k) (MeasureTheory.volume.restrict (B' ×ˢ J))) ∧ (∀ (k : Fin 3), ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict J, MeasureTheory.eLpNorm (fun (x : Foundation.Parabolic.Vec3) => Dp (x, t) k) (ENNReal.ofReal (6 / 5)) (MeasureTheory.volume.restrict B') ≤ K k t) ∧ (∀ (k : Fin 3) (Ψ : Foundation.Parabolic.Vec3 × ℝ → ℝ), ContDiff ℝ (↑⊤) Ψ → HasCompactSupport Ψ → tsupport Ψ ⊆ B' ×ˢ J → ∫ (t : ℝ) in J, ∫ (x : Foundation.Parabolic.Vec3) in B', p (x, t) * spatialPartial Ψ k (x, t) = -∫ (t : ℝ) in J, ∫ (x : Foundation.Parabolic.Vec3) in B', Dp (x, t) k * Ψ (x, t)) ∧ ∀ (k : Fin 3) (Ψ : Foundation.Parabolic.Vec3 × ℝ → ℝ), ContDiff ℝ (↑⊤) Ψ → HasCompactSupport Ψ → tsupport Ψ ⊆ B' ×ˢ J → MeasureTheory.IntegrableOn (fun (z : Foundation.Parabolic.ParabolicPoint) => p z * spatialPartial Ψ k z) (B' ×ˢ J) MeasureTheory.volume → MeasureTheory.IntegrableOn (fun (z : Foundation.Parabolic.ParabolicPoint) => Dp z k * Ψ z) (B' ×ˢ J) MeasureTheory.volume → ∫ (z : Foundation.Parabolic.Vec3 × ℝ) in B' ×ˢ J, p z * spatialPartial Ψ k z = -∫ (z : Foundation.Parabolic.Vec3 × ℝ) in B' ×ˢ J, Dp z k * Ψ z

Integrating the one-scale display over a one-sided time interval is a direct order argument. The spatial fields may be chosen independently on the almost-everywhere set; this is the form consumed by the parabolic decay layer.

theorem CKN.Core.Step4.pressure_gradient_two_scale_decay {Φ V : ℝ → ℝ} {C₃ ρ r : ℝ} (hC₃ : 0 ≤ C₃) : 0 < ρ → 0 < r → r ≤ ρ / 8 → ∀ (hΦ : 0 ≤ Φ ρ) (hdecomp : Φ r ≤ V r + Φ (r / 2)) (hpart : V r ≤ C₃ * (r / ρ) ^ 3 * V ρ) (hharm : Φ (r / 2) ≤ C₃ * (r / ρ) ^ 3 * (Φ ρ + V ρ)), Φ r ≤ 2 * C₃ * (r / ρ) ^ 3 * (Φ ρ + V ρ)

theorem CKN.Core.Step4.pressure_gradient_morrey_bound {κ : ℝ} {g : Foundation.Parabolic.ParabolicPoint → ℝ} {C : ENNReal} (hcell : ∀ (z : Foundation.Parabolic.ParabolicPoint) (r : { r : ℝ // 0 < r }), Foundation.Parabolic.Morrey.morreyCell (6 / 5) κ g z ↑r ≤ C) : Foundation.Parabolic.Morrey.morreyNorm (6 / 5) κ g ≤ C