Semantic Lemmas for Interval Bounds #

This file provides semantic lemmas for deriving real bounds from certified interval enclosures. Tactics consume these lemmas, but the definitions belong to the engine layer so checked programmatic APIs do not depend on tactic modules.

Main theorems #

Core (computable) lemmas #

exprCore_le_of_interval_hi - Upper bound from interval high endpoint
exprCore_ge_of_interval_lo - Lower bound from interval low endpoint
exprCore_lt_of_interval_hi_lt - Strict upper bound
exprCore_gt_of_interval_lo_gt - Strict lower bound

Extended (noncomputable) lemmas #

expr_le_of_interval_hi - Upper bound from interval high endpoint
expr_ge_of_interval_lo - Lower bound from interval low endpoint
expr_lt_of_interval_hi_lt - Strict upper bound
expr_gt_of_interval_lo_gt - Strict lower bound
expr_le_of_mem_interval - Single-point variant
expr_ge_of_mem_interval - Single-point variant

Usage #

These lemmas are intended to be used by tactics like certify_bound and interval_decide to close goals of the form ∀ x ∈ I, f(x) ≤ c or similar.

The core lemmas use the computable evaluator and can work with native_decide. The extended lemmas use the noncomputable evaluator with floor/ceil bounds.

Tactic-facing lemmas for interval bounds (core, computable) #

source

theorem LeanCert.Engine.exprCore_le_of_interval_hi (e : Core.Expr) (hsupp : ExprSupportedCore e) (I : Core.IntervalRat) (c : ℚ) (cfg : EvalConfig := { }) (hdom : evalDomainValid1 e I cfg) (hhi : (Internal.Rational.evalTotalCore1 e I cfg).hi ≤ c) (x : ℝ) :

x ∈ I → Core.Expr.eval (fun (x_1 : ℕ) => x) e ≤ ↑c

Upper bound lemma for core expressions (computable). FULLY PROVED - no sorry, no axioms. Accepts configurable Taylor depth. Requires domain validity (e.g., log arguments must be positive).

source

theorem LeanCert.Engine.exprCore_ge_of_interval_lo (e : Core.Expr) (hsupp : ExprSupportedCore e) (I : Core.IntervalRat) (c : ℚ) (cfg : EvalConfig := { }) (hdom : evalDomainValid1 e I cfg) (hlo : c ≤ (Internal.Rational.evalTotalCore1 e I cfg).lo) (x : ℝ) :

x ∈ I → ↑c ≤ Core.Expr.eval (fun (x_1 : ℕ) => x) e

Lower bound lemma for core expressions (computable). FULLY PROVED - no sorry, no axioms. Accepts configurable Taylor depth. Requires domain validity (e.g., log arguments must be positive).

source

theorem LeanCert.Engine.exprCore_lt_of_interval_hi_lt (e : Core.Expr) (hsupp : ExprSupportedCore e) (I : Core.IntervalRat) (c : ℚ) (cfg : EvalConfig := { }) (hdom : evalDomainValid1 e I cfg) (hhi : (Internal.Rational.evalTotalCore1 e I cfg).hi < c) (x : ℝ) :

x ∈ I → Core.Expr.eval (fun (x_1 : ℕ) => x) e < ↑c

Strict upper bound for core expressions (computable). FULLY PROVED - no sorry, no axioms. Accepts configurable Taylor depth. Requires domain validity (e.g., log arguments must be positive).

source

theorem LeanCert.Engine.exprCore_gt_of_interval_lo_gt (e : Core.Expr) (hsupp : ExprSupportedCore e) (I : Core.IntervalRat) (c : ℚ) (cfg : EvalConfig := { }) (hdom : evalDomainValid1 e I cfg) (hlo : c < (Internal.Rational.evalTotalCore1 e I cfg).lo) (x : ℝ) :

x ∈ I → ↑c < Core.Expr.eval (fun (x_1 : ℕ) => x) e

Strict lower bound for core expressions (computable). FULLY PROVED - no sorry, no axioms. Accepts configurable Taylor depth. Requires domain validity (e.g., log arguments must be positive).