Documentation

LeanCert.Validity.Bounds.Bridge

Set.Icc Bridge Theorems and Subdivision #

This module provides bridge theorems between IntervalRat-based proofs and Set.Icc goals, as well as subdivision theorems for combining bounds from interval partitions.

Main definitions #

Set.Icc Bridge Theorems #

Subdivision Theorems #

General Split Theorems #

Set.Icc Bridge Theorems #

These theorems bridge between IntervalRat-based proofs and Set.Icc goals, allowing tactics to work with the more natural Set.Icc syntax.

source
theorem LeanCert.Validity.verify_upper_bound_Icc (e : Core.Expr) (hsupp : Core.ADSupported e) (lo hi : ℚ) (hle : lo ≤ hi) (c : ℚ) (cfg : Engine.EvalConfig) (h_cert : checkUpperBoundSmart e { lo := lo, hi := hi, le := hle } c cfg = true) (x : ℝ) :
x ∈ Set.Icc ↑lo ↑hi → Core.Expr.eval (fun (x_1 : ℕ) => x) e ≤ ↑c

Bridge from IntervalRat proof to Set.Icc upper bound goal

source
theorem LeanCert.Validity.verify_lower_bound_Icc (e : Core.Expr) (hsupp : Core.ADSupported e) (lo hi : ℚ) (hle : lo ≤ hi) (c : ℚ) (cfg : Engine.EvalConfig) (h_cert : checkLowerBoundSmart e { lo := lo, hi := hi, le := hle } c cfg = true) (x : ℝ) :
x ∈ Set.Icc ↑lo ↑hi → ↑c ≤ Core.Expr.eval (fun (x_1 : ℕ) => x) e

Bridge from IntervalRat proof to Set.Icc lower bound goal

source
theorem LeanCert.Validity.verify_upper_bound_Icc_core (e : Core.Expr) (hsupp : Core.ExprSupportedCore e) (lo hi : ℚ) (hle : lo ≤ hi) (c : ℚ) (cfg : Engine.EvalConfig) (h_cert : checkUpperBound e { lo := lo, hi := hi, le := hle } c cfg = true) (x : ℝ) :
x ∈ Set.Icc ↑lo ↑hi → Core.Expr.eval (fun (x_1 : ℕ) => x) e ≤ ↑c

Bridge from IntervalRat proof to Set.Icc upper bound goal (Core version). This version uses ExprSupportedCore and the basic checkUpperBound (no monotonicity).

source
theorem LeanCert.Validity.verify_lower_bound_Icc_core (e : Core.Expr) (hsupp : Core.ExprSupportedCore e) (lo hi : ℚ) (hle : lo ≤ hi) (c : ℚ) (cfg : Engine.EvalConfig) (h_cert : checkLowerBound e { lo := lo, hi := hi, le := hle } c cfg = true) (x : ℝ) :
x ∈ Set.Icc ↑lo ↑hi → ↑c ≤ Core.Expr.eval (fun (x_1 : ℕ) => x) e

Bridge from IntervalRat proof to Set.Icc lower bound goal (Core version). This version uses ExprSupportedCore and the basic checkLowerBound (no monotonicity).

source
theorem LeanCert.Validity.verify_strict_upper_bound_Icc_core (e : Core.Expr) (hsupp : Core.ExprSupportedCore e) (lo hi : ℚ) (hle : lo ≤ hi) (c : ℚ) (cfg : Engine.EvalConfig) (h_cert : checkStrictUpperBound e { lo := lo, hi := hi, le := hle } c cfg = true) (x : ℝ) :
x ∈ Set.Icc ↑lo ↑hi → Core.Expr.eval (fun (x_1 : ℕ) => x) e < ↑c

Bridge from IntervalRat proof to Set.Icc strict upper bound goal (Core version).

source
theorem LeanCert.Validity.verify_strict_lower_bound_Icc_core (e : Core.Expr) (hsupp : Core.ExprSupportedCore e) (lo hi : ℚ) (hle : lo ≤ hi) (c : ℚ) (cfg : Engine.EvalConfig) (h_cert : checkStrictLowerBound e { lo := lo, hi := hi, le := hle } c cfg = true) (x : ℝ) :
x ∈ Set.Icc ↑lo ↑hi → ↑c < Core.Expr.eval (fun (x_1 : ℕ) => x) e

Bridge from IntervalRat proof to Set.Icc strict lower bound goal (Core version).

Subdivision Theorems #

These theorems allow combining bounds from interval subdivisions. When interval arithmetic gives overly wide bounds, subdividing the domain and proving bounds on each piece can help.

source
theorem LeanCert.Validity.verify_upper_bound_split (e : Core.Expr) (hsupp : Core.ExprSupportedCore e) (I : Core.IntervalRat) (c : ℚ) (cfg : Engine.EvalConfig) (h_left : checkUpperBound e (Engine.splitMid I).1 c cfg = true) (h_right : checkUpperBound e (Engine.splitMid I).2 c cfg = true) (x : ℝ) :
x ∈ I → Core.Expr.eval (fun (x_1 : ℕ) => x) e ≤ ↑c

Combine upper bounds from two halves using splitMid. If f ≤ c on both halves, then f ≤ c on the whole interval.

source
theorem LeanCert.Validity.verify_lower_bound_split (e : Core.Expr) (hsupp : Core.ExprSupportedCore e) (I : Core.IntervalRat) (c : ℚ) (cfg : Engine.EvalConfig) (h_left : checkLowerBound e (Engine.splitMid I).1 c cfg = true) (h_right : checkLowerBound e (Engine.splitMid I).2 c cfg = true) (x : ℝ) :
x ∈ I → ↑c ≤ Core.Expr.eval (fun (x_1 : ℕ) => x) e

Combine lower bounds from two halves using splitMid.

source
theorem LeanCert.Validity.verify_strict_upper_bound_split (e : Core.Expr) (hsupp : Core.ExprSupportedCore e) (I : Core.IntervalRat) (c : ℚ) (cfg : Engine.EvalConfig) (h_left : checkStrictUpperBound e (Engine.splitMid I).1 c cfg = true) (h_right : checkStrictUpperBound e (Engine.splitMid I).2 c cfg = true) (x : ℝ) :
x ∈ I → Core.Expr.eval (fun (x_1 : ℕ) => x) e < ↑c

Combine strict upper bounds from two halves.

source
theorem LeanCert.Validity.verify_strict_lower_bound_split (e : Core.Expr) (hsupp : Core.ExprSupportedCore e) (I : Core.IntervalRat) (c : ℚ) (cfg : Engine.EvalConfig) (h_left : checkStrictLowerBound e (Engine.splitMid I).1 c cfg = true) (h_right : checkStrictLowerBound e (Engine.splitMid I).2 c cfg = true) (x : ℝ) :
x ∈ I → ↑c < Core.Expr.eval (fun (x_1 : ℕ) => x) e

Combine strict lower bounds from two halves.

source
theorem LeanCert.Validity.verify_upper_bound_Icc_split (e : Core.Expr) (hsupp : Core.ExprSupportedCore e) (lo hi : ℚ) (hle : lo ≤ hi) (c : ℚ) (cfg : Engine.EvalConfig) (h_left : checkUpperBound e (Engine.splitMid { lo := lo, hi := hi, le := hle }).1 c cfg = true) (h_right : checkUpperBound e (Engine.splitMid { lo := lo, hi := hi, le := hle }).2 c cfg = true) (x : ℝ) :
x ∈ Set.Icc ↑lo ↑hi → Core.Expr.eval (fun (x_1 : ℕ) => x) e ≤ ↑c

Bridge from subdivision to Set.Icc upper bound goal.

source
theorem LeanCert.Validity.verify_lower_bound_Icc_split (e : Core.Expr) (hsupp : Core.ExprSupportedCore e) (lo hi : ℚ) (hle : lo ≤ hi) (c : ℚ) (cfg : Engine.EvalConfig) (h_left : checkLowerBound e (Engine.splitMid { lo := lo, hi := hi, le := hle }).1 c cfg = true) (h_right : checkLowerBound e (Engine.splitMid { lo := lo, hi := hi, le := hle }).2 c cfg = true) (x : ℝ) :
x ∈ Set.Icc ↑lo ↑hi → ↑c ≤ Core.Expr.eval (fun (x_1 : ℕ) => x) e

Bridge from subdivision to Set.Icc lower bound goal.

source
theorem LeanCert.Validity.verify_strict_upper_bound_Icc_split (e : Core.Expr) (hsupp : Core.ExprSupportedCore e) (lo hi : ℚ) (hle : lo ≤ hi) (c : ℚ) (cfg : Engine.EvalConfig) (h_left : checkStrictUpperBound e (Engine.splitMid { lo := lo, hi := hi, le := hle }).1 c cfg = true) (h_right : checkStrictUpperBound e (Engine.splitMid { lo := lo, hi := hi, le := hle }).2 c cfg = true) (x : ℝ) :
x ∈ Set.Icc ↑lo ↑hi → Core.Expr.eval (fun (x_1 : ℕ) => x) e < ↑c

Bridge from subdivision to Set.Icc strict upper bound goal.

source
theorem LeanCert.Validity.verify_strict_lower_bound_Icc_split (e : Core.Expr) (hsupp : Core.ExprSupportedCore e) (lo hi : ℚ) (hle : lo ≤ hi) (c : ℚ) (cfg : Engine.EvalConfig) (h_left : checkStrictLowerBound e (Engine.splitMid { lo := lo, hi := hi, le := hle }).1 c cfg = true) (h_right : checkStrictLowerBound e (Engine.splitMid { lo := lo, hi := hi, le := hle }).2 c cfg = true) (x : ℝ) :
x ∈ Set.Icc ↑lo ↑hi → ↑c < Core.Expr.eval (fun (x_1 : ℕ) => x) e

Bridge from subdivision to Set.Icc strict lower bound goal.

General Split Theorems #

These theorems work with arbitrary split points, not just midpoints. Useful for adaptive subdivision algorithms.

source
theorem LeanCert.Validity.mem_split_general {lo mid hi : ℚ} {x : ℝ} (hx : x ∈ Set.Icc ↑lo ↑hi) (_hLeMid : lo ≤ mid) (_hMidLe : mid ≤ hi) :
x ∈ Set.Icc ↑lo ↑mid ∨ x ∈ Set.Icc ↑mid ↑hi

Any x in [lo, hi] is in [lo, mid] or [mid, hi] for any mid in between

source
theorem LeanCert.Validity.combine_upper_bound_general_split (e : Core.Expr) (lo mid hi c : ℚ) (hLo : lo ≤ mid) (hHi : mid ≤ hi) (h_left : ∀ x ∈ Set.Icc ↑lo ↑mid, Core.Expr.eval (fun (x_1 : ℕ) => x) e ≤ ↑c) (h_right : ∀ x ∈ Set.Icc ↑mid ↑hi, Core.Expr.eval (fun (x_1 : ℕ) => x) e ≤ ↑c) (x : ℝ) :
x ∈ Set.Icc ↑lo ↑hi → Core.Expr.eval (fun (x_1 : ℕ) => x) e ≤ ↑c

Combine already-certified upper bounds on adjacent intervals. Unlike the checker-specific theorem below, this supports recursive subdivision proofs.

source
theorem LeanCert.Validity.combine_lower_bound_general_split (e : Core.Expr) (lo mid hi c : ℚ) (hLo : lo ≤ mid) (hHi : mid ≤ hi) (h_left : ∀ x ∈ Set.Icc ↑lo ↑mid, ↑c ≤ Core.Expr.eval (fun (x_1 : ℕ) => x) e) (h_right : ∀ x ∈ Set.Icc ↑mid ↑hi, ↑c ≤ Core.Expr.eval (fun (x_1 : ℕ) => x) e) (x : ℝ) :
x ∈ Set.Icc ↑lo ↑hi → ↑c ≤ Core.Expr.eval (fun (x_1 : ℕ) => x) e

Combine already-certified lower bounds on adjacent intervals.

source
theorem LeanCert.Validity.combine_strict_upper_bound_general_split (e : Core.Expr) (lo mid hi c : ℚ) (hLo : lo ≤ mid) (hHi : mid ≤ hi) (h_left : ∀ x ∈ Set.Icc ↑lo ↑mid, Core.Expr.eval (fun (x_1 : ℕ) => x) e < ↑c) (h_right : ∀ x ∈ Set.Icc ↑mid ↑hi, Core.Expr.eval (fun (x_1 : ℕ) => x) e < ↑c) (x : ℝ) :
x ∈ Set.Icc ↑lo ↑hi → Core.Expr.eval (fun (x_1 : ℕ) => x) e < ↑c

Combine already-certified strict upper bounds on adjacent intervals.

source
theorem LeanCert.Validity.combine_strict_lower_bound_general_split (e : Core.Expr) (lo mid hi c : ℚ) (hLo : lo ≤ mid) (hHi : mid ≤ hi) (h_left : ∀ x ∈ Set.Icc ↑lo ↑mid, ↑c < Core.Expr.eval (fun (x_1 : ℕ) => x) e) (h_right : ∀ x ∈ Set.Icc ↑mid ↑hi, ↑c < Core.Expr.eval (fun (x_1 : ℕ) => x) e) (x : ℝ) :
x ∈ Set.Icc ↑lo ↑hi → ↑c < Core.Expr.eval (fun (x_1 : ℕ) => x) e

Combine already-certified strict lower bounds on adjacent intervals.

source
theorem LeanCert.Validity.verify_upper_bound_general_split (e : Core.Expr) (hsupp : Core.ExprSupportedCore e) (lo mid hi : ℚ) (hLo : lo ≤ mid) (hHi : mid ≤ hi) (_hle : lo ≤ hi) (c : ℚ) (cfg : Engine.EvalConfig) (h_left : checkUpperBound e { lo := lo, hi := mid, le := hLo } c cfg = true) (h_right : checkUpperBound e { lo := mid, hi := hi, le := hHi } c cfg = true) (x : ℝ) :
x ∈ Set.Icc ↑lo ↑hi → Core.Expr.eval (fun (x_1 : ℕ) => x) e ≤ ↑c

Combine upper bounds from two arbitrary adjacent intervals. If f ≤ c on [lo, mid] and f ≤ c on [mid, hi], then f ≤ c on [lo, hi].

source
theorem LeanCert.Validity.verify_lower_bound_general_split (e : Core.Expr) (hsupp : Core.ExprSupportedCore e) (lo mid hi : ℚ) (hLo : lo ≤ mid) (hHi : mid ≤ hi) (_hle : lo ≤ hi) (c : ℚ) (cfg : Engine.EvalConfig) (h_left : checkLowerBound e { lo := lo, hi := mid, le := hLo } c cfg = true) (h_right : checkLowerBound e { lo := mid, hi := hi, le := hHi } c cfg = true) (x : ℝ) :
x ∈ Set.Icc ↑lo ↑hi → ↑c ≤ Core.Expr.eval (fun (x_1 : ℕ) => x) e

Combine lower bounds from two arbitrary adjacent intervals.

source
theorem LeanCert.Validity.verify_strict_upper_bound_general_split (e : Core.Expr) (hsupp : Core.ExprSupportedCore e) (lo mid hi : ℚ) (hLo : lo ≤ mid) (hHi : mid ≤ hi) (_hle : lo ≤ hi) (c : ℚ) (cfg : Engine.EvalConfig) (h_left : checkStrictUpperBound e { lo := lo, hi := mid, le := hLo } c cfg = true) (h_right : checkStrictUpperBound e { lo := mid, hi := hi, le := hHi } c cfg = true) (x : ℝ) :
x ∈ Set.Icc ↑lo ↑hi → Core.Expr.eval (fun (x_1 : ℕ) => x) e < ↑c

Combine strict upper bounds from two arbitrary adjacent intervals.

source
theorem LeanCert.Validity.verify_strict_lower_bound_general_split (e : Core.Expr) (hsupp : Core.ExprSupportedCore e) (lo mid hi : ℚ) (hLo : lo ≤ mid) (hHi : mid ≤ hi) (_hle : lo ≤ hi) (c : ℚ) (cfg : Engine.EvalConfig) (h_left : checkStrictLowerBound e { lo := lo, hi := mid, le := hLo } c cfg = true) (h_right : checkStrictLowerBound e { lo := mid, hi := hi, le := hHi } c cfg = true) (x : ℝ) :
x ∈ Set.Icc ↑lo ↑hi → ↑c < Core.Expr.eval (fun (x_1 : ℕ) => x) e

Combine strict lower bounds from two arbitrary adjacent intervals.