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. 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 : α) : α × α

IBP for absolute value.

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)

IBP for absolute value on boxes.

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

Affine bounds for absolute value.

Square Root

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

Square-root approximation using two Babylonian refinement steps for a Context scalar.

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

IBP for square root. Sqrt is monotone increasing on [0,∞).

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

IBP for square root on boxes.

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

Affine bounds for square root (concave function). Upper: tangent line, Lower: secant line.

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

Derivative bounds for sqrt: d/dx √x = 1/(2√x).

Reciprocal

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

Reciprocal: f(x) = 1/x.

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

IBP for reciprocal. Warning: 1/x has asymptote at 0, so this is only valid when 0 ∉ [l,u].

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

IBP for reciprocal on boxes.

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

Affine bounds for reciprocal (convex for x > 0). Lower: secant line, Upper: tangent line.

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

Derivative bounds for reciprocal: d/dx (1/x) = -1/x².

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 : ℤ) : α

Power: f(x) = x^n (integer power).

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.ibpClampScalar {α : Type} [Context α] (x_lo x_hi clamp_lo clamp_hi : α) : α × α

Clamp operation: clamp(x, lo, hi) = max(lo, min(hi, 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)

IBP for clamp.

theorem NN.MLTheory.CROWN.Operators.Arithmetic.Theorems.neg_ibp_scalar_structure {α : Type} [Context α] (l u : α) : ibpNegScalar l u = (-u, -l)

Negation IBP is exact. This states the basic structure of negation bounds.

theorem NN.MLTheory.CROWN.Operators.Arithmetic.Theorems.abs_ibp_returns_pair {α : Type} [Context α] (l u : α) : ∃ (lo : α) (hi : α), ibpAbsScalar l u = (lo, hi)

Absolute value IBP returns a pair.

theorem NN.MLTheory.CROWN.Operators.Arithmetic.Theorems.square_ibp_returns_pair {α : Type} [Context α] (l u : α) : ∃ (lo : α) (hi : α), ibpSquareScalar l u = (lo, hi)

Square IBP returns a pair.