Smart Bounds with Monotonicity

This module provides monotonicity-aware bounds that use derivative information to get tighter bounds at interval endpoints. If the function is monotonic on the interval, we can evaluate at the appropriate endpoint to get an exact bound, avoiding Taylor series remainder widening.

Main definitions

Boolean Checkers

• checkLowerBoundSmart - Lower bound check using monotonicity
• checkUpperBoundSmart - Upper bound check using monotonicity

Monotonicity Helpers

• increasing_min_at_left_core - For increasing functions, minimum is at left endpoint
• decreasing_min_at_right_core - For decreasing functions, minimum is at right endpoint
• increasing_max_at_right_core - For increasing functions, maximum is at right endpoint
• decreasing_max_at_left_core - For decreasing functions, maximum is at left endpoint

Golden Theorems

• verify_lower_bound_smart - Smart lower bound verification
• verify_upper_bound_smart - Smart upper bound verification

Smart Bounds with Monotonicity

These checkers use derivative information to get tighter bounds at interval endpoints. If the function is monotonic on the interval, we can evaluate at the appropriate endpoint to get an exact bound, avoiding Taylor series remainder widening.

def LeanCert.Validity.checkLowerBoundSmart (e : Core.Expr) (I : Core.IntervalRat) (c : ℚ) (cfg : Engine.EvalConfig) : Bool

Smart lower bound check using monotonicity.

1. Tries standard interval check first (fastest).
2. If fails, computes derivative interval.
3. If derivative > 0 (increasing), checks if f(I.lo) ≥ c.
4. If derivative < 0 (decreasing), checks if f(I.hi) ≥ c.

Equations

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

def LeanCert.Validity.checkUpperBoundSmart (e : Core.Expr) (I : Core.IntervalRat) (c : ℚ) (cfg : Engine.EvalConfig) : Bool

Smart upper bound check using monotonicity.

1. Tries standard interval check first.
2. If fails, computes derivative interval.
3. If derivative > 0 (increasing), checks if f(I.hi) ≤ c.
4. If derivative < 0 (decreasing), checks if f(I.lo) ≤ c.

Equations

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

Monotonicity Helper Theorems

theorem LeanCert.Validity.increasing_min_at_left_core (e : Core.Expr) (hsupp : Core.ADSupported e) (I : Core.IntervalRat) (cfg : Engine.EvalConfig) (hpos : 0 < (Engine.derivIntervalCore e I cfg).lo) (x : ℝ) : x ∈ I → Core.Expr.eval (fun (x : ℕ) => ↑I.lo) e ≤ Core.Expr.eval (fun (x_1 : ℕ) => x) e

Helper: For increasing functions, the minimum is at the left endpoint

theorem LeanCert.Validity.decreasing_min_at_right_core (e : Core.Expr) (hsupp : Core.ADSupported e) (I : Core.IntervalRat) (cfg : Engine.EvalConfig) (hneg : (Engine.derivIntervalCore e I cfg).hi < 0) (x : ℝ) : x ∈ I → Core.Expr.eval (fun (x : ℕ) => ↑I.hi) e ≤ Core.Expr.eval (fun (x_1 : ℕ) => x) e

Helper: For decreasing functions, the minimum is at the right endpoint

theorem LeanCert.Validity.verify_lower_bound_smart (e : Core.Expr) (hsupp : Core.ADSupported e) (I : Core.IntervalRat) (c : ℚ) (cfg : Engine.EvalConfig) (h_cert : checkLowerBoundSmart e I c cfg = true) (x : ℝ) : x ∈ I → ↑c ≤ Core.Expr.eval (fun (x_1 : ℕ) => x) e

Smart lower bound verification using monotonicity

theorem LeanCert.Validity.increasing_max_at_right_core (e : Core.Expr) (hsupp : Core.ADSupported e) (I : Core.IntervalRat) (cfg : Engine.EvalConfig) (hpos : 0 < (Engine.derivIntervalCore e I cfg).lo) (x : ℝ) : x ∈ I → Core.Expr.eval (fun (x_1 : ℕ) => x) e ≤ Core.Expr.eval (fun (x : ℕ) => ↑I.hi) e

Helper: For increasing functions, the maximum is at the right endpoint

theorem LeanCert.Validity.decreasing_max_at_left_core (e : Core.Expr) (hsupp : Core.ADSupported e) (I : Core.IntervalRat) (cfg : Engine.EvalConfig) (hneg : (Engine.derivIntervalCore e I cfg).hi < 0) (x : ℝ) : x ∈ I → Core.Expr.eval (fun (x_1 : ℕ) => x) e ≤ Core.Expr.eval (fun (x : ℕ) => ↑I.lo) e

Helper: For decreasing functions, the maximum is at the left endpoint

theorem LeanCert.Validity.verify_upper_bound_smart (e : Core.Expr) (hsupp : Core.ADSupported e) (I : Core.IntervalRat) (c : ℚ) (cfg : Engine.EvalConfig) (h_cert : checkUpperBoundSmart e I c cfg = true) (x : ℝ) : x ∈ I → Core.Expr.eval (fun (x_1 : ℕ) => x) e ≤ ↑c

Smart upper bound verification using monotonicity