Interval Evaluation of Expressions

This file re-exports the interval evaluation infrastructure for LeanCert.Core.Expr.

Module structure

The implementation is split across several files:

• LeanCert.Core.Support - Expression support predicates (ExprSupportedCore, ExprSupported, ExprSupportedWithInv)

• LeanCert.Engine.Eval.Core - Computable interval evaluator (evalIntervalCore) and transcendental interval bounds

• LeanCert.Engine.Eval.Extended - Noncomputable evaluator (evalInterval) and partial evaluator with inv/log support (evalInterval?)

• LeanCert.Tactic.Bound.Lemmas - Tactic-facing lemmas for proving bounds

Main definitions (re-exported)

Expression support predicates

• ExprSupportedCore - Computable subset (const, var, add, mul, neg, sin, cos, exp, sqrt, sinh, cosh, tanh, pi)
• ExprSupported - Noncomputable AD subset (const, var, add, mul, neg, sin, cos, exp)
• ExprSupportedWithInv - Syntactic support including inv and log

Evaluators

• evalIntervalCore - Computable interval evaluator (uses Taylor series)
• evalInterval - Noncomputable evaluator (uses floor/ceil for exp)
• evalInterval? - Partial evaluator with inv/log support

Correctness theorems

• evalIntervalCore_correct - Core evaluator correctness
• evalInterval_correct - Extended evaluator correctness
• evalInterval?_correct - Partial evaluator correctness

Tactic lemmas

• exprCore_le_of_interval_hi / exprCore_ge_of_interval_lo - Core bounds
• expr_le_of_interval_hi / expr_ge_of_interval_lo - Extended bounds

Design notes

The evaluators are split by computability:

• evalIntervalCore is COMPUTABLE, enabling native_decide in tactics
• evalInterval is NONCOMPUTABLE, using Real.exp with floor/ceil bounds
• Both are fully verified (no sorry, no axioms)