TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

NN.Floats.Interval.IEEEExec32MinMaxSoundness

minOfFour/maxOfFour real semantics (finite regime) #

NN/Floats/Interval/IEEEExec32.lean exposes helper combinators:

used to implement the classical 4-corner multiplication enclosure rule.

This file provides small lemmas that compute the toReal semantics of these helpers when all arguments are finite.

These lemmas are intended as building blocks for a larger Interval32.mul soundness theorem.

source
theorem TorchLean.Floats.IEEE754.IEEE32Exec.Interval32.toReal_min4_eq_min_of_isFinite (a b c d : IEEE32Exec) (ha : a.isFinite = true) (hb : b.isFinite = true) (hc : c.isFinite = true) (hd : d.isFinite = true) :
(minOfFour a b c d).toReal = min (min a.toReal b.toReal) (min c.toReal d.toReal)

Real semantics of Interval32.minOfFour in the finite regime.

If all four arguments are finite, then toReal (minOfFour a b c d) is the corresponding nested min of the four real values.

source
theorem TorchLean.Floats.IEEE754.IEEE32Exec.Interval32.toReal_max4_eq_max_of_isFinite (a b c d : IEEE32Exec) (ha : a.isFinite = true) (hb : b.isFinite = true) (hc : c.isFinite = true) (hd : d.isFinite = true) :
(maxOfFour a b c d).toReal = max (max a.toReal b.toReal) (max c.toReal d.toReal)

Real semantics of Interval32.maxOfFour in the finite regime.

If all four arguments are finite, then toReal (maxOfFour a b c d) is the corresponding nested max of the four real values.