Logarithmic Properties of Scientific Notation for Floating-Point

This module proves facts in ℚ about the sizes and properties of values like x * b^e where x is in [1, b) and e is an integer.

theorem le_log_of_ge_1 {b : ℕ} {e : ℤ} (h : 1 < b) {x : ℚ} (h' : 1 ≤ x) : e ≤ Int.log b (x * ↑b ^ e)

For 1 ≤ x, (x * b^e) has an exponent at least e.

theorem log_one_to_two_eq {b : ℕ} {e : ℤ} (h : 1 < b) {x : ℚ} (h' : 1 ≤ x) (h'' : x < ↑b) : Int.log b (x * ↑b ^ e) = e

When 1 ≤ x < 2, x*b^e has exponent exactly e.

theorem log_zero_to_one_lt (x : ℚ) (e : ℤ) (h : 0 < x) (h' : x < 1) : Int.log 2 |x * 2 ^ e| < e

When 0 < x < 1, then x*2^e has exponent < e.

theorem mantissa_ge_one {C : FloatCfg} {m : ℕ} : 1 ≤ ↑m / ↑C.prec + 1

theorem mantissa_lt_two {C : FloatCfg} {m : ℕ} (h : m < C.prec) : ↑m / ↑C.prec + 1 < 2

theorem q_exp_eq_exp {C : FloatCfg} {e : ℤ} {m : ℕ} (h : m < C.prec) : Int.log 2 |(↑m / ↑C.prec + 1) * 2 ^ e| = e

theorem q_mantissa_eq_mantissa {C : FloatCfg} {e : ℤ} {m : ℕ} (h : m < C.prec) : |(↑m / ↑C.prec + 1) * 2 ^ e| * (2 ^ Int.log 2 |(↑m / ↑C.prec + 1) * 2 ^ e|)⁻¹ = ↑m / ↑C.prec + 1

theorem mantissa_size_aux (q : ℚ) (h : q ≠ 0) : 1 ≤ |q| * (2 ^ Int.log 2 |q|)⁻¹ ∧ |q| * (2 ^ Int.log 2 |q|)⁻¹ < 2

theorem small_floor_aux {q : ℚ} {n : ℕ} (h : q < 1) (h' : 0 ≤ q) (n_pos : 0 < n) : ⌊q * ↑n⌋.natAbs < n

theorem small_ceil {q : ℚ} {n : ℕ} (h : q ≤ 1) (h' : 0 ≤ q) (n_nonneg : 0 ≤ n) : ⌈q * ↑n⌉.natAbs ≤ n

theorem mantissa_nonneg (C : FloatCfg) (q : ℚ) (q_nezero : q ≠ 0) : 0 ≤ (|q| * (2 ^ Int.log 2 |q|)⁻¹ - 1) * ↑C.prec

theorem casesQPlane (P : ℚ → ℚ → Prop) (h1 : ∀ q1 > 0, ∀ q2 > 0, P q1 q2) (h2 : ∀ q1 < 0, ∀ q2 > 0, P q1 q2) (h3 : ∀ q1 > 0, ∀ q2 < 0, P q1 q2) (h4 : ∀ q1 < 0, ∀ q2 < 0, P (-q1) (-q2) → P q2 q1) (q1 q2 : ℚ) (q1_nezero : q1 ≠ 0) (q2_nezero : q2 ≠ 0) : P q1 q2