Tactic-Facing Lemmas for Interval Bounds

This file provides lemmas designed for use by tactics that verify bounds on expressions using interval arithmetic.

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 interval_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)

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 : (evalIntervalCore1 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).

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 ≤ (evalIntervalCore1 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).

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 : (evalIntervalCore1 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).

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 < (evalIntervalCore1 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).

Tactic-facing lemmas for interval bounds (extended, noncomputable)

theorem LeanCert.Engine.expr_le_of_interval_hi (e : Core.Expr) (hsupp : ExprSupported e) (I : Core.IntervalRat) (c : ℚ) (hhi : (evalInterval1 e I).hi ≤ c) (x : ℝ) : x ∈ I → Core.Expr.eval (fun (x_1 : ℕ) => x) e ≤ ↑c

Upper bound lemma for extended expressions. FULLY PROVED - no sorry, no axioms.

theorem LeanCert.Engine.expr_ge_of_interval_lo (e : Core.Expr) (hsupp : ExprSupported e) (I : Core.IntervalRat) (c : ℚ) (hlo : c ≤ (evalInterval1 e I).lo) (x : ℝ) : x ∈ I → ↑c ≤ Core.Expr.eval (fun (x_1 : ℕ) => x) e

Lower bound lemma for extended expressions. FULLY PROVED - no sorry, no axioms.

theorem LeanCert.Engine.expr_lt_of_interval_hi_lt (e : Core.Expr) (hsupp : ExprSupported e) (I : Core.IntervalRat) (c : ℚ) (hhi : (evalInterval1 e I).hi < c) (x : ℝ) : x ∈ I → Core.Expr.eval (fun (x_1 : ℕ) => x) e < ↑c

Strict upper bound for extended expressions. FULLY PROVED - no sorry, no axioms.

theorem LeanCert.Engine.expr_gt_of_interval_lo_gt (e : Core.Expr) (hsupp : ExprSupported e) (I : Core.IntervalRat) (c : ℚ) (hlo : c < (evalInterval1 e I).lo) (x : ℝ) : x ∈ I → ↑c < Core.Expr.eval (fun (x_1 : ℕ) => x) e

Strict lower bound for extended expressions. FULLY PROVED - no sorry, no axioms.

theorem LeanCert.Engine.expr_le_of_mem_interval (e : Core.Expr) (hsupp : ExprSupported e) (I : Core.IntervalRat) (c : ℚ) (x : ℝ) (hx : x ∈ I) (hhi : (evalInterval1 e I).hi ≤ c) : Core.Expr.eval (fun (x_1 : ℕ) => x) e ≤ ↑c

Variant for single point (extended).

theorem LeanCert.Engine.expr_ge_of_mem_interval (e : Core.Expr) (hsupp : ExprSupported e) (I : Core.IntervalRat) (c : ℚ) (x : ℝ) (hx : x ∈ I) (hlo : c ≤ (evalInterval1 e I).lo) : ↑c ≤ Core.Expr.eval (fun (x_1 : ℕ) => x) e

Variant for single point (extended).