Double Rounding #
Directed rounding through a finer intermediate format gives the same answer as direct rounding to the coarser format. The order-theoretic proof only needs inclusion of representable values, so it applies beyond the standard FIX, FLX, and FLT families.
theorem
TorchLean.Floats.neuralRoundDownPoint_double
{fine coarse : ℝ → Prop}
{x fineValue coarseValue : ℝ}
(hsubset : ∀ (z : ℝ), coarse z → fine z)
(hf : NeuralRoundDownPoint fine x fineValue)
(hc : NeuralRoundDownPoint coarse x coarseValue)
:
NeuralRoundDownPoint coarse fineValue coarseValue
Downward rounding through a containing format collapses to direct downward rounding.
theorem
TorchLean.Floats.neuralRoundUpPoint_double
{fine coarse : ℝ → Prop}
{x fineValue coarseValue : ℝ}
(hsubset : ∀ (z : ℝ), coarse z → fine z)
(hf : NeuralRoundUpPoint fine x fineValue)
(hc : NeuralRoundUpPoint coarse x coarseValue)
:
NeuralRoundUpPoint coarse fineValue coarseValue
Upward rounding through a containing format collapses to direct upward rounding.
theorem
TorchLean.Floats.neural_generic_format_FLX_mono
{β : NeuralRadix}
{coarsePrec finePrec : ℤ}
(hcoarse : 0 < coarsePrec)
(hfine : 0 < finePrec)
(hprec : coarsePrec ≤ finePrec)
{x : ℝ}
(hx : neuralGenericFormat β (FLXExp coarsePrec) x)
:
neuralGenericFormat β (FLXExp finePrec) x
Increasing FLX precision preserves every exactly representable value.
theorem
TorchLean.Floats.neuralRound_floor_double_FLX
{β : NeuralRadix}
{coarsePrec finePrec : ℤ}
(hcoarse : 0 < coarsePrec)
(hfine : 0 < finePrec)
(hprec : coarsePrec ≤ finePrec)
(x : ℝ)
:
Downward FLX double rounding equals direct rounding to the coarser precision.
theorem
TorchLean.Floats.neuralRound_ceil_double_FLX
{β : NeuralRadix}
{coarsePrec finePrec : ℤ}
(hcoarse : 0 < coarsePrec)
(hfine : 0 < finePrec)
(hprec : coarsePrec ≤ finePrec)
(x : ℝ)
:
Upward FLX double rounding equals direct rounding to the coarser precision.