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.

Monotone nonlinear functions

noncomputable def NN.MLTheory.CROWN.IntervalLemmas.realSigmoid (x : ℝ) : ℝ

The real sigmoid written in the form used by NonlinearBoundOps.

theorem NN.MLTheory.CROWN.IntervalLemmas.monotone_realSigmoid : Monotone realSigmoid

The real sigmoid is monotone.

theorem NN.MLTheory.CROWN.IntervalLemmas.hasDerivAt_real_tanh (x : ℝ) : HasDerivAt Real.tanh (1 / Real.cosh x ^ 2) x

Derivative of real hyperbolic tangent.

theorem NN.MLTheory.CROWN.IntervalLemmas.strictMono_real_tanh : StrictMono Real.tanh

The real hyperbolic tangent is strictly monotone.

theorem NN.MLTheory.CROWN.IntervalLemmas.monotone_real_tanh : Monotone Real.tanh

The real hyperbolic tangent is monotone.

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\in[a,b]$ and $y\in[c,d]$, then $x+y\in[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\in[a,b]$ and $y\in[c,d]$, then $x-y\in[a-d,b-c]$.

ReLU Interval Soundness

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

Real-valued ReLU used by the interval soundness lemmas.

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

Monotonicity of ReLU on real inputs.

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

ReLU outputs are always nonnegative.

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

On the nonpositive branch, ReLU evaluates to zero.

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

On the nonnegative branch, ReLU is the identity function.

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 maps an input interval [l,u] into [max 0 l, max 0 u].

Square Interval Soundness

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

Squaring function used by interval propagation lemmas.

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

Squares over the reals are nonnegative.

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

If $0\le a\le b$, then $a^2\le b^2$.

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

Lower endpoint for the range of x ↦ x^2 over 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\in[l,u]$, then $x^2\in[\mathrm{minSq},\mathrm{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\in[l,u]$, then $|x|$ is bounded.

Directed endpoint arithmetic

@[reducible, inline]

abbrev NN.MLTheory.CROWN.IntervalLemmas.semanticValue {α : Type} [Context α] [BoundOps α] [LawfulBoundOps α] (x : α) : ℝ

Exact real meaning of an endpoint supplied by its lawful directed-arithmetic instance.

theorem NN.MLTheory.CROWN.IntervalLemmas.value_min2 {α : Type} [Context α] [BoundOps α] [LawfulBoundOps α] (a b : α) : semanticValue (BoundOps.min2 a b) = min (semanticValue a) (semanticValue b)

BoundOps.min2 selects the smaller endpoint in the mathematical interpretation.

theorem NN.MLTheory.CROWN.IntervalLemmas.value_max2 {α : Type} [Context α] [BoundOps α] [LawfulBoundOps α] (a b : α) : semanticValue (BoundOps.max2 a b) = max (semanticValue a) (semanticValue b)

BoundOps.max2 selects the larger endpoint in the mathematical interpretation.

theorem NN.MLTheory.CROWN.IntervalLemmas.directed_add_sound {α : Type} [Context α] [BoundOps α] [LawfulBoundOps α] {x y a b c d : α} (hx : inInterval (semanticValue x) (semanticValue a) (semanticValue b)) (hy : inInterval (semanticValue y) (semanticValue c) (semanticValue d)) : inInterval (semanticValue x + semanticValue y) (semanticValue (BoundOps.addDown a c)) (semanticValue (BoundOps.addUp b d))

Directed endpoint addition encloses exact real addition.

theorem NN.MLTheory.CROWN.IntervalLemmas.directed_sub_sound {α : Type} [Context α] [BoundOps α] [LawfulBoundOps α] {x y a b c d : α} (hx : inInterval (semanticValue x) (semanticValue a) (semanticValue b)) (hy : inInterval (semanticValue y) (semanticValue c) (semanticValue d)) : inInterval (semanticValue x - semanticValue y) (semanticValue (BoundOps.subDown a d)) (semanticValue (BoundOps.subUp b c))

Directed endpoint subtraction encloses exact real subtraction.

theorem NN.MLTheory.CROWN.IntervalLemmas.directed_mul_sound {α : Type} [Context α] [BoundOps α] [LawfulBoundOps α] {x y a b c d : α} (hx : inInterval (semanticValue x) (semanticValue a) (semanticValue b)) (hy : inInterval (semanticValue y) (semanticValue c) (semanticValue d)) : inInterval (semanticValue x * semanticValue y) (semanticValue (BoundOps.min2 (BoundOps.min2 (BoundOps.mulDown a c) (BoundOps.mulDown a d)) (BoundOps.min2 (BoundOps.mulDown b c) (BoundOps.mulDown b d)))) (semanticValue (BoundOps.max2 (BoundOps.max2 (BoundOps.mulUp a c) (BoundOps.mulUp a d)) (BoundOps.max2 (BoundOps.mulUp b c) (BoundOps.mulUp b d))))

The outward-rounded four-corner rule encloses exact real multiplication.

This is the scalar fact needed by rounded IBP and backward CROWN. It depends only on the declared endpoint interpretation and directed-operation laws; it does not assume that rounded scalars form a ring or that reassociation is exact.

Nonlinear transfer laws over the reals

instance NN.MLTheory.CROWN.IntervalLemmas.instLawfulNonlinearBoundOpsReal : LawfulNonlinearBoundOps ℝ

Exact real nonlinear transfers satisfy their mathematical interval contracts.