Beta #
Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.
noncomputable def
CKN.beta
(u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3)
(Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3)
(z : Foundation.Parabolic.ParabolicPoint)
(r : ℝ)
:
The gradient quantity β from the manuscript, eq:alpha-beta; Du is the explicit gradient
datum.
Equations
- One or more equations did not get rendered due to their size.