Real semantics of exact elementary comparisons

These are total comparisons with the mathematical exponential and natural logarithm. They include equality: exp 0 = 1 and log 1 = 0 are handled exactly before refinement.

theorem FloatLib.Numerics.ElementaryComparison.compareLog_eq_real (argument boundary : ℚ) (hpositive : 0 < argument) : compareLog argument boundary hpositive = cmp (Real.log ↑argument) ↑boundary

The executable logarithm comparison agrees with the real ordering.

theorem FloatLib.Numerics.ElementaryComparison.compareExp_eq_real (argument boundary : ℚ) : compareExp argument boundary = cmp (Real.exp ↑argument) ↑boundary

The executable exponential comparison agrees with the real ordering.

theorem FloatLib.Numerics.ElementaryComparison.prepareLog_eq_real (argument : ℚ) (levels : ℕ) (hpositive : 0 < argument) (boundary : ℚ) : (prepareLog argument levels hpositive).compare boundary = cmp (Real.log ↑argument) ↑boundary

Sharing logarithm enclosures preserves the exact real comparison.

theorem FloatLib.Numerics.ElementaryComparison.prepareExp_eq_real (argument : ℚ) (levels : ℕ) (boundary : ℚ) : (prepareExp argument levels).compare boundary = cmp (Real.exp ↑argument) ↑boundary

Both prepared exponential algorithms implement the same exact real comparison.