Reduction operator bounds

This file defines simple IBP and affine transfer rules for common reductions over flattened vectors (sum/mean/max/min/prod). These rules are primarily intended for the graph-based verifier.

Non-smooth reductions (max/min) are treated conservatively (interval enclosures), and prod is treated as a bilinear-style operation (also conservatively).

def NN.MLTheory.CROWN.Operators.Reduce.getDimScalarFn {α : Type} {n : ℕ} (t : Spec.Tensor α (Spec.Shape.dim n Spec.Shape.scalar)) : Fin n → Spec.Tensor α Spec.Shape.scalar

Helper to extract scalar from dim-scalar tensor.

def NN.MLTheory.CROWN.Operators.Reduce.tensorSum {α : Type} [Context α] {n : ℕ} (t : Spec.Tensor α (Spec.Shape.dim n Spec.Shape.scalar)) : α

Compute sum of a 1D tensor.

def NN.MLTheory.CROWN.Operators.Reduce.ibpReduceSum {α : Type} [Context α] (xB : FlatBox α) : FlatBox α

IBP for ReduceSum: sum of intervals = interval of sums. [Σ lo_i, Σ hi_i]

def NN.MLTheory.CROWN.Operators.Reduce.ibpReduceMean {α : Type} [Context α] (xB : FlatBox α) : FlatBox α

IBP for ReduceMean: mean of intervals. [Σ lo_i / n, Σ hi_i / n]

def NN.MLTheory.CROWN.Operators.Reduce.ibpReduceMax {α : Type} [Context α] (xB : FlatBox α) : FlatBox α

IBP for ReduceMax: max over intervals. lo = max of individual lower bounds (conservative but sound) hi = max of individual upper bounds

Note: This is conservative. The true lower bound on max(x) is max(min_i x_i), but we use max(lo_i) which may be looser.

def NN.MLTheory.CROWN.Operators.Reduce.ibpReduceMin {α : Type} [Context α] (xB : FlatBox α) : FlatBox α

IBP for ReduceMin: min over intervals. lo = min of individual lower bounds (tight) hi = min of individual upper bounds (conservative but sound)

def NN.MLTheory.CROWN.Operators.Reduce.ibpReduceProd {α : Type} [Context α] (xB : FlatBox α) : FlatBox α

IBP for ReduceProd: product over intervals. This is more complex due to sign changes. For each element, compute all 4 corner products and take min/max.

For n elements: Π[lo_i, hi_i] requires 2^n evaluations in general. We use a recursive interval multiplication approach.

def NN.MLTheory.CROWN.Operators.Reduce.affReduceSum {α : Type} [Context α] {inDim : ℕ} (n : ℕ) (aff : AffineVec α inDim n) : AffineVec α inDim 1

Affine bounds for ReduceSum: y = Σ x_i = [1, 1, ..., 1] · x The affine form maps inDim to 1: A = [[sum of A rows]], c = [sum of c].

def NN.MLTheory.CROWN.Operators.Reduce.affReduceMean {α : Type} [Context α] {inDim : ℕ} (n : ℕ) (aff : AffineVec α inDim n) : AffineVec α inDim 1

Affine bounds for ReduceMean: y = (Σ x_i) / n = (1/n) * Σ x_i

def NN.MLTheory.CROWN.Operators.Reduce.derivReduceSum {α : Type} [Context α] (dB : FlatBox α) : FlatBox α

Derivative bounds for ReduceSum: ∂(Σ x_i)/∂x_j = 1 for all j. If input derivatives are in [dlo, dhi], output derivative = Σ d_i.

def NN.MLTheory.CROWN.Operators.Reduce.derivReduceMean {α : Type} [Context α] (dB : FlatBox α) : FlatBox α

Derivative bounds for ReduceMean: ∂(mean)/∂x_j = 1/n for all j.

def NN.MLTheory.CROWN.Operators.Reduce.derivReduceMax {α : Type} [Context α] (_xB dB : FlatBox α) : FlatBox α

Derivative bounds for ReduceMax: non-smooth, uses subgradient. ∂max/∂x_i = 1 if x_i is the max, 0 otherwise. For intervals, we bound: derivative ∈ [0, 1] for argmax candidates.

def NN.MLTheory.CROWN.Operators.Reduce.derivReduceMin {α : Type} [Context α] (xB dB : FlatBox α) : FlatBox α

Derivative bounds for ReduceMin: similar to max but argmin.

def NN.MLTheory.CROWN.Operators.Reduce.AxisReduce.ibpReduceSumAxis0 {α : Type} [Context α] {rows cols : ℕ} (xB : Box α (Spec.Shape.dim rows (Spec.Shape.dim cols Spec.Shape.scalar))) : Box α (Spec.Shape.dim 1 (Spec.Shape.dim cols Spec.Shape.scalar))

IBP for ReduceSum along axis 0 (sum over rows) for 2D: [rows, cols] → [1, cols]. Each output column j = Σ_i input[i,j].

def NN.MLTheory.CROWN.Operators.Reduce.AxisReduce.ibpReduceSumAxis1 {α : Type} [Context α] {rows cols : ℕ} (xB : Box α (Spec.Shape.dim rows (Spec.Shape.dim cols Spec.Shape.scalar))) : Box α (Spec.Shape.dim rows (Spec.Shape.dim 1 Spec.Shape.scalar))

IBP for ReduceSum along axis 1 (sum over columns) for 2D: [rows, cols] → [rows, 1]. Each output row i = Σ_j input[i,j].

theorem NN.MLTheory.CROWN.Operators.Reduce.Theorems.ibp_reduce_sum_dim {α : Type} [Context α] (xB : FlatBox α) : (ibpReduceSum xB).dim = 1

ReduceSum output dimension is 1.

theorem NN.MLTheory.CROWN.Operators.Reduce.Theorems.ibp_reduce_mean_dim {α : Type} [Context α] (xB : FlatBox α) : (ibpReduceMean xB).dim = 1

ReduceMean output dimension is 1.

theorem NN.MLTheory.CROWN.Operators.Reduce.Theorems.ibp_reduce_max_dim {α : Type} [Context α] (xB : FlatBox α) : (ibpReduceMax xB).dim = 1

ReduceMax output dimension is 1.

theorem NN.MLTheory.CROWN.Operators.Reduce.Theorems.ibp_reduce_min_dim {α : Type} [Context α] (xB : FlatBox α) : (ibpReduceMin xB).dim = 1

ReduceMin output dimension is 1.

theorem NN.MLTheory.CROWN.Operators.Reduce.Theorems.ibp_reduce_prod_dim {α : Type} [Context α] (xB : FlatBox α) : (ibpReduceProd xB).dim = 1

ReduceProd output dimension is 1.

theorem NN.MLTheory.CROWN.Operators.Reduce.Theorems.aff_reduce_sum_dim {α : Type} [Context α] {inDim : ℕ} (n : ℕ) (aff : AffineVec α inDim n) : ∃ (A : Spec.Tensor α (Spec.Shape.dim 1 (Spec.Shape.dim inDim Spec.Shape.scalar))) (c : Spec.Tensor α (Spec.Shape.dim 1 Spec.Shape.scalar)), (affReduceSum n aff).A = A ∧ (affReduceSum n aff).c = c

Affine reduce sum output dimension is 1.