Rounding Away from Zero

Away-from-zero rounding uses ceiling on nonnegative inputs and floor on negative inputs. Together with toward-zero rounding, it supplies the second endpoint decomposition for arbitrary valid integer rounding modes.

noncomputable def FloatLib.Floats.Formats.Flocq.awayRound (x : ℝ) : ℤ

Integer rounding away from zero.

theorem FloatLib.Floats.Formats.Flocq.awayRound_eq_floor {x : ℝ} (hx : x < 0) : awayRound x = floorRound x

Away-from-zero agrees with floor on negative inputs.

theorem FloatLib.Floats.Formats.Flocq.awayRound_eq_ceil {x : ℝ} (hx : 0 ≤ x) : awayRound x = ceilRound x

Away-from-zero agrees with ceiling on nonnegative inputs.

theorem FloatLib.Floats.Formats.Flocq.awayRound_eq_floor_of_nonpos {x : ℝ} (hx : x ≤ 0) : awayRound x = floorRound x

On nonpositive inputs, away-from-zero agrees with floor, including at zero.

instance FloatLib.Floats.Formats.Flocq.awayRoundValid : ValidRnd awayRound

Away-from-zero rounding is monotone and fixes integers.

theorem FloatLib.Floats.Formats.Flocq.valid_round_eq_trunc_or_away (rnd : ℝ → ℤ) [ValidRnd rnd] (x : ℝ) : rnd x = truncRound x ∨ rnd x = awayRound x

Arbitrary valid integer rounding chooses toward-zero or away-from-zero.

def FloatLib.Floats.Formats.Flocq.RoundAwayFromZeroPoint (F : ℝ → Prop) (x f : ℝ) : Prop

Upward rounding on nonnegative inputs and downward rounding on nonpositive inputs.

theorem FloatLib.Floats.Formats.Flocq.round_away_point {β : Numerics.Radix} {fexp : ℤ → ℤ} [ValidExp fexp] (x : ℝ) : RoundAwayFromZeroPoint (genericFormat β fexp) x (round awayRound x)

Generic away-from-zero rounding satisfies its semantic point specification.