Rpow Squares

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

theorem CKN.Foundation.Euclidean.rpow_half_sq {κ : ℝ} (hκ : 0 < κ) : (κ ^ (1 / 2)) ^ 2 = κ

(κ^{1/2})² = κ for κ > 0.

theorem CKN.Foundation.Euclidean.rpow_neg_half_sq {κ : ℝ} (hκ : 0 < κ) : (κ ^ (-1 / 2)) ^ 2 = κ ^ (-1)

(κ^{-1/2})² = κ⁻¹ for κ > 0.

theorem CKN.Foundation.Euclidean.rpow_third_sq {κ : ℝ} (hκ : 0 < κ) : (κ ^ (1 / 3)) ^ 2 = κ ^ (2 / 3)

(κ^{1/3})² = κ^{2/3} for κ > 0.

theorem CKN.Foundation.Euclidean.rpow_half_sq_of_nonneg {x : ℝ} (hx : 0 ≤ x) : (x ^ (1 / 2)) ^ 2 = x

(x^{1/2})² = x for x ≥ 0.