Taylor Model Composition and Expression Integration

This file provides composition operations for Taylor models and integration with the Expr AST. It builds on the core Taylor model infrastructure and function-specific Taylor approximations to enable automatic Taylor model construction for expression trees.

Main definitions

• TaylorModel.sin, TaylorModel.cos, TaylorModel.exp - Interval-based composition
• TaylorModel.fromExpr, TaylorModel.fromExpr? - Expression to Taylor model conversion
• expIntervalRefined - Refined exp interval using Taylor models

Main results

• fromExpr_evalSet_correct - Taylor models from expressions are correct
• fromExpr_correct - Expression evaluation lies in Taylor model bound
• mem_expIntervalRefined - FTIA for refined exp interval

Interval-based composition operations

Given a TM for an argument, these operations return TMs that bound transcendental functions of that argument. They use function-level Taylor models for tight bounds.

noncomputable def LeanCert.Engine.TaylorModel.sin (tm : TaylorModel) (degree : ℕ) : TaylorModel

Interval-based sin composition. Given a TM for the argument, returns a TM that bounds sin of the argument. Uses function-level Taylor model for tight bounds.

Equations

• tm.sin degree = { poly := 0, remainder := (LeanCert.Engine.TaylorModel.tmSin tm.bound degree).bound, center := tm.center, domain := tm.domain }

noncomputable def LeanCert.Engine.TaylorModel.cos (tm : TaylorModel) (degree : ℕ) : TaylorModel

Interval-based cos composition. Given a TM for the argument, returns a TM that bounds cos of the argument. Uses function-level Taylor model for tight bounds.

Equations

• tm.cos degree = { poly := 0, remainder := (LeanCert.Engine.TaylorModel.tmCos tm.bound degree).bound, center := tm.center, domain := tm.domain }

noncomputable def LeanCert.Engine.TaylorModel.exp (tm : TaylorModel) (degree : ℕ) : TaylorModel

Interval-based exp composition. Given a TM for the argument, returns a TM that bounds exp of the argument. Uses function-level Taylor model for tight bounds.

Equations

• tm.exp degree = { poly := 0, remainder := (LeanCert.Engine.TaylorModel.tmExp tm.bound degree).bound, center := tm.center, domain := tm.domain }

noncomputable def LeanCert.Engine.TaylorModel.sinh (tm : TaylorModel) (degree : ℕ) : TaylorModel

Interval-based sinh composition. Given a TM for the argument, returns a TM that bounds sinh of the argument. Uses function-level Taylor model for tight bounds.

Equations

• tm.sinh degree = { poly := 0, remainder := (LeanCert.Engine.TaylorModel.tmSinh tm.bound degree).bound, center := tm.center, domain := tm.domain }

noncomputable def LeanCert.Engine.TaylorModel.cosh (tm : TaylorModel) (degree : ℕ) : TaylorModel

Interval-based cosh composition. Given a TM for the argument, returns a TM that bounds cosh of the argument. Uses function-level Taylor model for tight bounds.

Equations

• tm.cosh degree = { poly := 0, remainder := (LeanCert.Engine.TaylorModel.tmCosh tm.bound degree).bound, center := tm.center, domain := tm.domain }

noncomputable def LeanCert.Engine.TaylorModel.tanh (tm : TaylorModel) (degree : ℕ) : TaylorModel

Interval-based tanh composition. Given a TM for the argument, returns a TM that bounds tanh of the argument. Uses tanh = sinh / cosh with the fact that cosh ≥ 1 > 0.

Equations

• tm.tanh degree = { poly := 0, remainder := (LeanCert.Engine.TaylorModel.tmTanh tm.bound degree).bound, center := tm.center, domain := tm.domain }

noncomputable def LeanCert.Engine.TaylorModel.atan (tm : TaylorModel) (degree : ℕ) : TaylorModel

Interval-based atan composition. Given a TM for the argument, returns a TM that bounds atan of the argument. Uses function-level Taylor model. Valid for |arg| ≤ 1.

Equations

• tm.atan degree = { poly := 0, remainder := (LeanCert.Engine.TaylorModel.tmAtan tm.bound degree).bound, center := tm.center, domain := tm.domain }

noncomputable def LeanCert.Engine.TaylorModel.atanh (tm : TaylorModel) (degree : ℕ) : TaylorModel

Interval-based atanh composition. Given a TM for the argument, returns a TM that bounds atanh of the argument. Uses function-level Taylor model. Valid for |arg| < 1.

Equations

• tm.atanh degree = { poly := 0, remainder := (LeanCert.Engine.TaylorModel.tmAtanh tm.bound degree).bound, center := tm.center, domain := tm.domain }

noncomputable def LeanCert.Engine.TaylorModel.asinh (tm : TaylorModel) (degree : ℕ) : TaylorModel

Interval-based asinh composition. Given a TM for the argument, returns a TM that bounds asinh of the argument. Uses function-level Taylor model.

Equations

• tm.asinh degree = { poly := 0, remainder := (LeanCert.Engine.TaylorModel.tmAsinh tm.bound degree).bound, center := tm.center, domain := tm.domain }

noncomputable def LeanCert.Engine.TaylorModel.sinc (tm : TaylorModel) (degree : ℕ) : TaylorModel

Interval-based sinc composition. Given a TM for the argument, returns a TM that bounds sinc of the argument. sinc(z) = sin(z)/z for z ≠ 0, sinc(0) = 1.

Equations

• tm.sinc degree = { poly := 0, remainder := (LeanCert.Engine.TaylorModel.tmSinc tm.bound degree).bound, center := tm.center, domain := tm.domain }

noncomputable def LeanCert.Engine.TaylorModel.erf (tm : TaylorModel) (degree : ℕ) : TaylorModel

Interval-based erf composition. Given a TM for the argument, returns a TM that bounds erf of the argument. erf(z) = (2/√π) ∫₀ᶻ e^{-t²} dt.

Equations

• tm.erf degree = { poly := 0, remainder := (LeanCert.Engine.TaylorModel.tmErf tm.bound degree).bound, center := tm.center, domain := tm.domain }

noncomputable def LeanCert.Engine.TaylorModel.log? (tm : TaylorModel) (degree : ℕ) : Option TaylorModel

Interval-based log composition. Given a TM for the argument, returns a TM that bounds log of the argument. Only valid when the argument interval is strictly positive. Returns none if the argument could be ≤ 0.

Equations

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

noncomputable def LeanCert.Engine.TaylorModel.sqrt? (tm : TaylorModel) : Option TaylorModel

Interval-based sqrt composition. Given a TM for the argument, returns a TM that bounds sqrt of the argument. Uses sqrtIntervalTight for the interval bound.

Equations

• tm.sqrt? = some { poly := 0, remainder := tm.bound.sqrtIntervalTight, center := tm.center, domain := tm.domain }

noncomputable def LeanCert.Engine.TaylorModel.atan? (tm : TaylorModel) : Option TaylorModel

Interval-based atan composition. Given a TM for the argument, returns a TM that bounds atan of the argument. Uses atanInterval for the interval bound (a conservative [-2, 2]).

Equations

• tm.atan? = some { poly := 0, remainder := LeanCert.Engine.atanInterval tm.bound, center := tm.center, domain := tm.domain }

noncomputable def LeanCert.Engine.TaylorModel.erf? (tm : TaylorModel) : Option TaylorModel

Interval-based erf composition. Given a TM for the argument, returns a TM that bounds erf of the argument. Uses erfInterval for the interval bound ([-1, 1]).

Equations

• tm.erf? = some { poly := 0, remainder := LeanCert.Engine.erfInterval tm.bound, center := tm.center, domain := tm.domain }

def LeanCert.Engine.TaylorModel.atanhSafe (I : Core.IntervalRat) : Bool

Check if an interval is safe for atanh: max(|lo|, |hi|) ≤ 99/100. This ensures we're away from the singularities at ±1.

Equations

• LeanCert.Engine.TaylorModel.atanhSafe I = decide (max |I.lo| |I.hi| ≤ 99 / 100)

theorem LeanCert.Engine.TaylorModel.abs_lt_one_of_atanhSafe {I : Core.IntervalRat} (hsafe : atanhSafe I = true) {z : ℝ} (hz : z ∈ I) : |z| < 1

If an interval is atanh-safe, any value in the interval has |z| < 1.

noncomputable def LeanCert.Engine.TaylorModel.atanh? (tm : TaylorModel) (degree : ℕ) : Option TaylorModel

Interval-based atanh composition with domain check. Given a TM for the argument, returns a TM that bounds atanh of the argument. Returns none if the argument bound could be too close to ±1.

Equations

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

Building Taylor models from Expr

noncomputable def LeanCert.Engine.TaylorModel.fromExpr (e : Core.Expr) (domain : Core.IntervalRat) (degree : ℕ) : TaylorModel

Convert an expression to a Taylor model (total builder used for examples).

Equations

• One or more equations did not get rendered due to their size.
• LeanCert.Engine.TaylorModel.fromExpr (LeanCert.Core.Expr.const q) domain degree = LeanCert.Engine.TaylorModel.const q domain
• LeanCert.Engine.TaylorModel.fromExpr (LeanCert.Core.Expr.var idx) domain degree = LeanCert.Engine.TaylorModel.identity domain
• LeanCert.Engine.TaylorModel.fromExpr (e₁.add e₂) domain degree = (LeanCert.Engine.TaylorModel.fromExpr e₁ domain degree).add (LeanCert.Engine.TaylorModel.fromExpr e₂ domain degree)
• LeanCert.Engine.TaylorModel.fromExpr (e₁.mul e₂) domain degree = (LeanCert.Engine.TaylorModel.fromExpr e₁ domain degree).mul (LeanCert.Engine.TaylorModel.fromExpr e₂ domain degree) degree
• LeanCert.Engine.TaylorModel.fromExpr e_2.neg domain degree = (LeanCert.Engine.TaylorModel.fromExpr e_2 domain degree).neg
• LeanCert.Engine.TaylorModel.fromExpr e_2.exp domain degree = (LeanCert.Engine.TaylorModel.fromExpr e_2 domain degree).exp degree
• LeanCert.Engine.TaylorModel.fromExpr e_2.sin domain degree = (LeanCert.Engine.TaylorModel.fromExpr e_2 domain degree).sin degree
• LeanCert.Engine.TaylorModel.fromExpr e_2.cos domain degree = (LeanCert.Engine.TaylorModel.fromExpr e_2 domain degree).cos degree
• LeanCert.Engine.TaylorModel.fromExpr e_2.atan domain degree = (LeanCert.Engine.TaylorModel.fromExpr e_2 domain degree).atan degree
• LeanCert.Engine.TaylorModel.fromExpr e_2.arsinh domain degree = (LeanCert.Engine.TaylorModel.fromExpr e_2 domain degree).asinh degree
• LeanCert.Engine.TaylorModel.fromExpr e_2.atanh domain degree = (LeanCert.Engine.TaylorModel.fromExpr e_2 domain degree).atanh degree
• LeanCert.Engine.TaylorModel.fromExpr e_2.sinc domain degree = (LeanCert.Engine.TaylorModel.fromExpr e_2 domain degree).sinc degree
• LeanCert.Engine.TaylorModel.fromExpr e_2.erf domain degree = (LeanCert.Engine.TaylorModel.fromExpr e_2 domain degree).erf degree
• LeanCert.Engine.TaylorModel.fromExpr e_2.sinh domain degree = (LeanCert.Engine.TaylorModel.fromExpr e_2 domain degree).sinh degree
• LeanCert.Engine.TaylorModel.fromExpr e_2.cosh domain degree = (LeanCert.Engine.TaylorModel.fromExpr e_2 domain degree).cosh degree
• LeanCert.Engine.TaylorModel.fromExpr e_2.tanh domain degree = (LeanCert.Engine.TaylorModel.fromExpr e_2 domain degree).tanh degree
• LeanCert.Engine.TaylorModel.fromExpr e_2.sqrt domain degree = (LeanCert.Engine.TaylorModel.fromExpr e_2 domain degree).sqrt?.getD (LeanCert.Engine.TaylorModel.const 0 domain)

noncomputable def LeanCert.Engine.TaylorModel.fromExpr? (e : Core.Expr) (domain : Core.IntervalRat) (degree : ℕ) : Option TaylorModel

Safe (partial) builder: convert an expression to a Taylor model, returning none if an inversion would require dividing by an interval that contains 0.

Equations

• One or more equations did not get rendered due to their size.
• LeanCert.Engine.TaylorModel.fromExpr? (LeanCert.Core.Expr.const q) domain degree = some (LeanCert.Engine.TaylorModel.const q domain)
• LeanCert.Engine.TaylorModel.fromExpr? (LeanCert.Core.Expr.var idx) domain degree = some (LeanCert.Engine.TaylorModel.identity domain)
• LeanCert.Engine.TaylorModel.fromExpr? e_2.neg domain degree = do let tm ← LeanCert.Engine.TaylorModel.fromExpr? e_2 domain degree pure tm.neg
• LeanCert.Engine.TaylorModel.fromExpr? e_2.inv domain degree = do let tm ← LeanCert.Engine.TaylorModel.fromExpr? e_2 domain degree if h : tm.bound.containsZero then none else pure (tm.inv h)
• LeanCert.Engine.TaylorModel.fromExpr? e_2.exp domain degree = do let tm ← LeanCert.Engine.TaylorModel.fromExpr? e_2 domain degree pure (tm.exp degree)
• LeanCert.Engine.TaylorModel.fromExpr? e_2.sin domain degree = do let tm ← LeanCert.Engine.TaylorModel.fromExpr? e_2 domain degree pure (tm.sin degree)
• LeanCert.Engine.TaylorModel.fromExpr? e_2.cos domain degree = do let tm ← LeanCert.Engine.TaylorModel.fromExpr? e_2 domain degree pure (tm.cos degree)
• LeanCert.Engine.TaylorModel.fromExpr? e_2.log domain degree = do let tm ← LeanCert.Engine.TaylorModel.fromExpr? e_2 domain degree tm.log? degree
• LeanCert.Engine.TaylorModel.fromExpr? e_2.atan domain degree = do let tm ← LeanCert.Engine.TaylorModel.fromExpr? e_2 domain degree tm.atan?
• LeanCert.Engine.TaylorModel.fromExpr? e_2.arsinh domain degree = do let tm ← LeanCert.Engine.TaylorModel.fromExpr? e_2 domain degree pure (tm.asinh degree)
• LeanCert.Engine.TaylorModel.fromExpr? e_2.atanh domain degree = do let tm ← LeanCert.Engine.TaylorModel.fromExpr? e_2 domain degree tm.atanh? degree
• LeanCert.Engine.TaylorModel.fromExpr? e_2.sinc domain degree = do let tm ← LeanCert.Engine.TaylorModel.fromExpr? e_2 domain degree pure (tm.sinc degree)
• LeanCert.Engine.TaylorModel.fromExpr? e_2.erf domain degree = do let tm ← LeanCert.Engine.TaylorModel.fromExpr? e_2 domain degree tm.erf?
• LeanCert.Engine.TaylorModel.fromExpr? e_2.sinh domain degree = do let tm ← LeanCert.Engine.TaylorModel.fromExpr? e_2 domain degree pure (tm.sinh degree)
• LeanCert.Engine.TaylorModel.fromExpr? e_2.cosh domain degree = do let tm ← LeanCert.Engine.TaylorModel.fromExpr? e_2 domain degree pure (tm.cosh degree)
• LeanCert.Engine.TaylorModel.fromExpr? e_2.tanh domain degree = do let tm ← LeanCert.Engine.TaylorModel.fromExpr? e_2 domain degree pure (tm.tanh degree)
• LeanCert.Engine.TaylorModel.fromExpr? e_2.sqrt domain degree = do let tm ← LeanCert.Engine.TaylorModel.fromExpr? e_2 domain degree tm.sqrt?
• LeanCert.Engine.TaylorModel.fromExpr? LeanCert.Core.Expr.pi domain degree = some { poly := 0, remainder := LeanCert.Engine.piInterval, center := domain.midpoint, domain := domain }

theorem LeanCert.Engine.fromExpr?_center (e : Core.Expr) (domain : Core.IntervalRat) (degree : ℕ) (tm : TaylorModel) (h : TaylorModel.fromExpr? e domain degree = some tm) : tm.center = domain.midpoint

Centers produced by fromExpr? are always domain.midpoint.

theorem LeanCert.Engine.TaylorModel.add_evalSet_correct (e1 e2 : Core.Expr) (domain : Core.IntervalRat) (tm1 tm2 : TaylorModel) (hcenter : tm1.center = tm2.center) (hf1 : ∀ x ∈ domain, Core.Expr.eval (fun (x_1 : ℕ) => x) e1 ∈ tm1.evalSet x) (hf2 : ∀ x ∈ domain, Core.Expr.eval (fun (x_1 : ℕ) => x) e2 ∈ tm2.evalSet x) (x : ℝ) : x ∈ domain → Core.Expr.eval (fun (x_1 : ℕ) => x) (e1.add e2) ∈ (tm1.add tm2).evalSet x

Composition lemma (addition): if sub-evaluations are in their evalSets, the sum is in the evalSet of the added TM (centers must match).

theorem LeanCert.Engine.TaylorModel.neg_evalSet_correct (e : Core.Expr) (domain : Core.IntervalRat) (tm : TaylorModel) (hf : ∀ x ∈ domain, Core.Expr.eval (fun (x_1 : ℕ) => x) e ∈ tm.evalSet x) (x : ℝ) : x ∈ domain → Core.Expr.eval (fun (x_1 : ℕ) => x) e.neg ∈ tm.neg.evalSet x

If e evaluates into tm.evalSet x on the domain, then -e evaluates into (neg tm).evalSet x on the domain.

Correctness of transcendental operations

theorem LeanCert.Engine.TaylorModel.sin_evalSet_correct (f : ℝ → ℝ) (tm : TaylorModel) (degree : ℕ) (hf : ∀ x ∈ tm.domain, f x ∈ tm.evalSet x) (x : ℝ) : x ∈ tm.domain → Real.sin (f x) ∈ (tm.sin degree).evalSet x

sin preserves evalSet membership.

theorem LeanCert.Engine.TaylorModel.cos_evalSet_correct (f : ℝ → ℝ) (tm : TaylorModel) (degree : ℕ) (hf : ∀ x ∈ tm.domain, f x ∈ tm.evalSet x) (x : ℝ) : x ∈ tm.domain → Real.cos (f x) ∈ (tm.cos degree).evalSet x

cos preserves evalSet membership.

theorem LeanCert.Engine.TaylorModel.exp_evalSet_correct (f : ℝ → ℝ) (tm : TaylorModel) (degree : ℕ) (hf : ∀ x ∈ tm.domain, f x ∈ tm.evalSet x) (x : ℝ) : x ∈ tm.domain → Real.exp (f x) ∈ (tm.exp degree).evalSet x

exp preserves evalSet membership.

theorem LeanCert.Engine.TaylorModel.sinh_evalSet_correct (f : ℝ → ℝ) (tm : TaylorModel) (degree : ℕ) (hf : ∀ x ∈ tm.domain, f x ∈ tm.evalSet x) (x : ℝ) : x ∈ tm.domain → Real.sinh (f x) ∈ (tm.sinh degree).evalSet x

sinh preserves evalSet membership.

theorem LeanCert.Engine.TaylorModel.cosh_evalSet_correct (f : ℝ → ℝ) (tm : TaylorModel) (degree : ℕ) (hf : ∀ x ∈ tm.domain, f x ∈ tm.evalSet x) (x : ℝ) : x ∈ tm.domain → Real.cosh (f x) ∈ (tm.cosh degree).evalSet x

cosh preserves evalSet membership.

theorem LeanCert.Engine.TaylorModel.asinh_evalSet_correct (f : ℝ → ℝ) (tm : TaylorModel) (degree : ℕ) (hf : ∀ x ∈ tm.domain, f x ∈ tm.evalSet x) (x : ℝ) : x ∈ tm.domain → Real.arsinh (f x) ∈ (tm.asinh degree).evalSet x

asinh preserves evalSet membership.

theorem LeanCert.Engine.TaylorModel.sinc_evalSet_correct (f : ℝ → ℝ) (tm : TaylorModel) (degree : ℕ) (hf : ∀ x ∈ tm.domain, f x ∈ tm.evalSet x) (x : ℝ) : x ∈ tm.domain → Real.sinc (f x) ∈ (tm.sinc degree).evalSet x

sinc preserves evalSet membership.

theorem LeanCert.Engine.TaylorModel.tanh_evalSet_correct (f : ℝ → ℝ) (tm : TaylorModel) (degree : ℕ) (hf : ∀ x ∈ tm.domain, f x ∈ tm.evalSet x) (x : ℝ) : x ∈ tm.domain → Real.tanh (f x) ∈ (tm.tanh degree).evalSet x

tanh preserves evalSet membership.

theorem LeanCert.Engine.TaylorModel.atanh_evalSet_correct' (f : ℝ → ℝ) (tm result : TaylorModel) (degree : ℕ) (hf : ∀ x ∈ tm.domain, f x ∈ tm.evalSet x) (hatanh : tm.atanh? degree = some result) (x : ℝ) : x ∈ tm.domain → Core.Real.atanh (f x) ∈ result.evalSet x

atanh preserves evalSet membership when atanh? succeeds.

Main fromExpr correctness

theorem LeanCert.Engine.fromExpr?_domain (e : Core.Expr) (domain : Core.IntervalRat) (degree : ℕ) (tm : TaylorModel) (h : TaylorModel.fromExpr? e domain degree = some tm) : tm.domain = domain

Helper: fromExpr? produces TaylorModels with matching domain.

theorem LeanCert.Engine.fromExpr_evalSet_correct (e : Core.Expr) (domain : Core.IntervalRat) (degree : ℕ) (tm : TaylorModel) (h : TaylorModel.fromExpr? e domain degree = some tm) (x : ℝ) : x ∈ domain → Core.Expr.eval (fun (x_1 : ℕ) => x) e ∈ tm.evalSet x

Core evalSet correctness: if fromExpr? succeeds, evaluation is in evalSet.

theorem LeanCert.Engine.fromExpr_correct (e : Core.Expr) (domain : Core.IntervalRat) (degree : ℕ) (tm : TaylorModel) (h : TaylorModel.fromExpr? e domain degree = some tm) (x : ℝ) : x ∈ domain → Core.Expr.eval (fun (x_1 : ℕ) => x) e ∈ tm.bound

fromExpr? produces correct Taylor models when it succeeds.

Refined exp interval using Taylor models

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

Refined interval bound for exp using Taylor models. For small intervals (width ≤ 1), uses degree-5 Taylor model which gives tight bounds. For larger intervals, falls back to the monotonicity-based coarse bound.

Equations

• LeanCert.Engine.expIntervalRefined I = if I.width ≤ 1 then (LeanCert.Engine.TaylorModel.tmExp I 5).bound else I.expInterval

theorem LeanCert.Engine.mem_expIntervalRefined {x : ℝ} {I : Core.IntervalRat} (hx : x ∈ I) : Real.exp x ∈ expIntervalRefined I

FTIA for refined exp: if x ∈ I, then exp(x) ∈ expIntervalRefined I