Interval arithmetic lemmas (ℝ)

This file provides foundational lemmas for interval arithmetic operations used in CROWN/LiRPA bound propagation soundness proofs.

It is primarily intended as a small toolbox for proof scripts and examples; it lives under NN/MLTheory/CROWN/Extras/ to keep the main CROWN modules focused on the bound propagation API.

Basic Interval Membership

def NN.MLTheory.CROWN.IntervalLemmas.inInterval (x lo hi : ℝ) : Prop

A value is in an interval [lo, hi]

theorem NN.MLTheory.CROWN.IntervalLemmas.inInterval_refl (x : ℝ) : inInterval x x x

theorem NN.MLTheory.CROWN.IntervalLemmas.inInterval_of_bounds {x lo hi : ℝ} (hlo : lo ≤ x) (hhi : x ≤ hi) : inInterval x lo hi

Addition Interval Soundness

theorem NN.MLTheory.CROWN.IntervalLemmas.interval_add_sound {x y a b c d : ℝ} (hx : inInterval x a b) (hy : inInterval y c d) : inInterval (x + y) (a + c) (b + d)

If x ∈ [a,b] and y ∈ [c,d], then x + y ∈ [a+c, b+d]

Subtraction Interval Soundness

theorem NN.MLTheory.CROWN.IntervalLemmas.interval_sub_sound {x y a b c d : ℝ} (hx : inInterval x a b) (hy : inInterval y c d) : inInterval (x - y) (a - d) (b - c)

If x ∈ [a,b] and y ∈ [c,d], then x - y ∈ [a-d, b-c]

Multiplication Interval Soundness

def NN.MLTheory.CROWN.IntervalLemmas.min4 (p q r s : ℝ) : ℝ

Helper: minimum of four values

def NN.MLTheory.CROWN.IntervalLemmas.max4 (p q r s : ℝ) : ℝ

Helper: maximum of four values

theorem NN.MLTheory.CROWN.IntervalLemmas.interval_mul_sound {x y a b c d : ℝ} (hx : inInterval x a b) (hy : inInterval y c d) : inInterval (x * y) (min4 (a * c) (a * d) (b * c) (b * d)) (max4 (a * c) (a * d) (b * c) (b * d))

For multiplication, the interval is [min(ac,ad,bc,bd), max(ac,ad,bc,bd)].

The proof requires 9-case analysis based on signs of interval endpoints:

1. a >= 0, c >= 0: min=ac, max=bd
2. a >= 0, c < 0 <= d: min=bc, max=bd
3. a >= 0, d < 0: min=bc, max=ad
4. a < 0 <= b, c >= 0: min=ad, max=bd
5. a < 0 <= b, c < 0 <= d: min=min(ad,bc), max=max(ac,bd)
6. a < 0 <= b, d < 0: min=bc, max=ac
7. b < 0, c >= 0: min=ad, max=bc
8. b < 0, c < 0 <= d: min=ad, max=ac
9. b < 0, d < 0: min=bd, max=ac

The key insight is that extrema of the bilinear function x*y over a rectangle [a,b] x [c,d] occur at the corners.

ReLU Interval Soundness

def NN.MLTheory.CROWN.IntervalLemmas.relu (x : ℝ) : ℝ

ReLU function: max(0, x)

theorem NN.MLTheory.CROWN.IntervalLemmas.relu_monotone {x y : ℝ} (h : x ≤ y) : relu x ≤ relu y

ReLU is monotone

theorem NN.MLTheory.CROWN.IntervalLemmas.relu_nonneg (x : ℝ) : 0 ≤ relu x

ReLU is non-negative

theorem NN.MLTheory.CROWN.IntervalLemmas.relu_of_nonpos {x : ℝ} (h : x ≤ 0) : relu x = 0

If x ≤ 0, then relu(x) = 0

theorem NN.MLTheory.CROWN.IntervalLemmas.relu_of_nonneg {x : ℝ} (h : 0 ≤ x) : relu x = x

If 0 ≤ x, then relu(x) = x

theorem NN.MLTheory.CROWN.IntervalLemmas.interval_relu_sound {x l u : ℝ} (h : inInterval x l u) : inInterval (relu x) (max 0 l) (max 0 u)

ReLU interval: if x ∈ [l, u], then relu(x) ∈ [max(0,l), max(0,u)]

Square Interval Soundness

def NN.MLTheory.CROWN.IntervalLemmas.square (x : ℝ) : ℝ

Square function

theorem NN.MLTheory.CROWN.IntervalLemmas.square_nonneg (x : ℝ) : 0 ≤ square x

Square is non-negative

theorem NN.MLTheory.CROWN.IntervalLemmas.square_le_square_of_nonneg {a b : ℝ} (ha : 0 ≤ a) (hab : a ≤ b) : square a ≤ square b

If 0 ≤ a ≤ b, then a² ≤ b²

noncomputable def NN.MLTheory.CROWN.IntervalLemmas.intervalSquareMin (l u : ℝ) : ℝ

Minimum square in an interval

noncomputable def NN.MLTheory.CROWN.IntervalLemmas.intervalSquareMax (l u : ℝ) : ℝ

Maximum square in an interval

theorem NN.MLTheory.CROWN.IntervalLemmas.interval_square_sound {x l u : ℝ} (h : inInterval x l u) : inInterval (square x) (intervalSquareMin l u) (intervalSquareMax l u)

Square interval soundness: if x ∈ [l, u], then x² ∈ [minSq, maxSq]

Negation Interval

theorem NN.MLTheory.CROWN.IntervalLemmas.interval_neg_sound {x a b : ℝ} (h : inInterval x a b) : inInterval (-x) (-b) (-a)

Negation flips and swaps the interval: -[a,b] = [-b, -a]

Absolute Value Interval

theorem NN.MLTheory.CROWN.IntervalLemmas.interval_abs_sound {x l u : ℝ} (h : inInterval x l u) : 0 ≤ |x| ∧ |x| ≤ max |l| |u|

If x ∈ [l, u], then |x| is bounded