Pressure Gradient Symmetric Cell #
Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.
Pressure Gradient Morrey Bridge #
Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.
theorem
CKN.Core.Step4.pressure_gradient_morreyVecMem_of_cell_bounds_real
{S : Set Foundation.Parabolic.ParabolicPoint}
{κ C : ℝ}
{Dp : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
(hκ : 6 / 5 ≤ κ)
(hC : ENNReal.ofReal C < ⊤)
(hcell :
∀ (i : Fin 3) (z : Foundation.Parabolic.ParabolicPoint) (r : { r : ℝ // 0 < r }),
Foundation.Parabolic.Morrey.morreyCell (6 / 5) κ
(S.indicator fun (w : Foundation.Parabolic.ParabolicPoint) => Dp w i) z ↑r ≤ ENNReal.ofReal C)
:
morreyVecMem (6 / 5) κ S Dp
The same bridge with the scalar exponent written as an explicit real
number; this is convenient when the exponent is
min ((1 / τ + 8 / 25)⁻¹) q.
The symmetric carrier for G. The slice producer is deliberately kept at
the exact inner-ball interface consumed by exists_spacetime_weak_gradient_of_slices.
This is the space-time form of the paper's display (3.5).
Existence interface for pressure-gradient slices on symmetric interior parabolic balls.
Equations
- One or more equations did not get rendered due to their size.