Radix Magnitude

The magnitude of a nonzero real $x$ is the unique integer $e$ for which $\beta^{e-1}\le|x|<\beta^e$. These bounds are the basic bridge between logarithmic magnitude, canonical exponents, and generic-format rounding.

theorem FloatLib.Floats.Formats.Flocq.magnitude_eq_int_log_add_one (β : Numerics.Radix) (x : ℝ) (hx : x ≠ 0) : magnitude β x = Int.log β.base |x| + 1

Flocq magnitude is Mathlib's integer logarithm plus one away from zero.

theorem FloatLib.Floats.Formats.Flocq.magnitude_spec (β : Numerics.Radix) (x : ℝ) (hx : x ≠ 0) : bpow β (magnitude β x - 1) ≤ |x| ∧ |x| < bpow β (magnitude β x)

The logarithmic definition of magnitude satisfies the standard Flocq magnitude bounds.

theorem FloatLib.Floats.Formats.Flocq.bpow_magnitude_sub_one_le (β : Numerics.Radix) (x : ℝ) (hx : x ≠ 0) : bpow β (magnitude β x - 1) ≤ |x|

Lower magnitude bound for a nonzero real.

theorem FloatLib.Floats.Formats.Flocq.abs_lt_bpow_magnitude (β : Numerics.Radix) (x : ℝ) (hx : x ≠ 0) : |x| < bpow β (magnitude β x)

Strict upper magnitude bound for a nonzero real.

@[simp]

theorem FloatLib.Floats.Formats.Flocq.magnitude_bpow (β : Numerics.Radix) (e : ℤ) : magnitude β (bpow β e) = e + 1

The magnitude of $\beta^e$ is $e+1$.

@[simp]

theorem FloatLib.Floats.Formats.Flocq.bpow_le_bpow_iff (β : Numerics.Radix) (e₁ e₂ : ℤ) : bpow β e₁ ≤ bpow β e₂ ↔ e₁ ≤ e₂

Radix powers preserve and reflect exponent order.

@[simp]

theorem FloatLib.Floats.Formats.Flocq.bpow_lt_bpow_iff (β : Numerics.Radix) (e₁ e₂ : ℤ) : bpow β e₁ < bpow β e₂ ↔ e₁ < e₂

Radix powers preserve and reflect strict exponent order.

theorem FloatLib.Floats.Formats.Flocq.magnitude_eq_of_bpow_bounds (β : Numerics.Radix) (x : ℝ) (e : ℤ) (hx : x ≠ 0) (hlower : bpow β (e - 1) ≤ |x|) (hupper : |x| < bpow β e) : magnitude β x = e

Radix-power bounds uniquely determine magnitude.

theorem FloatLib.Floats.Formats.Flocq.magnitude_le_of_abs_lt_bpow (β : Numerics.Radix) (x : ℝ) (e : ℤ) (hx : x ≠ 0) (hupper : |x| < bpow β e) : magnitude β x ≤ e

Any strict radix-power upper bound is also an upper bound on magnitude.

theorem FloatLib.Floats.Formats.Flocq.magnitude_mono_pos (β : Numerics.Radix) {x y : ℝ} (hx : 0 < x) (hxy : x ≤ y) : magnitude β x ≤ magnitude β y

Magnitude is monotone on positive real inputs.

theorem FloatLib.Floats.Formats.Flocq.magnitude_mono_abs (β : Numerics.Radix) {x y : ℝ} (hx : x ≠ 0) (hxy : |x| ≤ |y|) : magnitude β x ≤ magnitude β y

Magnitude is monotone with respect to absolute value for nonzero inputs.

theorem FloatLib.Floats.Formats.Flocq.cexp_mono_abs (β : Numerics.Radix) {fexp : ℤ → ℤ} [ValidExp fexp] [MonotoneExp fexp] {x y : ℝ} (hx : x ≠ 0) (hxy : |x| ≤ |y|) : cexp β fexp x ≤ cexp β fexp y

A monotone exponent format preserves absolute-value order at canonical exponents of nonzero inputs.

theorem FloatLib.Floats.Formats.Flocq.magnitude_mul_le_add (β : Numerics.Radix) {x y : ℝ} (hx : x ≠ 0) (hy : y ≠ 0) : magnitude β (x * y) ≤ magnitude β x + magnitude β y

The magnitude of a nonzero product is at most the sum of operand magnitudes.

theorem FloatLib.Floats.Formats.Flocq.magnitude_mul_bpow (β : Numerics.Radix) (x : ℝ) (e : ℤ) (hx : x ≠ 0) : magnitude β (x * bpow β e) = magnitude β x + e

Multiplication by a radix power shifts magnitude by its exponent.

theorem FloatLib.Floats.Formats.Flocq.bpow_eq_natCast_of_nonneg (β : Numerics.Radix) (e : ℤ) (he : 0 ≤ e) : ∃ (n : ℕ), bpow β e = ↑n

A radix power with nonnegative exponent is the cast of a natural number.