Exact interval arithmetic for radical expressions

A square-root node carries rational lower and upper witnesses. The evaluator checks their squares exactly, so every successful enclosure has a kernel-checked real-number semantics.

inductive LeanPool.Besicovitch.RadicalExpression (n : ℕ) : Type

Rational expressions with explicitly certified square-root bounds.

• var {n : ℕ} : Fin n → RadicalExpression n
• literal {n : ℕ} : ℚ → RadicalExpression n
• add {n : ℕ} : RadicalExpression n → RadicalExpression n → RadicalExpression n
• neg {n : ℕ} : RadicalExpression n → RadicalExpression n
• mul {n : ℕ} : RadicalExpression n → RadicalExpression n → RadicalExpression n
• inv {n : ℕ} : RadicalExpression n → RadicalExpression n
• sqrt {n : ℕ} : RadicalExpression n → ℚ → ℚ → RadicalExpression n

noncomputable def LeanPool.Besicovitch.RadicalExpression.eval {n : ℕ} : RadicalExpression n → (Fin n → ℝ) → ℝ

Evaluate a radical expression in a real environment.

Equations

• (LeanPool.Besicovitch.RadicalExpression.var i).eval x✝ = x✝ i
• (LeanPool.Besicovitch.RadicalExpression.literal q).eval x✝ = ↑q
• (f.add g).eval x✝ = f.eval x✝ + g.eval x✝
• f.neg.eval x✝ = -f.eval x✝
• (f.mul g).eval x✝ = f.eval x✝ * g.eval x✝
• f.inv.eval x✝ = (f.eval x✝)⁻¹
• (f.sqrt a a_1).eval x✝ = √(f.eval x✝)

def LeanPool.Besicovitch.RadicalExpression.enclosure {n : ℕ} : RadicalExpression n → (Fin n → RationalInterval) → Option RationalInterval

Evaluate by exact rational intervals, rejecting unsafe inverses or square-root witnesses.

Equations

• One or more equations did not get rendered due to their size.
• (LeanPool.Besicovitch.RadicalExpression.var i).enclosure x✝ = some (x✝ i)
• (LeanPool.Besicovitch.RadicalExpression.literal q).enclosure x✝ = some (LeanPool.Besicovitch.RationalInterval.singleton q)
• (f.add g).enclosure x✝ = do let I ← f.enclosure x✝ let J ← g.enclosure x✝ pure (I.add J)
• f.neg.enclosure x✝ = do let I ← f.enclosure x✝ pure I.neg
• (f.mul g).enclosure x✝ = do let I ← f.enclosure x✝ let J ← g.enclosure x✝ pure (I.mul J)
• f.inv.enclosure x✝ = do let I ← f.enclosure x✝ if h : 0 < I.lower ∨ I.upper < 0 then pure (I.inv h) else none

def LeanPool.Besicovitch.RadicalExpression.enclosureWithin {n : ℕ} (f : RadicalExpression n) (X : Fin n → RationalInterval) (target : RationalInterval) : Option RationalInterval

Check an enclosure and widen it to a simpler rational target interval.

Equations

• f.enclosureWithin X target = do let I ← f.enclosure X if target.lower ≤ I.lower ∧ I.upper ≤ target.upper then some target else none

def LeanPool.Besicovitch.RadicalExpression.certifiesWithin {n : ℕ} (f : RadicalExpression n) (X : Fin n → RationalInterval) (target : RationalInterval) : Bool

Decide whether the computed enclosure lies in a given rational target interval.

Equations

• f.certifiesWithin X target = match f.enclosure X with | none => false | some I => decide (target.lower ≤ I.lower ∧ I.upper ≤ target.upper)

theorem LeanPool.Besicovitch.RadicalExpression.enclosure_sound {n : ℕ} {f : RadicalExpression n} {X : Fin n → RationalInterval} {x : Fin n → ℝ} (hx : ∀ (i : Fin n), (X i).Contains (x i)) {I : RationalInterval} (hI : f.enclosure X = some I) : I.Contains (f.eval x)

Every successful radical enclosure contains the real value of the expression.

theorem LeanPool.Besicovitch.RadicalExpression.enclosureWithin_sound {n : ℕ} {f : RadicalExpression n} {X : Fin n → RationalInterval} {x : Fin n → ℝ} (hx : ∀ (i : Fin n), (X i).Contains (x i)) {target : RationalInterval} (h : f.enclosureWithin X target = some target) : target.Contains (f.eval x)

A successful widened enclosure contains the real value of the expression.

theorem LeanPool.Besicovitch.RadicalExpression.certifiesWithin_sound {n : ℕ} {f : RadicalExpression n} {X : Fin n → RationalInterval} {x : Fin n → ℝ} (hx : ∀ (i : Fin n), (X i).Contains (x i)) {target : RationalInterval} (h : f.certifiesWithin X target = true) : target.Contains (f.eval x)

A successful Boolean certificate encloses the real value of the expression.