NN.MLTheory.CROWN.Operators.Arithmetic

IBP and affine transfer rules for arithmetic primitives (negation, absolute value, reciprocal, square root, powers, min/max) used by the CROWN bound propagation engine.

Negation

def NN.MLTheory.CROWN.Operators.Arithmetic.neg {α : Type} [Context α] (x : α) : α

Negation, $f(x)=-x$, is the simplest linear operation.

def NN.MLTheory.CROWN.Operators.Arithmetic.ibpNegScalar {α : Type} [Context α] (l u : α) : α × α

IBP for negation. Just swaps and negates bounds.

def NN.MLTheory.CROWN.Operators.Arithmetic.ibpNeg {α : Type} [Context α] (n : ℕ) (B : Box α (Spec.Shape.dim n Spec.Shape.scalar)) : Box α (Spec.Shape.dim n Spec.Shape.scalar)

IBP for negation on boxes.

def NN.MLTheory.CROWN.Operators.Arithmetic.affNeg {α : Type} [Context α] : α × α × α × α

Affine bounds for negation (exact).

def NN.MLTheory.CROWN.Operators.Arithmetic.derivNeg {α : Type} [Context α] : α × α

Derivative of negation (constant -1).

Absolute Value

def NN.MLTheory.CROWN.Operators.Arithmetic.abs {α : Type} [Context α] (x : α) : α

Absolute value: $f(x)=|x|$.

def NN.MLTheory.CROWN.Operators.Arithmetic.ibpAbsScalar {α : Type} [Context α] (l u : α) : α × α

Interval propagation rule for scalar absolute value over [l,u].

def NN.MLTheory.CROWN.Operators.Arithmetic.ibpAbs {α : Type} [Context α] (n : ℕ) (B : Box α (Spec.Shape.dim n Spec.Shape.scalar)) : Box α (Spec.Shape.dim n Spec.Shape.scalar)

Apply the scalar absolute-value interval rule coordinatewise to a vector box.

def NN.MLTheory.CROWN.Operators.Arithmetic.affAbs {α : Type} [Context α] (l u : α) : α × α × α × α

Affine lower and upper bounds for absolute value on an ordered interval [l, u].

On an interval crossing zero, the lower bound is the zero line and the upper bound is the secant through (l, -l) and (u, u). The degenerate interval [0, 0] is represented by the zero line.

Reciprocal

def NN.MLTheory.CROWN.Operators.Arithmetic.reciprocal {α : Type} [Context α] (x : α) : α

Reciprocal: $f(x)=1/x$.

def NN.MLTheory.CROWN.Operators.Arithmetic.ibpReciprocal? {α : Type} [Context α] (n : ℕ) (B : Box α (Spec.Shape.dim n Spec.Shape.scalar)) : Option (Box α (Spec.Shape.dim n Spec.Shape.scalar))

IBP for reciprocal on boxes, defined only when every coordinate interval excludes zero.

Power

def NN.MLTheory.CROWN.Operators.Arithmetic.posPow {α : Type} [Context α] (base : α) (exp : ℕ) : α

Helper for positive integer power.

def NN.MLTheory.CROWN.Operators.Arithmetic.powerInt {α : Type} [Context α] (x : α) (n : ℤ) : α

Integer power: $f(x)=x^n$.

def NN.MLTheory.CROWN.Operators.Arithmetic.ibpSquareScalar {α : Type} [Context α] (l u : α) : α × α

IBP for x².

def NN.MLTheory.CROWN.Operators.Arithmetic.ibpSquare {α : Type} [Context α] (n : ℕ) (B : Box α (Spec.Shape.dim n Spec.Shape.scalar)) : Box α (Spec.Shape.dim n Spec.Shape.scalar)

IBP for x² on boxes.

def NN.MLTheory.CROWN.Operators.Arithmetic.affSquare {α : Type} [Context α] (l u : α) : α × α × α × α

Affine bounds for x².

Min/Max

def NN.MLTheory.CROWN.Operators.Arithmetic.ibpMin {α : Type} [Context α] (n : ℕ) (B1 B2 : Box α (Spec.Shape.dim n Spec.Shape.scalar)) : Box α (Spec.Shape.dim n Spec.Shape.scalar)

Elementwise minimum of two boxes.

def NN.MLTheory.CROWN.Operators.Arithmetic.ibpMax {α : Type} [Context α] (n : ℕ) (B1 B2 : Box α (Spec.Shape.dim n Spec.Shape.scalar)) : Box α (Spec.Shape.dim n Spec.Shape.scalar)

Elementwise maximum of two boxes.

def NN.MLTheory.CROWN.Operators.Arithmetic.clampScalar {α : Type} [Context α] (x clamp_lo clamp_hi : α) : α

Clamp one scalar with the same composition used by Spec.clampSpec: min clamp_hi (max clamp_lo x).

In particular, when clamp_lo > clamp_hi, the result is clamp_hi. This agrees with PyTorch's documented behavior instead of silently switching the two bounds.

def NN.MLTheory.CROWN.Operators.Arithmetic.ibpClampScalar {α : Type} [Context α] (x_lo x_hi clamp_lo clamp_hi : α) : α × α

Clamp operation: clamp(x, lo, hi) = min(hi, max(lo, x)).

def NN.MLTheory.CROWN.Operators.Arithmetic.ibpClamp {α : Type} [Context α] (n : ℕ) (B : Box α (Spec.Shape.dim n Spec.Shape.scalar)) (clamp_lo clamp_hi : α) : Box α (Spec.Shape.dim n Spec.Shape.scalar)

Interval propagation for clamp, applied coordinatewise to a vector box.