RpowInterval — Exact Rational Power for Nonneg Intervals

For nonneg intervals with natural exponents, rpow(x, n) = x^n is exact ℚ arithmetic. This covers the dominant case in RSA: belief-based utility uses rpow(L0(w|u), α) where α is typically 1 (or another natural number).

Key property

Zero approximation error: the entire interval computation is exact when α ∈ ℕ and the base data is rational.

def Linglib.Interval.rpowNat (a : QInterval) (n : ℕ) (ha : 0 ≤ a.lo) : QInterval

Exact rational power for nonneg intervals: [lo^n, hi^n]. Requires 0 ≤ lo (so the interval is nonneg) and n : ℕ. Exact — no approximation error.

Equations

• Linglib.Interval.rpowNat a n ha = { lo := a.lo ^ n, hi := a.hi ^ n, valid := ⋯ }

theorem Linglib.Interval.rpowNat_containsReal {a : QInterval} {x : ℝ} {n : ℕ} (ha : 0 ≤ a.lo) (hx : a.containsReal x) : (rpowNat a n ha).containsReal (x ^ ↑n)

def Linglib.Interval.rpowZero : QInterval

Interval for rpow(x, 0) = [1, 1].

Equations

• Linglib.Interval.rpowZero = Linglib.Interval.QInterval.exact 1

theorem Linglib.Interval.rpowZero_containsReal (x : ℝ) : rpowZero.containsReal (x ^ 0)

theorem Linglib.Interval.rpowOne_containsReal {a : QInterval} {x : ℝ} (_ha : 0 ≤ a.lo) (hx : a.containsReal x) : a.containsReal (x ^ 1)

For rpow(x, 1) with x ∈ interval a, the result is just a.