Real correctness of rational-power comparisons

Raising a nonnegative real value to a positive integer power preserves strict and non-strict order. Clearing the rational exponent denominator therefore turns comparison with an algebraic real power into an exact rational computation, including equality cases.

theorem FloatLib.Numerics.RationalPower.rpow_pow_den (base exponent : ℚ) (hbase : 0 < base) : (↑base ^ ↑exponent) ^ exponent.den = ↑(base ^ exponent.num)

Clearing the exponent denominator gives an exact rational integer power.

theorem FloatLib.Numerics.RationalPower.pow_num_lt_pow_den_iff (base exponent target : ℚ) (hbase : 0 < base) (htarget : 0 ≤ target) : base ^ exponent.num < target ^ exponent.den ↔ ↑base ^ ↑exponent < ↑target

The executable strict comparison has the usual real-power meaning.

theorem FloatLib.Numerics.RationalPower.pow_den_lt_pow_num_iff (base exponent target : ℚ) (hbase : 0 < base) (htarget : 0 ≤ target) : target ^ exponent.den < base ^ exponent.num ↔ ↑target < ↑base ^ ↑exponent

Reversing the executable strict comparison reverses the real-power comparison.

theorem FloatLib.Numerics.RationalPower.pow_num_le_pow_den_iff (base exponent target : ℚ) (hbase : 0 < base) (htarget : 0 ≤ target) : base ^ exponent.num ≤ target ^ exponent.den ↔ ↑base ^ ↑exponent ≤ ↑target

The non-strict executable comparison also handles exact equality.

theorem FloatLib.Numerics.RationalPower.compare_eq_real (base exponent target : ℚ) (hbase : 0 < base) (htarget : 0 ≤ target) : compare base exponent target = cmp (↑base ^ ↑exponent) ↑target

The rational comparator returns exactly the ordering of the real power and target.