Affine Arithmetic: Non-Linear Operations

This file extends Affine Arithmetic with division and square root.

Key Insight

For non-linear functions f(x), we use the Chebyshev linearization:

1. Find the best linear approximation L(x) = α·x + β over the interval
2. Compute the maximum approximation error δ = max|f(x) - L(x)|
3. Result: α·â + β + [-δ, δ] where â is the affine input

This is sound because for any x ∈ [lo, hi]: f(x) ∈ L(x) + [-δ, δ] = α·x + β + [-δ, δ]

Main definitions

• AffineForm.inv - Interval inversion with linearization
• AffineForm.sqrt - Square root using Chebyshev approximation
• AffineForm.div - Division via multiplication by inverse

Inversion (1/x)

def LeanCert.Engine.Affine.AffineForm.inv (a : AffineForm) : AffineForm

Conservative inversion for affine forms.

For positive intervals [lo, hi]:

• Linear approx: L(x) = -1/(lo·hi)·x + (lo+hi)/(lo·hi)
• Max error at endpoints and midpoint

We use a simpler approach: convert to interval, invert, convert back. This loses correlation but is always sound.

Equations

• One or more equations did not get rendered due to their size.

def LeanCert.Engine.Affine.AffineForm.invChebyshev (a : AffineForm) (_hpos : 0 < a.toInterval.lo) : AffineForm

Chebyshev linearization for 1/x on [lo, hi] with 0 < lo.

The optimal linear approximation minimizes max error. For 1/x, the Chebyshev approximation is: L(x) = -1/(lo·hi)·x + (lo+hi)/(lo·hi) with error bounded by (√hi - √lo)² / (2·lo·hi)

Equations

• One or more equations did not get rendered due to their size.

Square Root

def LeanCert.Engine.Affine.AffineForm.sqrt (a : AffineForm) : AffineForm

Square root using Chebyshev linearization.

For √x on [lo, hi] with 0 ≤ lo:

• Optimal linear: L(x) = x/(√lo + √hi) + √(lo·hi)/(√lo + √hi)
• Error: (√hi - √lo)² / 4

Simplified approach: use interval sqrt, convert back.

Equations

• One or more equations did not get rendered due to their size.

def LeanCert.Engine.Affine.AffineForm.sqrtChebyshev (a : AffineForm) (_hpos : 0 < a.toInterval.lo) : AffineForm

Chebyshev linearization for √x on [lo, hi].

Optimal approximation: L(x) = x/(2·√m) + √m/2 where m = (lo + hi)/2 is the midpoint. Error ≤ (√hi - √lo)²/4

Equations

• One or more equations did not get rendered due to their size.

Division

def LeanCert.Engine.Affine.AffineForm.div (a b : AffineForm) : AffineForm

Division: a / b = a · (1/b)

Equations

• a.div b = a.mul b.inv

def LeanCert.Engine.Affine.AffineForm.divChebyshev (a b : AffineForm) (hpos : 0 < b.toInterval.lo) : AffineForm

Division with Chebyshev linearization for the inverse

Equations

• a.divChebyshev b hpos = a.mul (b.invChebyshev hpos)

Power Operations

@[irreducible]

def LeanCert.Engine.Affine.AffineForm.pow (a : AffineForm) : ℕ → AffineForm

Natural number power

Equations

• a.pow 0 = LeanCert.Engine.Affine.AffineForm.const 1
• a.pow 1 = a
• a.pow n.succ.succ = if ((n + 2) % 2 == 0) = true then (a.pow ((n + 2) / 2)).mul (a.pow ((n + 2) / 2)) else ((a.pow ((n + 2) / 2)).mul (a.pow ((n + 2) / 2))).mul a

Soundness (Placeholder)

theorem LeanCert.Engine.Affine.AffineForm.mem_inv {a : AffineForm} {eps : NoiseAssignment} {v : ℝ} (hvalid : validNoise eps) (hlen : List.length eps = a.coeffs.length) (hmem : a.mem_affine eps v) (_hv_pos : 0 < v) (hI_pos : 0 < a.toInterval.lo) : a.inv.mem_affine eps (1 / v)

Inversion is sound when interval is positive

theorem LeanCert.Engine.Affine.AffineForm.mem_sqrt {a : AffineForm} {eps : NoiseAssignment} {v : ℝ} (hvalid : validNoise eps) (hlen : List.length eps = a.coeffs.length) (hmem : a.mem_affine eps v) (hv_nonneg : 0 ≤ v) : a.sqrt.mem_affine eps √v

Square root is sound for non-negative inputs

theorem LeanCert.Engine.Affine.AffineForm.mem_sqrt' {a : AffineForm} {eps : NoiseAssignment} {v : ℝ} (hvalid : validNoise eps) (hmem : a.mem_affine eps v) : a.sqrt.mem_affine eps √v

Square root is sound without a nonnegativity hypothesis.