TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

NN.Floats.NeuralFloat.Rounding.Generic

Rounding Into A Generic Format #

This file develops the converse of neural_round_preserves_generic: rounding an arbitrary real produces a value in the selected generic format. The proof follows the small/large magnitude split used by Flocq rather than assuming the conclusion as part of the rounding definition.

source
theorem TorchLean.Floats.neuralValidExp_small {fexp : ℤ → ℤ} [NeuralValidExp fexp] {e : ℤ} (h : e ≤ fexp e) :
fexp (fexp e + 1) ≤ fexp e

The Valid_exp consequence used when the input magnitude is below the selected exponent.

source
theorem TorchLean.Floats.neuralValidExp_large {fexp : ℤ → ℤ} [NeuralValidExp fexp] {e : ℤ} (h : fexp e < e) :
fexp (e + 1) ≤ e

The Valid_exp consequence used when the selected exponent is below the input magnitude.

source
theorem TorchLean.Floats.neural_round_pos_small_cases {β : NeuralRadix} {fexp : ℤ → ℤ} [NeuralValidExp fexp] (rnd : ℝ → ℤ) [NeuralValidRnd rnd] (x : ℝ) (hx : 0 < x) (hsmall : neuralMagnitude β x ≤ fexp (neuralMagnitude β x)) :
neuralRound rnd x = 0 ∨ neuralRound rnd x = neuralBpow β (fexp (neuralMagnitude β x))

Positive inputs in the small-magnitude regime round either to zero or to one radix power.

source
theorem TorchLean.Floats.neural_generic_format_round_pos_small {β : NeuralRadix} {fexp : ℤ → ℤ} [NeuralValidExp fexp] (rnd : ℝ → ℤ) [NeuralValidRnd rnd] (x : ℝ) (hx : 0 < x) (hsmall : neuralMagnitude β x ≤ fexp (neuralMagnitude β x)) :
neuralGenericFormat β fexp (neuralRound rnd x)

Rounding in the small-magnitude regime produces a generic-format value.

source
theorem TorchLean.Floats.neural_round_pos_large_bounds_and_generic {β : NeuralRadix} {fexp : ℤ → ℤ} [NeuralValidExp fexp] (rnd : ℝ → ℤ) [NeuralValidRnd rnd] (x : ℝ) (hx : 0 < x) (hlarge : fexp (neuralMagnitude β x) < neuralMagnitude β x) :
(neuralBpow β (neuralMagnitude β x - 1) ≤ neuralRound rnd x ∧ neuralRound rnd x ≤ neuralBpow β (neuralMagnitude β x)) ∧ neuralGenericFormat β fexp (neuralRound rnd x)

In the large-magnitude regime, rounding stays inside the input magnitude bin and produces a generic-format value.

source
theorem TorchLean.Floats.neural_generic_format_round_pos_large {β : NeuralRadix} {fexp : ℤ → ℤ} [NeuralValidExp fexp] (rnd : ℝ → ℤ) [NeuralValidRnd rnd] (x : ℝ) (hx : 0 < x) (hlarge : fexp (neuralMagnitude β x) < neuralMagnitude β x) :
neuralGenericFormat β fexp (neuralRound rnd x)

Rounding in the large-magnitude regime produces a generic-format value.

source
theorem TorchLean.Floats.neural_generic_format_round_pos {β : NeuralRadix} {fexp : ℤ → ℤ} [NeuralValidExp fexp] (rnd : ℝ → ℤ) [NeuralValidRnd rnd] (x : ℝ) (hx : 0 < x) :
neuralGenericFormat β fexp (neuralRound rnd x)

Every positive real rounds into the selected generic format.

source
def TorchLean.Floats.neuralNegRound (rnd : ℝ → ℤ) :
ℝ → ℤ

Conjugate a rounding rule by negation.

Instances For
    source
    instance TorchLean.Floats.neuralNegRoundValid (rnd : ℝ → ℤ) [NeuralValidRnd rnd] :
    NeuralValidRnd (neuralNegRound rnd)
    source
    theorem TorchLean.Floats.neuralRound_neg {β : NeuralRadix} {fexp : ℤ → ℤ} [NeuralValidExp fexp] (rnd : ℝ → ℤ) [NeuralValidRnd rnd] (x : ℝ) :
    neuralRound rnd (-x) = -neuralRound (neuralNegRound rnd) x

    Rounding a negated input is negated rounding with the conjugate integer rule.

    source
    theorem TorchLean.Floats.neural_generic_format_round {β : NeuralRadix} {fexp : ℤ → ℤ} [NeuralValidExp fexp] (rnd : ℝ → ℤ) [NeuralValidRnd rnd] (x : ℝ) :
    neuralGenericFormat β fexp (neuralRound rnd x)

    Rounding any real produces a value in the selected generic format.