Nonnegative real powers with nonnegative rational exponents

Writing a nonnegative rational q as the reduced fraction q.num / q.den, the real power x ^ (1 / q) of x : ℝ≥0 is (x ^ q.den) ^ (1 / q.num). For q ≠ 0, so that q.num > 0, this turns an inequality against x ^ (1 / q) into one between natural-number powers, via NNReal.rpow_inv_le_iff and NNReal.le_rpow_inv_iff.

Main results

• NNReal.rpow_inv_nnratCast: x ^ (1 / q) = (x ^ q.den) ^ (1 / q.num).
• NNReal.rpow_inv_nnratCast_pow_num: for q ≠ 0, (x ^ (1 / q)) ^ q.num = x ^ q.den.

theorem NNReal.rpow_inv_nnratCast (x : NNReal) (q : ℚ≥0) : x ^ (↑q)⁻¹ = (x ^ q.den) ^ (↑q.num)⁻¹

Writing q = a / b in lowest terms, x ^ (1 / q) = (x ^ b) ^ (1 / a).

theorem NNReal.rpow_inv_nnratCast_pow_num (x : NNReal) {q : ℚ≥0} (hq : q ≠ 0) : (x ^ (↑q)⁻¹) ^ q.num = x ^ q.den

Writing q = a / b ≠ 0 in lowest terms, ρ = x ^ (1 / q) solves ρ ^ a = x ^ b.