Rounding an integer-degree root on the coefficient grid

The integer root of the rational floor brackets the nonnegative real root. Exact powers compare that root with integer coefficients and their midpoints. The degree is any positive natural number.

theorem FloatLib.Floats.Formats.DecimalInterchange.rootFloor_eq_nthRoot (degree : ℕ) (radicand : ℚ) : rootFloor degree radicand = degree.nthRoot ⌊radicand⌋₊

noncomputable def FloatLib.Floats.Formats.DecimalInterchange.realRoot (degree : ℕ) (x : ℝ) : ℝ

The nonnegative real root used in the numerical specifications.

theorem FloatLib.Floats.Formats.DecimalInterchange.realRoot_nonneg (degree : ℕ) {x : ℝ} (hx : 0 ≤ x) : 0 ≤ realRoot degree x

theorem FloatLib.Floats.Formats.DecimalInterchange.realRoot_pow {degree : ℕ} (hn : degree ≠ 0) {x : ℝ} (hx : 0 ≤ x) : realRoot degree x ^ degree = x

theorem FloatLib.Floats.Formats.DecimalInterchange.le_realRoot_iff {degree : ℕ} (hn : degree ≠ 0) {x a : ℝ} (hx : 0 ≤ x) (ha : 0 ≤ a) : a ≤ realRoot degree x ↔ a ^ degree ≤ x

theorem FloatLib.Floats.Formats.DecimalInterchange.realRoot_le_iff {degree : ℕ} (hn : degree ≠ 0) {x a : ℝ} (hx : 0 ≤ x) (ha : 0 ≤ a) : realRoot degree x ≤ a ↔ x ≤ a ^ degree

theorem FloatLib.Floats.Formats.DecimalInterchange.realRoot_lt_iff {degree : ℕ} (hn : degree ≠ 0) {x a : ℝ} (hx : 0 ≤ x) (ha : 0 ≤ a) : realRoot degree x < a ↔ x < a ^ degree

theorem FloatLib.Floats.Formats.DecimalInterchange.rootFloor_pow_le {degree : ℕ} (hn : degree ≠ 0) {x : ℚ} (hx : 0 ≤ x) : ↑(rootFloor degree x) ^ degree ≤ x

theorem FloatLib.Floats.Formats.DecimalInterchange.lt_rootFloor_succ_pow {degree : ℕ} (hn : degree ≠ 0) {x : ℚ} (hx : 0 ≤ x) : x < (↑(rootFloor degree x) + 1) ^ degree

theorem FloatLib.Floats.Formats.DecimalInterchange.rootFloor_le_realRoot {degree : ℕ} (hn : degree ≠ 0) {x : ℚ} (hx : 0 ≤ x) : ↑(rootFloor degree x) ≤ realRoot degree ↑x

theorem FloatLib.Floats.Formats.DecimalInterchange.realRoot_lt_rootFloor_succ {degree : ℕ} (hn : degree ≠ 0) {x : ℚ} (hx : 0 ≤ x) : realRoot degree ↑x < ↑(rootFloor degree x) + 1

theorem FloatLib.Floats.Formats.DecimalInterchange.RoundingMode.rootRound_eq_floor_or_succ (mode : RoundingMode) (s : Bool) (degree : ℕ) (x : ℚ) : mode.rootRound s degree x = rootFloor degree x ∨ mode.rootRound s degree x = rootFloor degree x + 1

theorem FloatLib.Floats.Formats.DecimalInterchange.RoundingMode.rootRound_le_floor_add_one (mode : RoundingMode) (s : Bool) (degree : ℕ) (x : ℚ) : mode.rootRound s degree x ≤ rootFloor degree x + 1

theorem FloatLib.Floats.Formats.DecimalInterchange.RoundingMode.rootRound_nat_pow (mode : RoundingMode) (s : Bool) {degree : ℕ} (hn : degree ≠ 0) (k : ℕ) : mode.rootRound s degree (↑k ^ degree) = k

Exact integer roots stay exact in every mode, with either output sign.

theorem FloatLib.Floats.Formats.DecimalInterchange.rootFloor_midpoint_pow {degree : ℕ} (hn : degree ≠ 0) (k : ℕ) : rootFloor degree ((↑k + 1 / 2) ^ degree) = k

theorem FloatLib.Floats.Formats.DecimalInterchange.rootRound_nearestEven_midpoint (s : Bool) {degree : ℕ} (hn : degree ≠ 0) (k : ℕ) : RoundingMode.nearestEven.rootRound s degree ((↑k + 1 / 2) ^ degree) = if k % 2 = 1 then k + 1 else k

theorem FloatLib.Floats.Formats.DecimalInterchange.rootRound_nearestAway_midpoint (s : Bool) {degree : ℕ} (hn : degree ≠ 0) (k : ℕ) : RoundingMode.nearestAway.rootRound s degree ((↑k + 1 / 2) ^ degree) = k + 1

theorem FloatLib.Floats.Formats.DecimalInterchange.rootRound_error_lt_one (mode : RoundingMode) (s : Bool) {degree : ℕ} (hn : degree ≠ 0) {x : ℚ} (hx : 0 ≤ x) : |↑(mode.rootRound s degree x) - realRoot degree ↑x| < 1

theorem FloatLib.Floats.Formats.DecimalInterchange.rootRound_error_le_half (mode : RoundingMode) (s : Bool) (hm : mode = RoundingMode.nearestEven ∨ mode = RoundingMode.nearestAway) {degree : ℕ} (hn : degree ≠ 0) {x : ℚ} (hx : 0 ≤ x) : |↑(mode.rootRound s degree x) - realRoot degree ↑x| ≤ 1 / 2

Exact power comparisons imply the nearest-mode half-grid error bound.

theorem FloatLib.Floats.Formats.DecimalInterchange.rootRound_towardZero_le (s : Bool) {degree : ℕ} (hn : degree ≠ 0) {x : ℚ} (hx : 0 ≤ x) : ↑(RoundingMode.towardZero.rootRound s degree x) ≤ realRoot degree ↑x

theorem FloatLib.Floats.Formats.DecimalInterchange.rootRound_directed_down_le (s : Bool) {degree : ℕ} (hn : degree ≠ 0) {x : ℚ} (hx : 0 ≤ x) : ↑((if s = true then RoundingMode.towardPositive else RoundingMode.towardNegative).rootRound s degree x) ≤ realRoot degree ↑x

theorem FloatLib.Floats.Formats.DecimalInterchange.le_rootRound_directed_up (s : Bool) {degree : ℕ} (hn : degree ≠ 0) {x : ℚ} (hx : 0 ≤ x) : realRoot degree ↑x ≤ ↑((if s = true then RoundingMode.towardNegative else RoundingMode.towardPositive).rootRound s degree x)