Pk Bounds Unconditional Constants

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

Explicit constants used by the three unconditional pressure estimates.

noncomputable def CKN.pressureP234Constant : ℝ

Combined coefficient for the three velocity-tensor pressure corrections.

Equations

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

noncomputable def CKN.pressureP56Constant : ℝ

Combined coefficient for the two pressure-cutoff corrections.

Equations

• CKN.pressureP56Constant = 2 * ((Real.pi * 4 / 3) ^ (1 / 3) * (18 * CKN.cutoffSecondDerivativeConstant + 240 * CKN.cutoffGradientConstant)) * (4 * Real.pi / 3) ^ (2 / 3)

noncomputable def CKN.pressureP12Constant : ℝ

Common coefficient dominating the velocity and pressure cutoff contributions.

Equations

• CKN.pressureP12Constant = max CKN.pressureP234Constant CKN.pressureP56Constant

noncomputable def CKN.pressureP13Constant (q : ℝ) : ℝ

Exponent-dependent coefficient for the force-cutoff contribution.

Equations

• CKN.pressureP13Constant q = 6 * CKN.cutoffGradientConstant * (4 * Real.pi / 3) ^ (1 - 1 / q) * (4 * Real.pi / 3) ^ (2 / 3)

theorem CKN.pressure_cutoff_constants_nonneg {x₀ : Foundation.Parabolic.Vec3} {ρ : ℝ} (hρ : 0 < ρ) : 0 ≤ cutoffGradientConstant ∧ 0 ≤ cutoffSecondDerivativeConstant

theorem CKN.pressureP234Constant_nonneg {x₀ : Foundation.Parabolic.Vec3} {ρ : ℝ} (hρ : 0 < ρ) : 0 ≤ pressureP234Constant

theorem CKN.pressureP56Constant_nonneg {x₀ : Foundation.Parabolic.Vec3} {ρ : ℝ} (hρ : 0 < ρ) : 0 ≤ pressureP56Constant

theorem CKN.pressureP13Constant_nonneg {x₀ : Foundation.Parabolic.Vec3} {ρ q : ℝ} (hρ : 0 < ρ) : 0 ≤ pressureP13Constant q

theorem CKN.pressure_volume_ball {x₀ : Foundation.Parabolic.Vec3} {r : ℝ} (hr : 0 < r) : MeasureTheory.volume (Foundation.Parabolic.vec3Ball x₀ r) = ENNReal.ofReal (4 * Real.pi / 3 * r ^ 3)

theorem CKN.pressure_rpow_three_halves {ρ : ℝ} (hρ : 0 < ρ) : ρ ^ (3 / 2) = ρ * √ρ

theorem CKN.pressure_rpow_div {r ρ a : ℝ} (hr : 0 < r) (hρ : 0 < ρ) : (r / ρ) ^ a = r ^ a * ρ ^ (-a)