Pressure Gradient Base

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

The distributional pressure-Laplacian pairing.

def CKN.Core.Step4.HasPressureDeltaOn {U : Set Foundation.Parabolic.Vec3} (p : Foundation.Parabolic.Vec3 → ℝ) (u f : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) : Prop

Distributional pressure Poisson identity on a spatial domain, retaining the force contribution.

Equations

• One or more equations did not get rendered due to their size.

theorem CKN.Core.Step4.pressure_gradient_one_scale {i : Fin 3} {ρ C_CZ C_H : ℝ} : 0 < ρ → ∀ {G p : Foundation.Parabolic.Vec3 → ℝ} {D gp gh : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} {x₀ : Foundation.Parabolic.Vec3}, MeasureTheory.MemLp G (ENNReal.ofReal (6 / 5)) MeasureTheory.volume → HasCompactSupport G → MeasureTheory.MemLp D (ENNReal.ofReal (6 / 5)) MeasureTheory.volume → (∀ (j : Fin 3) (ψ : Foundation.Parabolic.Vec3 → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → ∫ (x : Foundation.Parabolic.Vec3), pressureNewtonianDerivativePotential i G x * spatialDeriv ψ j x = -∫ (x : Foundation.Parabolic.Vec3), D x j * ψ x) → ∀ (hrepresentation : ∀ᵐ (x : Foundation.Parabolic.Vec3) ∂MeasureTheory.volume.restrict (euclideanBall x₀ (ρ / 2)), gp x = D x + gh x) (hD_bound : MeasureTheory.eLpNorm D (ENNReal.ofReal (6 / 5)) MeasureTheory.volume ≤ ENNReal.ofReal C_CZ * MeasureTheory.eLpNorm G (ENNReal.ofReal (6 / 5)) MeasureTheory.volume) (hgh : MeasureTheory.eLpNorm gh (ENNReal.ofReal (6 / 5)) (MeasureTheory.volume.restrict (euclideanBall x₀ (ρ / 2))) ≤ ENNReal.ofReal C_H * ENNReal.ofReal (ρ ^ (-1 / 2)) * MeasureTheory.eLpNorm p (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall x₀ ρ))), MeasureTheory.eLpNorm gp (ENNReal.ofReal (6 / 5)) (MeasureTheory.volume.restrict (euclideanBall x₀ (ρ / 2))) ≤ ENNReal.ofReal C_CZ * MeasureTheory.eLpNorm G (ENNReal.ofReal (6 / 5)) MeasureTheory.volume + ENNReal.ofReal C_H * ENNReal.ofReal (ρ ^ (-1 / 2)) * MeasureTheory.eLpNorm p (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall x₀ ρ))