Vec3 Norm

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

theorem CKN.Foundation.Parabolic.vec3EuclideanNorm_add_le (v w : Vec3) : vec3EuclideanNorm (v + w) ≤ vec3EuclideanNorm v + vec3EuclideanNorm w

The Euclidean norm on Vec3 satisfies the triangle inequality.

theorem CKN.Foundation.Parabolic.vec3EuclideanNorm_neg (v : Vec3) : vec3EuclideanNorm (-v) = vec3EuclideanNorm v

The Euclidean norm on Vec3 is invariant under negation.

theorem CKN.Foundation.Parabolic.vec3EuclideanNorm_sub_le (v w : Vec3) : vec3EuclideanNorm (v - w) ≤ vec3EuclideanNorm v + vec3EuclideanNorm w

The Euclidean norm on Vec3 satisfies the reverse triangle inequality.

theorem CKN.Foundation.Parabolic.abs_apply_le_vec3EuclideanNorm (v : Vec3) (i : Fin 3) : |v i| ≤ vec3EuclideanNorm v

Each component of a vector in Vec3 is bounded in absolute value by the Euclidean norm.

theorem CKN.Foundation.Parabolic.norm_le_vec3EuclideanNorm (v : Vec3) : ‖v‖ ≤ vec3EuclideanNorm v

The sup norm on Vec3 (the default ‖·‖ for Fin 3 → ℝ) is bounded by the Euclidean norm.

theorem CKN.Foundation.Parabolic.vec3EuclideanNorm_le_sqrt_three_mul_norm (v : Vec3) : vec3EuclideanNorm v ≤ √3 * ‖v‖

The Euclidean norm on Vec3 is bounded by √3 times the sup norm.

theorem CKN.Foundation.Parabolic.vec3EuclideanNorm_le_sum_abs (v : Vec3) : vec3EuclideanNorm v ≤ ∑ i : Fin 3, |v i|

The Euclidean norm on Vec3 is bounded by the sum of absolute values of its components.

theorem CKN.Foundation.Parabolic.continuous_vec3EuclideanNorm : Continuous vec3EuclideanNorm

The Euclidean norm on Vec3 is continuous with respect to the product topology.