TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

NN.Proofs.RuntimeApprox.IEEE32.MinMaxTotal

Total optional observations of binary32 minimum and maximum #

Finite operands use the real minimum and maximum contracts. NaNs propagate without a real observation, while positive infinity is neutral for minimum and negative infinity is neutral for maximum. The exceptional cases follow FloatLib's NaN selection and infinity comparison directly.

source
theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal?_minimum_eq_match_total (x y : FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) toReal?_minimum_eq_match_total._proof_3 toReal?_minimum_eq_match_total._proof_4 toReal?_minimum_eq_match_total._proof_5 toReal?_minimum_eq_match_total._proof_6) :
toReal? (x ⊓ y) = match toReal? x, toReal? y with | some rx, some ry => some (min rx ry) | some rx, none => if (FloatLib.Floats.ExecFloat.Binary.isInfinite y && !FloatLib.Floats.ExecFloat.Binary.signBit y) = true then some rx else none | none, some ry => if (FloatLib.Floats.ExecFloat.Binary.isInfinite x && !FloatLib.Floats.ExecFloat.Binary.signBit x) = true then some ry else none | none, none => none

Total characterization of toReal? (minimum x y) via toReal? x and toReal? y.

This lemma covers the cases where one side is +∞ (which acts as a neutral element for min) and the cases where toReal? is none because of NaN.

source
theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal?_maximum_eq_match_total (x y : FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) toReal?_minimum_eq_match_total._proof_3 toReal?_minimum_eq_match_total._proof_4 toReal?_minimum_eq_match_total._proof_5 toReal?_minimum_eq_match_total._proof_6) :
toReal? (x ⊔ y) = match toReal? x, toReal? y with | some rx, some ry => some (max rx ry) | some rx, none => if (FloatLib.Floats.ExecFloat.Binary.isInfinite y && FloatLib.Floats.ExecFloat.Binary.signBit y) = true then some rx else none | none, some ry => if (FloatLib.Floats.ExecFloat.Binary.isInfinite x && FloatLib.Floats.ExecFloat.Binary.signBit x) = true then some ry else none | none, none => none

Total characterization of toReal? (maximum x y) via toReal? x and toReal? y.

This lemma covers the cases where one side is -∞ (which acts as a neutral element for max) and the cases where toReal? is none because of NaN.