Saturating quantization

clamp restricts an exact scalar to declared finite endpoints. spec requires a code denoting that clamped scalar exactly; it does not round an interior input onto a representable grid. The relation has no result when the clamped scalar is unrepresentable, even if both endpoints are representable. A concrete family must establish representability to obtain a total kernel.

The definitions are independent of radix, storage width, and overflow encodings.

@[inline]

def FloatLib.Numerics.Quantization.Saturating.clamp {α : Type} [LinearOrder α] (lower upper value : α) : α

Clamp to [lower, upper] when lower ≤ upper; otherwise return lower.

theorem FloatLib.Numerics.Quantization.Saturating.clamp_eq_projIcc {α : Type} [LinearOrder α] (lower upper value : α) (hendpoints : lower ≤ upper) : clamp lower upper value = ↑(Set.projIcc lower upper hendpoints value)

On a nonempty interval, clamping is Mathlib's interval projection with its bounds erased.

@[simp]

theorem FloatLib.Numerics.Quantization.Saturating.clamp_eq_self {α : Type} [LinearOrder α] {lower upper value : α} (hlower : lower ≤ value) (hupper : value ≤ upper) : clamp lower upper value = value

Clamping fixes values already inside the declared interval.

theorem FloatLib.Numerics.Quantization.Saturating.lower_le_clamp {α : Type} [LinearOrder α] (lower upper value : α) : lower ≤ clamp lower upper value

A clamped value is never below the lower endpoint.

theorem FloatLib.Numerics.Quantization.Saturating.clamp_le_upper {α : Type} [LinearOrder α] {lower upper value : α} (hendpoints : lower ≤ upper) : clamp lower upper value ≤ upper

When lower ≤ upper, a clamped value never exceeds upper.

def FloatLib.Numerics.Quantization.Saturating.spec (system : NumericalSystem) [LinearOrder system.Scalar] (lower upper : system.Scalar) : Spec Unit system.Scalar system.Code

Require exact representation of clamp lower upper input.

An unrepresentable clamped scalar has no permitted result. When lower > upper, the relation requires representation of lower for every input, following clamp's endpoint convention.