Refined Interval Evaluation using Taylor Models

This file provides interval evaluation functions that use Taylor-model-based bounds for transcendental functions (exp, sin, cos) when the interval is small, falling back to coarse bounds for larger intervals.

Main definitions

• sinIntervalRefined, cosIntervalRefined - Refined bounds using Taylor models
• evalIntervalRefined - Interval evaluation using refined bounds
• evalDualRefined - AD evaluation using refined bounds

Design

The refined evaluators give tighter bounds on small intervals by using Taylor approximations. For example, expIntervalRefined uses a degree-5 Taylor model when the interval width is ≤ 1, which gives much tighter bounds than the monotonicity-based expInterval.

The correctness proofs follow directly from the Taylor model correctness theorems (mem_expIntervalRefined, etc.).

Refined transcendental intervals

We define refined versions of sin and cos intervals using Taylor models, following the same pattern as expIntervalRefined.

noncomputable def LeanCert.Engine.sinIntervalRefined (I : Core.IntervalRat) : Core.IntervalRat

Refined interval bound for sin using Taylor models. For small intervals (width ≤ 1), uses degree-5 Taylor model. For larger intervals, uses the global [-1, 1] bound.

Equations

• LeanCert.Engine.sinIntervalRefined I = if I.width ≤ 1 then (LeanCert.Engine.TaylorModel.tmSin I 5).bound else LeanCert.Engine.sinInterval I

theorem LeanCert.Engine.mem_sinIntervalRefined {x : ℝ} {I : Core.IntervalRat} (hx : x ∈ I) : Real.sin x ∈ sinIntervalRefined I

FTIA for refined sin: if x ∈ I, then sin(x) ∈ sinIntervalRefined I

noncomputable def LeanCert.Engine.cosIntervalRefined (I : Core.IntervalRat) : Core.IntervalRat

Refined interval bound for cos using Taylor models. For small intervals (width ≤ 1), uses degree-5 Taylor model. For larger intervals, uses the global [-1, 1] bound.

Equations

• LeanCert.Engine.cosIntervalRefined I = if I.width ≤ 1 then (LeanCert.Engine.TaylorModel.tmCos I 5).bound else LeanCert.Engine.cosInterval I

theorem LeanCert.Engine.mem_cosIntervalRefined {x : ℝ} {I : Core.IntervalRat} (hx : x ∈ I) : Real.cos x ∈ cosIntervalRefined I

FTIA for refined cos: if x ∈ I, then cos(x) ∈ cosIntervalRefined I

noncomputable def LeanCert.Engine.logIntervalRefined (I : Core.IntervalRat.IntervalRatPos) : Core.IntervalRat

Refined interval bound for log using Taylor models. For strictly positive intervals with width ≤ 1, uses degree-5 Taylor model. For larger intervals or non-positive intervals, falls back to coarse bound.

Equations

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

theorem LeanCert.Engine.mem_logIntervalRefined {x : ℝ} {I : Core.IntervalRat.IntervalRatPos} (hx : x ∈ I.toIntervalRat) : Real.log x ∈ logIntervalRefined I

FTIA for refined log: if x ∈ I and I is positive, then log(x) ∈ logIntervalRefined I

noncomputable def LeanCert.Engine.atanhIntervalRefined' (I : Core.IntervalRat) (hlo : -1 < I.lo) (hhi : I.hi < 1) : Core.IntervalRat

Refined interval bound for atanh using Taylor models. For small intervals with |x| < 1 and width ≤ 1, uses degree-5 Taylor model. For larger intervals, uses computed bound via monotonicity. Requires -1 < I.lo and I.hi < 1 for correctness.

Equations

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

noncomputable def LeanCert.Engine.atanhIntervalRefined (I : Core.IntervalRat) : Core.IntervalRat

Refined interval bound for atanh (version without proof arguments, falls back to default)

Equations

• LeanCert.Engine.atanhIntervalRefined I = if h : -1 < I.lo ∧ I.hi < 1 then LeanCert.Engine.atanhIntervalRefined' I ⋯ ⋯ else default

theorem LeanCert.Engine.mem_atanhIntervalRefined {x : ℝ} {I : Core.IntervalRat} (hx : x ∈ I) (hlo : -1 < I.lo) (hhi : I.hi < 1) : Core.Real.atanh x ∈ atanhIntervalRefined I

FTIA for refined atanh: if x ∈ I and I ⊂ (-1, 1), then atanh(x) ∈ atanhIntervalRefined I

Refined interval evaluation

Interval evaluation that uses Taylor-model-based bounds for transcendental functions when the interval is reasonably small.

noncomputable def LeanCert.Engine.evalIntervalRefined (e : Core.Expr) (ρ : IntervalEnv) : Core.IntervalRat

Interval evaluation using refined bounds for transcendentals. Uses Taylor-model-based bounds for exp, sin, cos on small intervals. For partial functions (inv, log), returns default. Use evalInterval? instead.

Equations

• LeanCert.Engine.evalIntervalRefined (LeanCert.Core.Expr.const q) ρ = LeanCert.Core.IntervalRat.singleton q
• LeanCert.Engine.evalIntervalRefined (LeanCert.Core.Expr.var i) ρ = ρ i
• LeanCert.Engine.evalIntervalRefined (e₁.add e₂) ρ = (LeanCert.Engine.evalIntervalRefined e₁ ρ).add (LeanCert.Engine.evalIntervalRefined e₂ ρ)
• LeanCert.Engine.evalIntervalRefined (e₁.mul e₂) ρ = (LeanCert.Engine.evalIntervalRefined e₁ ρ).mul (LeanCert.Engine.evalIntervalRefined e₂ ρ)
• LeanCert.Engine.evalIntervalRefined e_2.neg ρ = (LeanCert.Engine.evalIntervalRefined e_2 ρ).neg
• LeanCert.Engine.evalIntervalRefined e_2.inv ρ = default
• LeanCert.Engine.evalIntervalRefined e_2.sin ρ = LeanCert.Engine.sinIntervalRefined (LeanCert.Engine.evalIntervalRefined e_2 ρ)
• LeanCert.Engine.evalIntervalRefined e_2.cos ρ = LeanCert.Engine.cosIntervalRefined (LeanCert.Engine.evalIntervalRefined e_2 ρ)
• LeanCert.Engine.evalIntervalRefined e_2.exp ρ = LeanCert.Engine.expIntervalRefined (LeanCert.Engine.evalIntervalRefined e_2 ρ)
• LeanCert.Engine.evalIntervalRefined e_2.log ρ = default
• LeanCert.Engine.evalIntervalRefined e_2.atan ρ = LeanCert.Engine.atanInterval (LeanCert.Engine.evalIntervalRefined e_2 ρ)
• LeanCert.Engine.evalIntervalRefined e_2.arsinh ρ = LeanCert.Engine.arsinhInterval (LeanCert.Engine.evalIntervalRefined e_2 ρ)
• LeanCert.Engine.evalIntervalRefined e_2.atanh ρ = default
• LeanCert.Engine.evalIntervalRefined e_2.sinc ρ = { lo := -1, hi := 1, le := LeanCert.Engine.evalIntervalRefined._proof_1 }
• LeanCert.Engine.evalIntervalRefined e_2.erf ρ = { lo := -1, hi := 1, le := LeanCert.Engine.evalIntervalRefined._proof_1 }
• LeanCert.Engine.evalIntervalRefined e_2.sinh ρ = LeanCert.Engine.sinhInterval (LeanCert.Engine.evalIntervalRefined e_2 ρ)
• LeanCert.Engine.evalIntervalRefined e_2.cosh ρ = LeanCert.Engine.coshInterval (LeanCert.Engine.evalIntervalRefined e_2 ρ)
• LeanCert.Engine.evalIntervalRefined e_2.tanh ρ = LeanCert.Engine.tanhInterval (LeanCert.Engine.evalIntervalRefined e_2 ρ)
• LeanCert.Engine.evalIntervalRefined e_2.sqrt ρ = (LeanCert.Engine.evalIntervalRefined e_2 ρ).sqrtInterval
• LeanCert.Engine.evalIntervalRefined LeanCert.Core.Expr.pi ρ = LeanCert.Engine.piInterval

noncomputable def LeanCert.Engine.evalIntervalRefined1 (e : Core.Expr) (I : Core.IntervalRat) : Core.IntervalRat

Single-variable refined interval evaluation

Equations

• LeanCert.Engine.evalIntervalRefined1 e I = LeanCert.Engine.evalIntervalRefined e fun (x : ℕ) => I

theorem LeanCert.Engine.evalIntervalRefined_correct (e : Core.Expr) (hsupp : ExprSupported e) (ρ_real : ℕ → ℝ) (ρ_int : IntervalEnv) (hρ : envMem ρ_real ρ_int) : Core.Expr.eval ρ_real e ∈ evalIntervalRefined e ρ_int

Refined interval evaluation is correct for supported expressions

theorem LeanCert.Engine.evalIntervalRefined1_correct (e : Core.Expr) (hsupp : ExprSupported e) (x : ℝ) (I : Core.IntervalRat) (hx : x ∈ I) : Core.Expr.eval (fun (x_1 : ℕ) => x) e ∈ evalIntervalRefined1 e I

Single-variable refined evaluation is correct

Refined dual interval (AD) evaluation

Automatic differentiation using refined interval bounds.

noncomputable def LeanCert.Engine.DualInterval.expRefined (d : DualInterval) : DualInterval

Refined dual interval for exp

Equations

• d.expRefined = { val := LeanCert.Engine.expIntervalRefined d.val, der := (LeanCert.Engine.expIntervalRefined d.val).mul d.der }

noncomputable def LeanCert.Engine.DualInterval.sinRefined (d : DualInterval) : DualInterval

Refined dual interval for sin: d/dx sin(f(x)) = cos(f(x)) * f'(x)

Equations

• d.sinRefined = { val := LeanCert.Engine.sinIntervalRefined d.val, der := (LeanCert.Engine.cosIntervalRefined d.val).mul d.der }

noncomputable def LeanCert.Engine.DualInterval.cosRefined (d : DualInterval) : DualInterval

Refined dual interval for cos: d/dx cos(f(x)) = -sin(f(x)) * f'(x)

Equations

• d.cosRefined = { val := LeanCert.Engine.cosIntervalRefined d.val, der := (LeanCert.Engine.sinIntervalRefined d.val).neg.mul d.der }

noncomputable def LeanCert.Engine.evalDualRefined (e : Core.Expr) (ρ : DualEnv) : DualInterval

Refined dual interval evaluation. For partial functions (inv, log), returns default.

Equations

• LeanCert.Engine.evalDualRefined (LeanCert.Core.Expr.const q) ρ = LeanCert.Engine.DualInterval.const q
• LeanCert.Engine.evalDualRefined (LeanCert.Core.Expr.var i) ρ = ρ i
• LeanCert.Engine.evalDualRefined (e₁.add e₂) ρ = (LeanCert.Engine.evalDualRefined e₁ ρ).add (LeanCert.Engine.evalDualRefined e₂ ρ)
• LeanCert.Engine.evalDualRefined (e₁.mul e₂) ρ = (LeanCert.Engine.evalDualRefined e₁ ρ).mul (LeanCert.Engine.evalDualRefined e₂ ρ)
• LeanCert.Engine.evalDualRefined e_2.neg ρ = (LeanCert.Engine.evalDualRefined e_2 ρ).neg
• LeanCert.Engine.evalDualRefined e_2.inv ρ = default
• LeanCert.Engine.evalDualRefined e_2.sin ρ = (LeanCert.Engine.evalDualRefined e_2 ρ).sinRefined
• LeanCert.Engine.evalDualRefined e_2.cos ρ = (LeanCert.Engine.evalDualRefined e_2 ρ).cosRefined
• LeanCert.Engine.evalDualRefined e_2.exp ρ = (LeanCert.Engine.evalDualRefined e_2 ρ).expRefined
• LeanCert.Engine.evalDualRefined e_2.log ρ = default
• LeanCert.Engine.evalDualRefined e_2.atan ρ = (LeanCert.Engine.evalDualRefined e_2 ρ).atan
• LeanCert.Engine.evalDualRefined e_2.arsinh ρ = (LeanCert.Engine.evalDualRefined e_2 ρ).arsinh
• LeanCert.Engine.evalDualRefined e_2.atanh ρ = default
• LeanCert.Engine.evalDualRefined e_2.sinc ρ = (LeanCert.Engine.evalDualRefined e_2 ρ).sinc
• LeanCert.Engine.evalDualRefined e_2.erf ρ = (LeanCert.Engine.evalDualRefined e_2 ρ).erf
• LeanCert.Engine.evalDualRefined e_2.sinh ρ = (LeanCert.Engine.evalDualRefined e_2 ρ).sinh
• LeanCert.Engine.evalDualRefined e_2.cosh ρ = (LeanCert.Engine.evalDualRefined e_2 ρ).cosh
• LeanCert.Engine.evalDualRefined e_2.tanh ρ = (LeanCert.Engine.evalDualRefined e_2 ρ).tanh
• LeanCert.Engine.evalDualRefined e_2.sqrt ρ = (LeanCert.Engine.evalDualRefined e_2 ρ).sqrt
• LeanCert.Engine.evalDualRefined LeanCert.Core.Expr.pi ρ = LeanCert.Engine.DualInterval.piConst

noncomputable def LeanCert.Engine.evalDualRefined1 (e : Core.Expr) (I : Core.IntervalRat) : DualInterval

Single-variable refined dual evaluation

Equations

• LeanCert.Engine.evalDualRefined1 e I = LeanCert.Engine.evalDualRefined e fun (x : ℕ) => LeanCert.Engine.DualInterval.varActive I

Correctness of refined dual evaluation

theorem LeanCert.Engine.DualInterval.expRefined_val_mem {d : DualInterval} {x : ℝ} (hx : x ∈ d.val) : Real.exp x ∈ d.expRefined.val

Refined exp preserves value correctness

theorem LeanCert.Engine.DualInterval.sinRefined_val_mem {d : DualInterval} {x : ℝ} (hx : x ∈ d.val) : Real.sin x ∈ d.sinRefined.val

Refined sin preserves value correctness

theorem LeanCert.Engine.DualInterval.cosRefined_val_mem {d : DualInterval} {x : ℝ} (hx : x ∈ d.val) : Real.cos x ∈ d.cosRefined.val

Refined cos preserves value correctness

theorem LeanCert.Engine.DualInterval.atan_val_mem {d : DualInterval} {x : ℝ} (hx : x ∈ d.val) : Real.arctan x ∈ d.atan.val

atan preserves value correctness

theorem LeanCert.Engine.DualInterval.arsinh_val_mem {d : DualInterval} {x : ℝ} (hx : x ∈ d.val) : Real.arsinh x ∈ d.arsinh.val

arsinh preserves value correctness

theorem LeanCert.Engine.evalDualRefined_val_correct (e : Core.Expr) (hsupp : ExprSupported e) (ρ_real : ℕ → ℝ) (ρ_dual : DualEnv) (hρ : ∀ (i : ℕ), ρ_real i ∈ (ρ_dual i).val) : Core.Expr.eval ρ_real e ∈ (evalDualRefined e ρ_dual).val

Refined dual evaluation value is correct for supported expressions

theorem LeanCert.Engine.evalDualRefined1_val_correct (e : Core.Expr) (hsupp : ExprSupported e) (x : ℝ) (I : Core.IntervalRat) (hx : x ∈ I) : Core.Expr.eval (fun (x_1 : ℕ) => x) e ∈ (evalDualRefined1 e I).val

Single-variable refined dual evaluation is correct for values