TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.BinaryInterchange.IntervalSemantics.Activations

Activation enclosures for executable binary intervals #

ReLU, absolute value, and square root have enclosure and interval-validity theorems with operation-specific hypotheses. The executable definitions live in Interval.Activations; shared endpoint order and negation facts come from IntervalSemantics.Arithmetic.

ReLU and absolute value work for every descriptor and accept ordered non-NaN endpoints, including infinities from an earlier operation. Their finite-input theorems specialize the same proofs. Square root uses directed IEEE rounding and requires finite valid input bounds with a nonnegative lower endpoint. These differences appear in the theorem statements rather than in a second interval carrier or an implicit execution mode.

ReLU #

source
theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Interval.relu_sound_extended {fmt : FloatFormat} (A : Interval fmt) (hA : A.ValidExtended) {x : ℝ} (hx : A.ERealMem ↑x) :
A.relu.ERealMem ↑(max x 0)

The ReLU interval encloses each member's ReLU, including with infinite endpoints.

source
theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Interval.relu_validExtended {fmt : FloatFormat} (A : Interval fmt) (hA : A.ValidExtended) :
A.relu.ValidExtended

ReLU preserves ordered, non-NaN endpoints in every format.

source
theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Interval.relu_sound {fmt : FloatFormat} (A : Interval fmt) (hA : A.Valid) {x : ℝ} (hx : A.RealMem x) :
A.relu.ERealMem ↑(max x 0)

Executable interval ReLU encloses the ReLU of every represented real value.

Absolute value #

source
theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Interval.abs_sound_extended {fmt : FloatFormat} (A : Interval fmt) (hA : A.ValidExtended) {x : ℝ} (hx : A.ERealMem ↑x) :
A.abs.ERealMem ↑|x|

Absolute value encloses every represented real magnitude, including with infinite endpoints.

source
theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Interval.abs_validExtended {fmt : FloatFormat} (A : Interval fmt) (hA : A.ValidExtended) :
A.abs.ValidExtended

Absolute value preserves ordered, non-NaN endpoints in every format.

source
theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Interval.abs_sound {fmt : FloatFormat} (A : Interval fmt) (hA : A.Valid) {x : ℝ} (hx : A.RealMem x) :
A.abs.ERealMem ↑|x|

Executable interval absolute value encloses the absolute value of every represented real.

Directed square root #

source
theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Interval.sqrt_sound {fmt : FloatFormat} (A : Interval fmt) (hfmt : fmt.isIEEE = true) (hA : A.Valid) (hnonnegative : 0 ≤ A.lo.toReal) {x : ℝ} (hx : A.RealMem x) :
A.sqrt.ERealMem ↑√x

Executable interval square root encloses the square root of every represented real value.

The lower endpoint's decoded value must be nonnegative. Validity and endpoint order then imply that the upper endpoint is nonnegative as well.

source
theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Interval.sqrt_validExtended {fmt : FloatFormat} (A : Interval fmt) (hfmt : fmt.isIEEE = true) (hA : A.Valid) (hnonnegative : 0 ≤ A.lo.toReal) :
A.sqrt.ValidExtended

Square root maps a finite valid nonnegative interval to an ordered interval with non-NaN endpoints. The extended-valid conclusion avoids requiring a separate output-finiteness premise.