Pk Bounds Unconditional Scale #
Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.
The three scale calculations used when the fixed-time pressure estimates are assembled over a smaller parabolic cylinder.
theorem
CKN.pressureP234_scale
{r ρ α β A K : ℝ}
{X : ENNReal}
{V : Set Foundation.Parabolic.Vec3}
(hr : 0 < r)
(hρ : 0 < ρ)
(hα : 0 ≤ α)
(hA : 0 ≤ A)
(hKeq : K = A * α / ρ ^ (3 / 2))
(hX : X ^ (2 / 3) ≤ ENNReal.ofReal (r ^ (1 / 3)) * ENNReal.ofReal (√ρ * β))
(hV : MeasureTheory.volume V = ENNReal.ofReal (4 * Real.pi / 3 * r ^ 3))
:
theorem
CKN.pressureP234_scale_cylinder
{r ρ α β A K : ℝ}
{X : ENNReal}
{V : Set Foundation.Parabolic.Vec3}
(hr : 0 < r)
(hρ : 0 < ρ)
(hα : 0 ≤ α)
(hA : 0 ≤ A)
(hKeq : K = A * α / ρ ^ (3 / 2))
(hX : X ^ (2 / 3) ≤ ENNReal.ofReal (r ^ (1 / 3)) * ENNReal.ofReal (√ρ * β))
(hV : MeasureTheory.volume V = ENNReal.ofReal (4 * Real.pi / 3 * r ^ 3))
:
theorem
CKN.pressureP56_scale
{r ρ δ A K : ℝ}
{X : ENNReal}
{V : Set Foundation.Parabolic.Vec3}
(hr : 0 < r)
(hρ : 0 < ρ)
(hA : 0 ≤ A)
(hKeq : K = A / ρ ^ 2)
(hX : X ^ (2 / 3) ≤ ENNReal.ofReal (ρ ^ (4 / 3)) * ENNReal.ofReal (δ ^ 2))
(hV : MeasureTheory.volume V = ENNReal.ofReal (4 * Real.pi / 3 * r ^ 3))
:
theorem
CKN.pressureP56_scale_cylinder
{r ρ δ A K : ℝ}
{X : ENNReal}
{V : Set Foundation.Parabolic.Vec3}
(hr : 0 < r)
(hρ : 0 < ρ)
(hA : 0 ≤ A)
(hKeq : K = A / ρ ^ 2)
(hX : X ^ (2 / 3) ≤ ENNReal.ofReal (ρ ^ (4 / 3)) * ENNReal.ofReal (δ ^ 2))
(hV : MeasureTheory.volume V = ENNReal.ofReal (4 * Real.pi / 3 * r ^ 3))
:
theorem
CKN.pressureP8_scale
{q r ρ lam A K : ℝ}
{X : ENNReal}
{V : Set Foundation.Parabolic.Vec3}
(hr : 0 < r)
(hρ : 0 < ρ)
(hA : 0 ≤ A)
(hKeq : K = A * ρ ^ (1 - 3 / q))
(hX : X ^ (2 / 3) ≤ ENNReal.ofReal (r ^ (2 * (2 / 3 - 1 / q))) * ENNReal.ofReal (ρ ^ (5 / q - 3) * lam))
(hV : MeasureTheory.volume V = ENNReal.ofReal (4 * Real.pi / 3 * r ^ 3))
: