FP32 interval enclosures

This module packages per-op absolute error bounds into the convenient enclosure form:

exact ∈ Icc (approx - eps) (approx + eps).

Interval enclosures (soundness-friendly form)

theorem TorchLean.Floats.FP32.exp_mem_Icc (a : FP32) : Real.exp a.val ∈ Set.Icc ((MathFunctions.exp a).val - eps₃₂ (Real.exp a.val)) ((MathFunctions.exp a).val + eps₃₂ (Real.exp a.val))

Enclosure for exp in the FP32 proof model.

The exact real value Real.exp a.val lies in the interval [exp(a) - ulp/2, exp(a) + ulp/2], where exp(a) is the FP32-rounded value.

theorem TorchLean.Floats.FP32.tanh_mem_Icc (a : FP32) : Real.tanh a.val ∈ Set.Icc ((MathFunctions.tanh a).val - eps₃₂ (Real.tanh a.val)) ((MathFunctions.tanh a).val + eps₃₂ (Real.tanh a.val))

Enclosure for tanh in the FP32 proof model (Real.tanh rounded once).

theorem TorchLean.Floats.FP32.log_mem_Icc (a : FP32) : Real.log a.val ∈ Set.Icc ((MathFunctions.log a).val - eps₃₂ (Real.log a.val)) ((MathFunctions.log a).val + eps₃₂ (Real.log a.val))

Enclosure for log in the FP32 proof model (Real.log rounded once).

theorem TorchLean.Floats.FP32.cos_mem_Icc (a : FP32) : Real.cos a.val ∈ Set.Icc ((MathFunctions.cos a).val - eps₃₂ (Real.cos a.val)) ((MathFunctions.cos a).val + eps₃₂ (Real.cos a.val))

Enclosure for cos in the FP32 proof model (Real.cos rounded once).

theorem TorchLean.Floats.FP32.sin_mem_Icc (a : FP32) : Real.sin a.val ∈ Set.Icc ((MathFunctions.sin a).val - eps₃₂ (Real.sin a.val)) ((MathFunctions.sin a).val + eps₃₂ (Real.sin a.val))

Enclosure for sin in the FP32 proof model (Real.sin rounded once).

theorem TorchLean.Floats.FP32.sinh_mem_Icc (a : FP32) : Real.sinh a.val ∈ Set.Icc ((MathFunctions.sinh a).val - eps₃₂ (Real.sinh a.val)) ((MathFunctions.sinh a).val + eps₃₂ (Real.sinh a.val))

Enclosure for sinh in the FP32 proof model (Real.sinh rounded once).

theorem TorchLean.Floats.FP32.cosh_mem_Icc (a : FP32) : Real.cosh a.val ∈ Set.Icc ((MathFunctions.cosh a).val - eps₃₂ (Real.cosh a.val)) ((MathFunctions.cosh a).val + eps₃₂ (Real.cosh a.val))

Enclosure for cosh in the FP32 proof model (Real.cosh rounded once).

theorem TorchLean.Floats.FP32.sqrt_mem_Icc (a : FP32) : √a.val ∈ Set.Icc ((MathFunctions.sqrt a).val - eps₃₂ √a.val) ((MathFunctions.sqrt a).val + eps₃₂ √a.val)

Enclosure for sqrt in the FP32 proof model (Real.sqrt rounded once).

theorem TorchLean.Floats.FP32.abs_mem_Icc (a : FP32) : |a.val| ∈ Set.Icc ((MathFunctions.abs a).val - eps₃₂ |a.val|) ((MathFunctions.abs a).val + eps₃₂ |a.val|)

Enclosure for abs in the FP32 proof model.

Even though |x| is exact over Real, the FP32 proof semantics rounds after each primitive.