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 - Total refined evaluation for a supported expression
• LeanCert.Internal.Refined.evalDualUnchecked - 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) : Option Core.IntervalRat

Strict refined interval evaluation.

Unsupported partial operations return none, and compound expressions return none if a required subexpression fails.

Equations

• One or more equations did not get rendered due to their size.
• LeanCert.Engine.evalIntervalRefined? (LeanCert.Core.Expr.const q) ρ = some (LeanCert.Core.IntervalRat.singleton q)
• LeanCert.Engine.evalIntervalRefined? (LeanCert.Core.Expr.var i) ρ = some (ρ i)
• LeanCert.Engine.evalIntervalRefined? e_2.neg ρ = match LeanCert.Engine.evalIntervalRefined? e_2 ρ with | some I => some I.neg | none => none
• LeanCert.Engine.evalIntervalRefined? e_2.inv ρ = none
• LeanCert.Engine.evalIntervalRefined? e_2.sin ρ = match LeanCert.Engine.evalIntervalRefined? e_2 ρ with | some I => some (LeanCert.Engine.sinIntervalRefined I) | none => none
• LeanCert.Engine.evalIntervalRefined? e_2.cos ρ = match LeanCert.Engine.evalIntervalRefined? e_2 ρ with | some I => some (LeanCert.Engine.cosIntervalRefined I) | none => none
• LeanCert.Engine.evalIntervalRefined? e_2.exp ρ = match LeanCert.Engine.evalIntervalRefined? e_2 ρ with | some I => some (LeanCert.Engine.expIntervalRefined I) | none => none
• LeanCert.Engine.evalIntervalRefined? e_2.log ρ = none
• LeanCert.Engine.evalIntervalRefined? e_2.atan ρ = match LeanCert.Engine.evalIntervalRefined? e_2 ρ with | some I => some (LeanCert.Engine.atanInterval I) | none => none
• LeanCert.Engine.evalIntervalRefined? e_2.arsinh ρ = match LeanCert.Engine.evalIntervalRefined? e_2 ρ with | some I => some (LeanCert.Engine.arsinhInterval I) | none => none
• LeanCert.Engine.evalIntervalRefined? e_2.atanh ρ = none
• LeanCert.Engine.evalIntervalRefined? e_2.sinc ρ = some { lo := -1, hi := 1, le := LeanCert.Engine.evalIntervalRefined?._proof_1 }
• LeanCert.Engine.evalIntervalRefined? e_2.erf ρ = some { lo := -1, hi := 1, le := LeanCert.Engine.evalIntervalRefined?._proof_1 }
• LeanCert.Engine.evalIntervalRefined? e_2.sinh ρ = match LeanCert.Engine.evalIntervalRefined? e_2 ρ with | some I => some (LeanCert.Engine.sinhInterval I) | none => none
• LeanCert.Engine.evalIntervalRefined? e_2.cosh ρ = match LeanCert.Engine.evalIntervalRefined? e_2 ρ with | some I => some (LeanCert.Engine.coshInterval I) | none => none
• LeanCert.Engine.evalIntervalRefined? e_2.tanh ρ = match LeanCert.Engine.evalIntervalRefined? e_2 ρ with | some I => some (LeanCert.Engine.tanhInterval I) | none => none
• LeanCert.Engine.evalIntervalRefined? e_2.sqrt ρ = match LeanCert.Engine.evalIntervalRefined? e_2 ρ with | some I => some I.sqrtInterval | none => none
• LeanCert.Engine.evalIntervalRefined? (LeanCert.Core.Expr.namedConst c) ρ = some c.interval

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

Strict single-variable refined interval evaluation.

Equations

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

theorem LeanCert.Engine.evalIntervalRefined?_isSome_of_supported (e : Core.Expr) (hsupp : ADSupported e) (ρ : IntervalEnv) : (evalIntervalRefined? e ρ).isSome = true

A supported expression always succeeds in the strict refined evaluator.

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

Refined evaluation with failure ruled out by the supported-expression proof.

Equations

• LeanCert.Engine.evalIntervalRefined e hsupp ρ = Classical.choose ⋯

theorem LeanCert.Engine.evalIntervalRefined_eq_some (e : Core.Expr) (hsupp : ADSupported e) (ρ : IntervalEnv) : evalIntervalRefined? e ρ = some (evalIntervalRefined e hsupp ρ)

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

Single-variable refined evaluation with an explicit support proof.

Equations

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

theorem LeanCert.Engine.evalIntervalRefined?_correct (e : Core.Expr) (ρ_real : ℕ → ℝ) (ρ_int : IntervalEnv) (hρ : envMem ρ_real ρ_int) {I : Core.IntervalRat} (hI : evalIntervalRefined? e ρ_int = some I) : Core.Expr.eval ρ_real e ∈ I

Strict refined interval evaluation is correct whenever it returns an interval.

theorem LeanCert.Engine.evalIntervalRefined1?_correct (e : Core.Expr) (x : ℝ) (I J : Core.IntervalRat) (hx : x ∈ I) (hJ : evalIntervalRefined1? e I = some J) : Core.Expr.eval (fun (x_1 : ℕ) => x) e ∈ J

Strict single-variable refined interval evaluation is correct.

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

Refined interval evaluation is correct for supported expressions

theorem LeanCert.Engine.evalIntervalRefined1_correct (e : Core.Expr) (hsupp : ADSupported e) (x : ℝ) (I : Core.IntervalRat) (hx : x ∈ I) : Core.Expr.eval (fun (x_1 : ℕ) => x) e ∈ evalIntervalRefined1 e hsupp 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.Internal.Refined.evalDualUnchecked (e : Core.Expr) (ρ : Engine.DualEnv) : Engine.DualInterval

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

Equations

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

noncomputable def LeanCert.Internal.Refined.evalDualUnchecked1 (e : Core.Expr) (I : Core.IntervalRat) : Engine.DualInterval

Single-variable refined dual evaluation

Equations

• LeanCert.Internal.Refined.evalDualUnchecked1 e I = LeanCert.Internal.Refined.evalDualUnchecked 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 : ADSupported e) (ρ_real : ℕ → ℝ) (ρ_dual : DualEnv) (hρ : ∀ (i : ℕ), ρ_real i ∈ (ρ_dual i).val) : Core.Expr.eval ρ_real e ∈ (Internal.Refined.evalDualUnchecked e ρ_dual).val

Refined dual evaluation value is correct for supported expressions

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

Single-variable refined dual evaluation is correct for values