Spatial Gradient Sq

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

def CKN.spatialGradientSq (_u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3) (z : Foundation.Parabolic.ParabolicPoint) : ℝ

The squared spatial-gradient density used by paper label def:sws.

Equations

• CKN.spatialGradientSq _u Du z = ∑ i : Fin 3, ∑ j : Fin 3, Du z i j ^ 2