TorchLean API

Docs HomeGuideExamplesGraphs

NN.Floats.Interval.IEEEExec32MinMaxSoundness

min4/max4 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) :
(min4 a b c d).toReal = min (min a.toReal b.toReal) (min c.toReal d.toReal)

Real semantics of Interval32.min4 in the finite regime.

If all four arguments are finite, then toReal (min4 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) :
(max4 a b c d).toReal = max (max a.toReal b.toReal) (max c.toReal d.toReal)

Real semantics of Interval32.max4 in the finite regime.

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