Norm Triangle

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

theorem CKN.vecEuclideanNorm_eq_norm_toLp {d : ℕ} (x : Vec d) : vecEuclideanNorm x = ‖WithLp.toLp 2 x‖

The Euclidean norm on native coordinate vectors coincides with the L² norm of WithLp.toLp 2 x.

theorem CKN.vecEuclideanNorm_add_le {d : ℕ} (x y : Vec d) : vecEuclideanNorm (x + y) ≤ vecEuclideanNorm x + vecEuclideanNorm y

The triangle inequality for the Euclidean norm on native coordinate vectors.