Moving sofa: related mathematical developments #
LeanCert.Contrib.Sinc.LeanCert.Core.DerivativeIntervals.LeanCert.Core.Dyadic.LeanCert.Core.Expr.LeanCert.Core.Interval.LeanCert.Core.IntervalRat.Basic.LeanCert.Core.IntervalRat.LogReduction.LeanCert.Core.IntervalRat.Transcendental.LeanCert.Core.Support.LeanCert.Core.Taylor.LeanCert.Core.IntervalRat.Taylor.LeanCert.Core.IntervalReal.LeanCert.Core.IntervalDyadic.LeanCert.Core.IntervalRealEndpoints.LeanCert.Core.TrigReduction.LeanCert.Core.IntervalRat.TrigReduced.LeanCert.Engine.Eval.Core.LeanCert.Engine.Eval.Result.LeanCert.Engine.Eval.Extended.LeanCert.Engine.Bounds.Lemmas.LeanCert.Engine.IntervalEval.LeanCert.Engine.AD.Basic.LeanCert.Engine.AD.Transcendental.LeanCert.Engine.AD.Eval.LeanCert.Engine.AD.Correctness.LeanCert.Engine.AD.Computable.LeanCert.Engine.AD.DomainChecked.
Differentiability of sinc and dslope #
This file proves that the sinc function is differentiable everywhere, including at 0.
Main results #
Real.differentiableAt_sinc: sinc is differentiable at every pointReal.hasDerivAt_sinc_zero: sinc has derivative 0 at x = 0
Mathematical background #
The sinc function is defined as:
Equivalently, sinc = dslope sin 0.
The derivative of sinc at 0 can be computed using Taylor expansion:
The derivative of sinc at 0 is 0.
The proof uses the squeeze theorem with the bound |sinc x - 1| ≤ |x|² / 4,
which follows from sin bounds in Mathlib.
sinc is differentiable everywhere.
Integral representation and smoothness of sinc #
The sinc function is smooth (C^∞). The key insight is the integral representation: sinc(x) = ∫ t in 0..1, cos(t * x) dt
This works because:
- For x ≠ 0: ∫₀¹ cos(tx) dt = [sin(tx)/x]₀¹ = sin(x)/x = sinc(x)
- For x = 0: ∫₀¹ cos(0) dt = ∫₀¹ 1 dt = 1 = sinc(0)
Smoothness follows from differentiation under the integral sign (Leibniz rule): since cos(t*x) is C^∞ in x and the domain [0,1] is compact, the integral is C^∞.
The derivative of sinc equals dslope (cos - sinc) at 0.
For x ≠ 0: dslope (cos - sinc) 0 x = (cos x - sinc x) / x = (x cos x - sin x) / x² = deriv sinc x
For x = 0: dslope (cos - sinc) 0 0 = deriv (cos - sinc) 0 = -sin 0 - deriv sinc 0 = 0 = deriv sinc 0
sinc is smooth at every nonzero point.
sinc is analytic at 0.
The proof uses the order theory of analytic functions. Since sin is analytic at 0 with order ≥ 1 (because sin(0) = 0), there exists an analytic function g such that sin(z) = z • g(z) near 0. This g must equal sinc away from 0, and by continuity of both functions at 0, g = sinc everywhere near 0. Therefore sinc is analytic at 0.
Derivative Interval Library #
This file provides a systematic collection of derivative interval facts for basic functions. These lemmas establish that derivatives of common functions lie within specified intervals, which feeds into:
- Monotonicity analysis
- Lipschitz/contractivity bounds
- Newton method analysis
- Global optimization pruning
Main theorems #
Exp (derivative = exp, always positive) #
exp_deriv_pos- exp' x > 0 for all xexp_deriv_interval- exp' x ∈ [exp a, exp b] for x ∈ [a, b]
Log (derivative = 1/x on (0, ∞)) #
log_deriv_interval- log' x ∈ [1/b, 1/a] for x ∈ [a, b] with 0 < a
Arctan (derivative = 1/(1+x²) ∈ (0, 1]) #
arctan_deriv_interval- arctan' x ∈ (0, 1] for all xarctan_deriv_mem_Icc- arctan' x ∈ [0, 1] for all x
Arsinh (derivative = 1/√(1+x²) ∈ (0, 1]) #
arsinh_deriv_interval- arsinh' x ∈ (0, 1] for all xarsinh_deriv_mem_Icc- arsinh' x ∈ [0, 1] for all x
Sin/Cos (derivatives bounded by 1) #
sin_deriv_interval- |sin' x| = |cos x| ≤ 1cos_deriv_interval- |cos' x| = |sin x| ≤ 1
Sinh/Cosh (derivative relationships) #
sinh_deriv_eq_cosh- sinh' = coshcosh_deriv_eq_sinh- cosh' = sinhcosh_deriv_interval- cosh' x = sinh x, monotonicity facts
Design notes #
These lemmas are independent of any specific algorithm; they're just facts about functions. They're designed to be composable with the chain rule for AD correctness proofs.
Exp derivative intervals #
exp is strictly increasing (follows from positive derivative)
Log derivative intervals #
log is strictly increasing on (0, ∞)
Arctan derivative intervals #
The derivative of arctan at x is 1/(1+x²)
1/(1+x²) is always positive
1/(1+x²) ≤ 1 for all x
arctan' x ∈ (0, 1] for all x
arctan' x ∈ [0, 1] for all x (closed interval version for interval arithmetic)
arctan is strictly increasing (follows from positive derivative)
Arsinh derivative intervals #
The derivative of arsinh at x is (√(1+x²))⁻¹
arsinh' x > 0 for all x
arsinh' x ≤ 1 for all x
arsinh' x ∈ (0, 1] for all x
arsinh' x ∈ [0, 1] for all x (closed interval version)
arsinh is strictly increasing
Sin derivative intervals #
Cos derivative intervals #
Sinh derivative intervals #
sinh is strictly increasing
Cosh derivative intervals #
cosh' 0 = sinh 0 = 0
cosh is strictly decreasing on (-∞, 0]
cosh is strictly increasing on [0, ∞)
One-Sided Taylor Bounds #
For convex functions, the Taylor polynomial provides a one-sided bound. For exp on [0, ∞), the n-th Taylor polynomial is a lower bound. For concave functions, similar upper bounds hold.
These bounds are tighter than symmetric remainder bounds at endpoints, which is important for verified numerics.
Exp lower bounds (convexity gives Taylor poly ≤ function) #
Monotonicity from derivative bounds #
These wrap the Mathlib lemmas for convenience with our naming.
If f' ≥ 0 on [a, b], then f is monotone increasing on [a, b]
If f' > 0 on (a, b), then f is strictly monotone on [a, b]
If f' ≤ 0 on [a, b], then f is antitone (monotone decreasing) on [a, b]
If f' < 0 on (a, b), then f is strictly antitone on [a, b]
Dyadic Rationals (n * 2^e) #
This file defines Dyadic rationals, which are the backbone of high-performance
verified numerics. Unlike arbitrary Rat, Dyadics do not require GCD
normalization, making them significantly faster for kernel evaluation.
Main definitions #
Dyadic- A dyadic rational number:mantissa * 2^exponentDyadic.toRat- Convert to standard rationalDyadic.add,Dyadic.mul,Dyadic.neg- Arithmetic operationsDyadic.shiftDown,Dyadic.shiftUp- Directed rounding for interval bounds
Design notes #
Dyadics use power-of-2 multiplications instead of GCD-based normalization.
This makes them orders of magnitude faster for kernel evaluation via
native_decide, since 2^n can be computed by simple bit operations.
For interval arithmetic, we use directed rounding:
This ensures mathematical soundness even when truncating precision.
Equations
- LeanCert.Core.instReprDyadic = { reprPrec := LeanCert.Core.instReprDyadic.repr }
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
Helper: Power of 2 #
Compute 2^n for natural n
Equations
Instances For
Shift an integer left by n bits (multiply by 2^n)
Equations
Instances For
Shift an integer right by n bits (divide by 2^n, floor toward -∞)
Equations
Instances For
Check if any of the low n bits are set
Equations
- LeanCert.Core.Dyadic.hasLowBits m n = decide (m % ↑(LeanCert.Core.Dyadic.pow2Nat n) ≠ 0)
Instances For
Conversion to Rat #
Equations
Equations
Equations
A lawful identity key for caches, sets, serialization, and deduplication.
Arithmetic keeps the fast, noncanonical Dyadic representation. Converting at
an identity boundary collapses all representations of the same rational value.
- value : ℚ
The exact rational value used to compare normalized dyadic numbers.
Instances For
Equations
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
Instances For
Equations
- LeanCert.Core.Dyadic.instBEqCanonicalKey.beq { value := a } { value := b } = (a == b)
- LeanCert.Core.Dyadic.instBEqCanonicalKey.beq x✝¹ x✝ = false
Instances For
Instances For
Convert a dyadic value to its canonical identity key.
Equations
- d.canonicalKey = { value := d.toRat }
Instances For
Canonical keys agree exactly when represented dyadic values agree.
Equations
Construction #
Create a dyadic from an integer (exponent = 0)
Equations
- LeanCert.Core.Dyadic.ofInt i = { mantissa := i, exponent := 0 }
Instances For
Create a dyadic for 2^n
Equations
- LeanCert.Core.Dyadic.pow2 n = { mantissa := 1, exponent := n }
Instances For
Equations
Equations
Arithmetic Operations #
Equations
Addition of Dyadics. Aligns exponents by shifting the mantissa with larger exponent to match the smaller one.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
Equations
Equations
Directed Rounding for Interval Arithmetic #
Shift a dyadic to a new (larger) exponent with "Down" rounding (for lower bounds).
If newExp > d.exponent, we lose precision by right-shifting the mantissa.
Bits are discarded (floor division toward -∞).
Equations
Instances For
Shift a dyadic to a new (larger) exponent with "Up" rounding (for upper bounds).
If newExp > d.exponent, we lose precision by right-shifting the mantissa.
If any bits are lost, we add 1 to ensure upward rounding (ceiling toward +∞).
Equations
- One or more equations did not get rendered due to their size.
Instances For
Normalization (Mantissa Control) #
Get the bit length of the absolute value of an integer
Instances For
Normalize a Dyadic to keep the mantissa within a reasonable bit-limit.
This prevents mantissas from growing without bound during repeated multiplications. Similar to how hardware floats work, but with directed rounding.
maxBits: Maximum allowed bits for mantissa (default 256)roundUp: If true, round toward +∞; if false, round toward -∞
Equations
- One or more equations did not get rendered due to their size.
Instances For
Normalize for lower bounds (round down)
Equations
- d.normalizeDown maxBits = d.normalize maxBits
Instances For
Normalize for upper bounds (round up)
Equations
- d.normalizeUp maxBits = d.normalize maxBits true
Instances For
Comparison #
Compare two Dyadics (decidable)
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- LeanCert.Core.Dyadic.instOrd = { compare := LeanCert.Core.Dyadic.compare }
Equations
- LeanCert.Core.Dyadic.instLE = { le := fun (d₁ d₂ : LeanCert.Core.Dyadic) => d₁.le d₂ = true }
Equations
- LeanCert.Core.Dyadic.instLT = { lt := fun (d₁ d₂ : LeanCert.Core.Dyadic) => d₁.lt d₂ = true }
Correctness Theorems #
Helper lemmas for shift proofs #
Arithmetic Homomorphisms #
Rounding Properties #
Comparison Helper Lemmas #
Comparison Theorems #
compare reflects toRat ordering: lt case
compare reflects toRat ordering: gt case
compare reflects toRat ordering: eq case
Min/Max Lemmas #
Normalize Lemmas #
normalizeDown produces value ≤ original
normalizeUp produces value ≥ original
Scale2 Lemmas #
Square Root Operations #
Integer square root of a natural number.
Satisfies: (intSqrtNat n)^2 ≤ n < (intSqrtNat n + 1)^2
Equations
Instances For
Integer square root of a non-negative integer. Returns 0 for negative inputs.
Equations
Instances For
Compute sqrt(d) with a target exponent prec.
Returns a Dyadic with exponent prec such that result ≤ sqrt(d).
For d = m * 2^e, we compute:
- shift = e - 2*prec (to align for sqrt)
- m' = m * 2^shift (or m / 2^(-shift) if shift < 0)
- result = floor(sqrt(m')) * 2^prec
This ensures: result.toRat ≤ sqrt(d.toRat)
Equations
- One or more equations did not get rendered due to their size.
Instances For
Compute sqrt(d) rounded up with target exponent prec.
Returns a Dyadic with exponent prec such that result ≥ sqrt(d).
Uses the same computation as sqrtDown, but if the result is not a perfect square, adds 1 to round up.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Sqrt Correctness Theorems #
Unified Expression AST #
This file defines the unified AST for real expressions (Expr) and its
evaluation semantics. All numerical algorithms in LeanCert operate on this
single expression type.
Main definitions #
LeanCert.Core.Expr- The expression AST supporting algebraic and transcendental operationsLeanCert.Core.Expr.eval- Evaluation of expressions given a variable assignment
Design notes #
The expression type uses natural number indices for variables. This simplifies the interval evaluation and automatic differentiation implementations.
Auxiliary definition for atanh #
Since Mathlib doesn't provide Real.atanh, we define it here using the
standard formula: atanh x = (1/2) * log((1+x)/(1-x)) for |x| < 1.
atanh is strictly monotone on (-1, 1)
The error function: erf(x) = (2/√π) ∫₀ˣ exp(-t²) dt. Essential for statistical and financial modeling (normal distribution CDF). Uses interval integral notation (∫ t in 0..x) which handles negative x correctly.
Instances For
The error function is bounded above by 1.
The error function is bounded below by -1.
Named mathematical constants with known interval bounds. Adding a new constant (e.g., Catalan's) only requires extending this enum and its lookup tables — zero evaluator files need updating.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
Equations
The real value of a named mathematical constant.
Equations
Instances For
Float approximation for heuristic evaluation (unverified).
Equations
- LeanCert.Core.MathConst.pi.toFloat = 3.141592653589793
- LeanCert.Core.MathConst.eulerMascheroni.toFloat = 0.5772156649015329
Instances For
Rational approximation for display/debugging (unverified).
Equations
- LeanCert.Core.MathConst.pi.toRatApprox = 157 / 50
- LeanCert.Core.MathConst.eulerMascheroni.toRatApprox = 577 / 1000
Instances For
Unified AST for real-valued expressions.
- const
(q : ℚ)
: Expr
Rational constant
- var
(idx : ℕ)
: Expr
Variable with de Bruijn-style index
- add
(e₁ e₂ : Expr)
: Expr
Addition
- mul
(e₁ e₂ : Expr)
: Expr
Multiplication
- neg
(e : Expr)
: Expr
Negation
- inv
(e : Expr)
: Expr
Multiplicative inverse (partial: undefined at 0)
- exp
(e : Expr)
: Expr
Exponential function
- sin
(e : Expr)
: Expr
Sine function
- cos
(e : Expr)
: Expr
Cosine function
- log
(e : Expr)
: Expr
Natural logarithm (partial: undefined for x ≤ 0)
- atan
(e : Expr)
: Expr
Arctangent function
- arsinh
(e : Expr)
: Expr
Inverse hyperbolic sine (arsinh)
- atanh
(e : Expr)
: Expr
Inverse hyperbolic tangent (partial: undefined for |x| ≥ 1)
- sinc
(e : Expr)
: Expr
Sinc function: sinc(x) = sin(x)/x for x ≠ 0, sinc(0) = 1
- erf
(e : Expr)
: Expr
Error function: erf(x) = (2/√π) ∫₀ˣ exp(-t²) dt
- sinh
(e : Expr)
: Expr
Hyperbolic sine: sinh(x) = (exp(x) - exp(-x)) / 2
- cosh
(e : Expr)
: Expr
Hyperbolic cosine: cosh(x) = (exp(x) + exp(-x)) / 2
- tanh
(e : Expr)
: Expr
Hyperbolic tangent: tanh(x) = sinh(x) / cosh(x) ∈ (-1, 1)
- sqrt
(e : Expr)
: Expr
Square root (partial: undefined for x < 0)
- namedConst
(c : MathConst)
: Expr
A named mathematical constant (π, γ, …) looked up from a table.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- LeanCert.Core.instReprExpr = { reprPrec := LeanCert.Core.instReprExpr.repr }
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
Evaluate an expression given a variable assignment ρ : Nat → ℝ
Equations
- LeanCert.Core.Expr.eval ρ (LeanCert.Core.Expr.const q) = ↑q
- LeanCert.Core.Expr.eval ρ (LeanCert.Core.Expr.var idx) = ρ idx
- LeanCert.Core.Expr.eval ρ (e₁.add e₂) = LeanCert.Core.Expr.eval ρ e₁ + LeanCert.Core.Expr.eval ρ e₂
- LeanCert.Core.Expr.eval ρ (e₁.mul e₂) = LeanCert.Core.Expr.eval ρ e₁ * LeanCert.Core.Expr.eval ρ e₂
- LeanCert.Core.Expr.eval ρ e.neg = -LeanCert.Core.Expr.eval ρ e
- LeanCert.Core.Expr.eval ρ e.inv = (LeanCert.Core.Expr.eval ρ e)⁻¹
- LeanCert.Core.Expr.eval ρ e.exp = Real.exp (LeanCert.Core.Expr.eval ρ e)
- LeanCert.Core.Expr.eval ρ e.sin = Real.sin (LeanCert.Core.Expr.eval ρ e)
- LeanCert.Core.Expr.eval ρ e.cos = Real.cos (LeanCert.Core.Expr.eval ρ e)
- LeanCert.Core.Expr.eval ρ e.log = Real.log (LeanCert.Core.Expr.eval ρ e)
- LeanCert.Core.Expr.eval ρ e.atan = Real.arctan (LeanCert.Core.Expr.eval ρ e)
- LeanCert.Core.Expr.eval ρ e.arsinh = Real.arsinh (LeanCert.Core.Expr.eval ρ e)
- LeanCert.Core.Expr.eval ρ e.atanh = LeanCert.Core.Real.atanh (LeanCert.Core.Expr.eval ρ e)
- LeanCert.Core.Expr.eval ρ e.sinc = Real.sinc (LeanCert.Core.Expr.eval ρ e)
- LeanCert.Core.Expr.eval ρ e.erf = LeanCert.Core.Real.erf (LeanCert.Core.Expr.eval ρ e)
- LeanCert.Core.Expr.eval ρ e.sinh = Real.sinh (LeanCert.Core.Expr.eval ρ e)
- LeanCert.Core.Expr.eval ρ e.cosh = Real.cosh (LeanCert.Core.Expr.eval ρ e)
- LeanCert.Core.Expr.eval ρ e.tanh = Real.tanh (LeanCert.Core.Expr.eval ρ e)
- LeanCert.Core.Expr.eval ρ e.sqrt = √(LeanCert.Core.Expr.eval ρ e)
- LeanCert.Core.Expr.eval ρ (LeanCert.Core.Expr.namedConst c) = c.toReal
Instances For
Notation for replacing one coordinate of a variable environment.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Evaluate e as a scalar function of variable idx, with all other
variables fixed by ρ. This represents the map t ↦ eval ρ[idx ↦ t] e.
Instances For
The set of free variable indices in an expression
Equations
- (LeanCert.Core.Expr.const q).freeVars = ∅
- (LeanCert.Core.Expr.var idx).freeVars = {idx}
- (e₁.add e₂).freeVars = e₁.freeVars ∪ e₂.freeVars
- (e₁.mul e₂).freeVars = e₁.freeVars ∪ e₂.freeVars
- e.neg.freeVars = e.freeVars
- e.inv.freeVars = e.freeVars
- e.exp.freeVars = e.freeVars
- e.sin.freeVars = e.freeVars
- e.cos.freeVars = e.freeVars
- e.log.freeVars = e.freeVars
- e.atan.freeVars = e.freeVars
- e.arsinh.freeVars = e.freeVars
- e.atanh.freeVars = e.freeVars
- e.sinc.freeVars = e.freeVars
- e.erf.freeVars = e.freeVars
- e.sinh.freeVars = e.freeVars
- e.cosh.freeVars = e.freeVars
- e.tanh.freeVars = e.freeVars
- e.sqrt.freeVars = e.freeVars
- (LeanCert.Core.Expr.namedConst c).freeVars = ∅
Instances For
√(x * x) = |x| — LeanCert-namespaced alias of Real.sqrt_mul_self_eq_abs.
Single-variable expressions #
For 1D optimization and root finding, we often work with expressions that only use variable 0. These lemmas establish that such expressions can be evaluated equivalently with different environment representations.
Check if an expression only uses variable 0 (computable)
Equations
- (LeanCert.Core.Expr.const q).usesOnlyVar0 = true
- (LeanCert.Core.Expr.var idx).usesOnlyVar0 = (idx == 0)
- (e₁.add e₂).usesOnlyVar0 = (e₁.usesOnlyVar0 && e₂.usesOnlyVar0)
- (e₁.mul e₂).usesOnlyVar0 = (e₁.usesOnlyVar0 && e₂.usesOnlyVar0)
- e.neg.usesOnlyVar0 = e.usesOnlyVar0
- e.inv.usesOnlyVar0 = e.usesOnlyVar0
- e.exp.usesOnlyVar0 = e.usesOnlyVar0
- e.sin.usesOnlyVar0 = e.usesOnlyVar0
- e.cos.usesOnlyVar0 = e.usesOnlyVar0
- e.log.usesOnlyVar0 = e.usesOnlyVar0
- e.atan.usesOnlyVar0 = e.usesOnlyVar0
- e.arsinh.usesOnlyVar0 = e.usesOnlyVar0
- e.atanh.usesOnlyVar0 = e.usesOnlyVar0
- e.sinc.usesOnlyVar0 = e.usesOnlyVar0
- e.erf.usesOnlyVar0 = e.usesOnlyVar0
- e.sinh.usesOnlyVar0 = e.usesOnlyVar0
- e.cosh.usesOnlyVar0 = e.usesOnlyVar0
- e.tanh.usesOnlyVar0 = e.usesOnlyVar0
- e.sqrt.usesOnlyVar0 = e.usesOnlyVar0
- (LeanCert.Core.Expr.namedConst c).usesOnlyVar0 = true
Instances For
Abstract Interval Interface #
This file defines the abstract notion of intervals as subsets of ℝ,
with semantic properties. This provides the mathematical foundation
that IntervalReal will implement computationally.
Main definitions #
- Lemmas about
Set.Icc(closed intervals) relevant to interval arithmetic - Convexity and integrability properties
Design notes #
We primarily use Set.Icc a b from Mathlib as our semantic interval type.
This file collects lemmas and abstractions useful for verified numerics.
Interval membership and operations #
A real number is in the interval [a, b]
Equations
- LeanCert.Core.memIcc x a b = (a ≤ x ∧ x ≤ b)
Instances For
Interval arithmetic semantics #
These lemmas establish the semantic foundation for interval arithmetic: if x ∈ [a, b] and y ∈ [c, d], then x ⊕ y ∈ [a ⊕ c, b ⊕ d] (for appropriate ⊕).
Convexity #
Compactness #
Nonempty closed bounded intervals are compact
Continuous functions on intervals #
Rational Endpoint Intervals - Core Definitions #
This file defines IntervalRat, a concrete interval type with rational endpoints
suitable for computation. We prove the Fundamental Theorem of Interval Arithmetic
(FTIA) for each operation.
Main definitions #
LeanCert.Core.IntervalRat- Intervals with rational endpointsLeanCert.Core.IntervalRat.toSet- Semantic interpretation as a subset of ℝ- Operations:
add,neg,sub,mul,inv,div
Main theorems #
mem_add- FTIA for additionmem_neg- FTIA for negationmem_sub- FTIA for subtractionmem_mul- FTIA for multiplication
Design notes #
All operations maintain the invariant lo ≤ hi. Domain restrictions for partial
operations (like inv) are encoded via separate types or explicit hypotheses.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
Equations
- One or more equations did not get rendered due to their size.
Instances For
Default interval [0, 0] for unsupported expression branches
Equations
- LeanCert.Core.instInhabitedIntervalRat = { default := { lo := 0, hi := 0, le := LeanCert.Core.instInhabitedIntervalRat._proof_1 } }
The set of reals contained in this interval
Instances For
Membership in an interval
Membership in IntervalRat is the same as membership in Set.Icc
Universal quantifier over IntervalRat equals universal over Set.Icc
Existence in IntervalRat equals existence in Set.Icc
Create an interval from a single rational
Equations
- LeanCert.Core.IntervalRat.singleton q = { lo := q, hi := q, le := ⋯ }
Instances For
The width of an interval
Instances For
Midpoint of an interval
Instances For
The midpoint of an interval is contained in the interval
Interval addition #
Add two intervals
Instances For
FTIA for addition
Interval negation #
Negate an interval
Instances For
FTIA for negation
Interval subtraction #
Subtract two intervals
Instances For
FTIA for subtraction
Interval multiplication #
Helper: minimum of four rationals
Equations
- LeanCert.Core.IntervalRat.min4 a b c d = min (min a b) (min c d)
Instances For
Helper: maximum of four rationals
Equations
- LeanCert.Core.IntervalRat.max4 a b c d = max (max a b) (max c d)
Instances For
Multiply two intervals
Equations
- One or more equations did not get rendered due to their size.
Instances For
Fast interval multiplication using sign-based case splitting. Reduces from 4 multiplications + 12 comparisons to 2 multiplications in the common case (both intervals positive or both negative). Falls back to the full 4-way product for mixed-sign intervals.
Equations
- One or more equations did not get rendered due to their size.
Instances For
FTIA for multiplication
mulFast preserves the containment property of mul.
This is retained as documentation and a future audited optimization hook;
production certificate checking currently uses mul directly.
Interval containing zero check #
Check if an interval contains zero
Instances For
Decidable containsZero
Interval inversion (for nonzero intervals) #
Invert an interval that doesn't contain zero
Equations
Instances For
FTIA for inversion #
Scalar operations #
Scale an interval by a rational
Equations
Instances For
FTIA for scaling
Interval splitting #
Split an interval at its midpoint
Equations
Instances For
Midpoint is at least lo
Midpoint is at most hi
Midpoint is at least lo (real version)
Midpoint is at most hi (real version)
Left bisection is a subset of the original interval
Right bisection is a subset of the original interval
Any point in an interval is in one of its bisected halves
Interval intersection #
If intersection succeeds, the result contains any point in both intervals
Verified Argument Reduction for Logarithm #
This file provides argument reduction for computing log(q) using the identity: log(q) = log(m) + k * log(2) where m = q * 2^(-k) is in a "good" range [1/2, 2] for Taylor series convergence.
Main definitions #
reductionExponent- Find k such that q * 2^(-k) is in [1/2, 2]reduceMantissa- The reduced mantissa m = q * 2^(-k)
Main theorems #
reconstruction_eq- Algebraic identity: q = m * 2^kreduced_bounds- Bounds on m: 1 / 2 ≤ m ≤ 2 for q > 0
Design notes #
This reduction allows us to use the rapidly converging atanh-based series: log(m) = 2 * atanh((m-1)/(m+1)) For m ∈ [1/2, 2], we have (m-1)/(m+1) ∈ [-1/3, 1/3], where atanh converges very fast.
Argument Reduction #
Find k such that q * 2^(-k) is approximately in [1/2, 2]. Implementation: k = log2(num) - log2(den) approximately.
Equations
Instances For
The reduced mantissa m = q * 2^(-k).
Equations
- LeanCert.Core.LogReduction.reduceMantissa q = if q ≤ 0 then 1 else have k := LeanCert.Core.LogReduction.reductionExponent q; q * 2 ^ (-k)
Instances For
The main algebraic theorem: q = m * 2^k for positive q
The reduced mantissa is bounded: 1/4 ≤ m ≤ 4 for q > 0. (We use slightly weaker bounds than [1/2, 2] for simpler proofs, but the series still converges rapidly.)
Tighter bounds: 1 / 2 ≤ m ≤ 2 for most q > 0
The reduced mantissa is positive for positive input
Connection to Real.log #
Key algebraic identity for Real.log: log(q) = log(m) + k * log(2)
Rational Endpoint Intervals - Transcendental Functions #
This file provides noncomputable interval bounds for transcendental functions using floor/ceiling to obtain rational endpoints.
Main definitions #
ofRealEndpoints- Create rational interval from real bounds using floor/ceilexpInterval- Interval bound for exponentiallogInterval- Interval bound for logarithm (positive intervals)atanhIntervalComputed- Interval bound for atanh (intervals in (-1, 1))sqrtInterval- Interval bound for square root
Main theorems #
mem_expInterval- FTIA for expmem_logInterval- FTIA for logmem_atanhIntervalComputed- FTIA for atanhmem_sqrtInterval- FTIA for sqrt
Design notes #
All definitions in this file are noncomputable as they use Real.exp, Real.log,
etc. For computable versions, see IntervalRat.Taylor.
Rational enclosure of real intervals #
Coarse rational enclosure of a real interval using floor/ceil. Given a real interval [lo, hi], returns a rational interval [⌊lo⌋, ⌈hi⌉] that is guaranteed to contain all points in the original interval.
Equations
Instances For
Exponential interval #
Interval bound for exp on rational intervals. Since exp is strictly increasing, exp([a,b]) ⊆ [⌊exp(a)⌋, ⌈exp(b)⌉]. This uses Real.exp and floor/ceil to get rational bounds.
Equations
- I.expInterval = LeanCert.Core.IntervalRat.ofRealEndpoints (Real.exp ↑I.lo) (Real.exp ↑I.hi) ⋯
Instances For
FTIA for exp: if x ∈ I, then exp(x) ∈ expInterval(I)
Positive interval check #
Decidable isPositive
Logarithm interval (for positive intervals) #
Interval bound for log on positive rational intervals. Since log is strictly increasing on (0, ∞), log([a,b]) ⊆ [⌊log(a)⌋, ⌈log(b)⌉] for a > 0. This uses Real.log and floor/ceil to get rational bounds.
Equations
Instances For
FTIA for log: if x ∈ I with lo > 0, then log(x) ∈ logInterval(I)
Atanh interval (for intervals in (-1, 1)) #
Convert to standard interval
Instances For
Membership in the underlying interval
Interval bound for atanh on intervals strictly inside (-1, 1). Since atanh is strictly increasing on (-1, 1), atanh([a,b]) ⊆ [⌊atanh(a)⌋, ⌈atanh(b)⌉].
Equations
Instances For
FTIA for atanh: if x ∈ I and I ⊂ (-1, 1), then atanh(x) ∈ atanhIntervalComputed(I)
Square Root Interval #
Integer square root (floor of sqrt).
Satisfies: (intSqrtNat n)^2 ≤ n < (intSqrtNat n + 1)^2
Equations
Instances For
Rational lower bound for sqrt. For q ≥ 0 with q = num/den, we compute floor(sqrt(num * den)) / den. This gives: sqrtRatLower q ≤ sqrt(q).
The idea: sqrt(num/den) = sqrt(num*den)/den when properly scaled.
Equations
Instances For
Rational upper bound for sqrt. For q ≥ 0, we compute ceil(sqrt(num * den)) / den. This gives: sqrt(q) ≤ sqrtRatUpper q.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Scaling exponent for precise sqrt bounds (2^scaleBits = scaling factor for denominator)
Equations
Instances For
Rational lower bound for sqrt with high precision. For q ≥ 0, we scale by 4^k, compute integer sqrt, and scale back by 2^k. This gives: sqrtRatLowerPrec q ≤ sqrt(q) with precision ~2^(-k).
Equations
- One or more equations did not get rendered due to their size.
Instances For
Rational upper bound for sqrt with high precision. For q ≥ 0, we scale by 4^k, compute ceil of integer sqrt, and scale back by 2^k. This gives: sqrt(q) ≤ sqrtRatUpperPrec q with precision ~2^(-k).
Equations
- One or more equations did not get rendered due to their size.
Instances For
Soundness of sqrtRatLower: sqrtRatLower q ≤ Real.sqrt q for q ≥ 0
Soundness of sqrtRatUpper: Real.sqrt q ≤ sqrtRatUpper q for q ≥ 0
Square root interval with conservative bounds. For a non-negative interval [lo, hi], sqrt is monotone so: sqrt([lo, hi]) ⊆ [0, max(hi, 1)]
The lower bound is 0 (always sound for sqrt). The upper bound uses max(hi, 1) which satisfies sqrt(x) ≤ max(x, 1) for x ≥ 0.
Instances For
Improved square root interval with tight lower bounds. For a non-negative interval [lo, hi] with lo ≥ 0:
- Lower bound: sqrtRatLower(lo)
- Upper bound: sqrtRatUpper(hi)
For intervals crossing zero, we use 0 as lower bound.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Soundness of sqrtRatLowerPrec: sqrtRatLowerPrec q k ≤ Real.sqrt q for q ≥ 0
Soundness of sqrtRatUpperPrec: Real.sqrt q ≤ sqrtRatUpperPrec q k for q ≥ 0
High-precision square root interval. For a non-negative interval [lo, hi] with lo ≥ 0:
- Lower bound: sqrtRatLowerPrec(lo)
- Upper bound: sqrtRatUpperPrec(hi)
Uses scaling to achieve ~6 decimal digits of precision.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Membership theorem for sqrtIntervalTightPrec
Soundness of sqrt interval: if x ∈ I and x ≥ 0, then sqrt(x) ∈ sqrtInterval I
General soundness of sqrt interval: works for any x ∈ I (including negative). When x < 0, Real.sqrt x = 0, which is always in [0, max(hi, 1)].
Soundness of tight sqrt interval: if x ∈ I and x ≥ 0, then sqrt(x) ∈ sqrtIntervalTight I
General soundness of tight sqrt interval: works for any x ∈ I (including negative). When x < 0, Real.sqrt x = 0, which is always in the result interval.
Expression Support Predicates #
This file defines predicates indicating which expressions are supported by different interval evaluation strategies.
Main definitions #
ExprSupportedCore- Predicate for expressions in the computable subset (const, var, add, mul, neg, sin, cos, exp, log, sqrt, sinh, cosh, tanh, erf, pi)ADSupported- Predicate for the noncomputable AD subset (const, var, add, mul, neg, sin, cos, exp)
Design notes #
ADSupported is the differentiable fragment used by automatic
differentiation. It is contained in ExprSupportedCore via
ADSupported.toCore. Checked evaluators accept arbitrary expressions and
encode domain failure in their result type, so they need no syntactic support
predicate.
The core subset is kept computable so that tactics can use native_decide
for interval bound checking. The extended subset uses Real.exp with
floor/ceil bounds, which requires noncomputability.
Core supported expression subset (computable) #
Predicate indicating an expression is in the computable core subset. Supports: const, var, add, mul, neg, sin, cos, exp, log, sqrt, sinh, cosh, tanh, erf, pi
Note: log requires positive domain for correctness. The correctness theorem
evalIntervalCore_correct has an additional hypothesis evalDomainValid
that ensures log arguments evaluate to positive intervals.
- const (q : ℚ) : ExprSupportedCore (Expr.const q)
- var (idx : ℕ) : ExprSupportedCore (Expr.var idx)
- add {e₁ e₂ : Expr} : ExprSupportedCore e₁ → ExprSupportedCore e₂ → ExprSupportedCore (e₁.add e₂)
- mul {e₁ e₂ : Expr} : ExprSupportedCore e₁ → ExprSupportedCore e₂ → ExprSupportedCore (e₁.mul e₂)
- neg {e : Expr} : ExprSupportedCore e → ExprSupportedCore e.neg
- sin {e : Expr} : ExprSupportedCore e → ExprSupportedCore e.sin
- cos {e : Expr} : ExprSupportedCore e → ExprSupportedCore e.cos
- exp {e : Expr} : ExprSupportedCore e → ExprSupportedCore e.exp
- log {e : Expr} : ExprSupportedCore e → ExprSupportedCore e.log
- sqrt {e : Expr} : ExprSupportedCore e → ExprSupportedCore e.sqrt
- sinh {e : Expr} : ExprSupportedCore e → ExprSupportedCore e.sinh
- cosh {e : Expr} : ExprSupportedCore e → ExprSupportedCore e.cosh
- tanh {e : Expr} : ExprSupportedCore e → ExprSupportedCore e.tanh
- erf {e : Expr} : ExprSupportedCore e → ExprSupportedCore e.erf
- namedConst (c : MathConst) : ExprSupportedCore (Expr.namedConst c)
Instances For
Extended supported expression subset (with exp) #
Predicate indicating an expression is in the fully-verified subset for AD. Supports: const, var, add, mul, neg, sin, cos, exp Does NOT support:
- sqrt (not differentiable at 0 - use ExprSupportedCore for interval evaluation only)
- inv (requires nonzero interval checks)
- log (requires positive interval checks)
- atan/arsinh/atanh (derivative proofs incomplete in the total AD evaluator)
- const (q : ℚ) : ADSupported (Expr.const q)
- var (idx : ℕ) : ADSupported (Expr.var idx)
- add {e₁ e₂ : Expr} : ADSupported e₁ → ADSupported e₂ → ADSupported (e₁.add e₂)
- mul {e₁ e₂ : Expr} : ADSupported e₁ → ADSupported e₂ → ADSupported (e₁.mul e₂)
- neg {e : Expr} : ADSupported e → ADSupported e.neg
- sin {e : Expr} : ADSupported e → ADSupported e.sin
- cos {e : Expr} : ADSupported e → ADSupported e.cos
- exp {e : Expr} : ADSupported e → ADSupported e.exp
Instances For
ADSupported expressions are also in ExprSupportedCore
Computable recognition of the differentiable ADSupported subset used
by Newton/AD backends.
Equations
- (LeanCert.Core.Expr.const q).checkADSupported = true
- (LeanCert.Core.Expr.var idx).checkADSupported = true
- (e₁.add e₂).checkADSupported = (e₁.checkADSupported && e₂.checkADSupported)
- (e₁.mul e₂).checkADSupported = (e₁.checkADSupported && e₂.checkADSupported)
- e.neg.checkADSupported = e.checkADSupported
- e.exp.checkADSupported = e.checkADSupported
- e.sin.checkADSupported = e.checkADSupported
- e.cos.checkADSupported = e.checkADSupported
- x✝.checkADSupported = false
Instances For
The executable support check recognizes exactly the differentiable
ADSupported fragment used by the checked AD/monotonicity backend.
Computable recognition of ExprSupportedCore.
Equations
- (LeanCert.Core.Expr.const q).checkSupportedCore = true
- (LeanCert.Core.Expr.var idx).checkSupportedCore = true
- (LeanCert.Core.Expr.namedConst c).checkSupportedCore = true
- (e₁.add e₂).checkSupportedCore = (e₁.checkSupportedCore && e₂.checkSupportedCore)
- (e₁.mul e₂).checkSupportedCore = (e₁.checkSupportedCore && e₂.checkSupportedCore)
- e.neg.checkSupportedCore = e.checkSupportedCore
- e.exp.checkSupportedCore = e.checkSupportedCore
- e.sin.checkSupportedCore = e.checkSupportedCore
- e.cos.checkSupportedCore = e.checkSupportedCore
- e.log.checkSupportedCore = e.checkSupportedCore
- e.sqrt.checkSupportedCore = e.checkSupportedCore
- e.sinh.checkSupportedCore = e.checkSupportedCore
- e.cosh.checkSupportedCore = e.checkSupportedCore
- e.tanh.checkSupportedCore = e.checkSupportedCore
- e.erf.checkSupportedCore = e.checkSupportedCore
- x✝.checkSupportedCore = false
Instances For
A successful computable core-support check produces the corresponding proof object required by the tight Rational evaluator theorem.
Generic Taylor Series Abstractions #
This file provides generic Taylor series machinery for verified numerics. We wrap Mathlib's Taylor expansion theorems in forms convenient for our interval arithmetic framework.
Phase Status #
This module is now Phase 3 complete. The main Taylor remainder bound theorem
taylor_remainder_bound is fully proved with no sorry markers.
The theorem provides rigorous bounds on Taylor polynomial approximation errors using Lagrange's form of the remainder.
Main definitions #
TaylorApprox- A Taylor approximation with explicit remainder bounds- Generic theorems for composing Taylor approximations
Design notes #
This file provides the abstract theory. Specific Taylor expansions for
exp, sin, cos, etc. are built using this machinery in conjunction
with Mathlib's calculus lemmas.
Taylor approximation structure #
A Taylor approximation of a function on an interval.
Given a function f, center c, and radius r, this represents:
- A polynomial approximation
polyof degreen - A remainder bound
Rsuch that for allxwith|x - c| ≤ r:|f(x) - poly(x - c)| ≤ R
- degree : ℕ
Degree of the polynomial
Polynomial coefficients (Taylor coefficients at center)
- remainder : ℚ
Remainder bound
The remainder is non-negative
Instances For
Derivative bounds #
Taylor remainder bounds #
Helper lemmas for iteratedDerivWithin conversion #
Unique differentiability at the left endpoint of a closed interval.
Unique differentiability at the right endpoint of a closed interval.
At the left endpoint of [c, x], derivWithin equals deriv for differentiable functions.
At the right endpoint of [c, x], derivWithin equals deriv for differentiable functions.
Helper lemma: iteratedDerivWithin on Icc a b equals iteratedDeriv at interior points.
This bridges Mathlib's iteratedDerivWithin-based Taylor theorems with global iteratedDeriv.
At the left endpoint of [c, x], iteratedDerivWithin equals iteratedDeriv for functions that are ContDiffOn on an open set containing c.
This is useful for functions like log that are only smooth on (0, ∞).
Taylor remainder bound for c < x case with ContDiffOn hypothesis.
For functions that are ContDiffOn on an open set containing [a, b], this provides the same Lagrange remainder bound as the global ContDiff version.
Key lemma for reflection: derivatives of g(t) = f(2c - t) when f is smooth on an open set.
This is a local version of iteratedDeriv_reflect that works with ContDiffOn on an open set
rather than global ContDiff.
Taylor remainder bound for x < c case with ContDiffOn hypothesis.
For functions that are ContDiffOn on an open set containing [a, b], this provides the same Lagrange remainder bound as the global ContDiff version.
The proof uses reflection: define g(t) = f(2c - t), apply Lagrange to g on [c, 2c-x], then convert back.
Combined Taylor remainder bound with ContDiffOn hypothesis.
For functions that are ContDiffOn on an open set containing [a, b], this provides the Lagrange remainder bound for any x ∈ [a, b] and center c ∈ [a, b].
Key lemma: derivatives of reflected function g(t) = f(2c - t).
For the x < c case, we use reflection: define g(t) = f(2c - t), apply Lagrange
to g on [c, 2c-x], then convert back. This lemma shows how g's derivatives
relate to f's derivatives.
Taylor remainder bound for c < x case (Lagrange form).
For c < x, we apply taylor_mean_remainder_lagrange on [c, x] and convert
iteratedDerivWithin to iteratedDeriv using the helper lemmas above.
Taylor remainder bound for x < c case (Lagrange form via reflection).
For x < c, we define g(t) = f(2c - t), apply taylor_mean_remainder_lagrange on [c, 2c-x],
then use iteratedDeriv_reflect to convert back to f's derivatives. The key insight is that
g's Taylor expansion at c, evaluated at 2c-x, equals f's Taylor expansion at c, evaluated at x,
because the (-1)^i factors from the derivatives cancel with the (-1)^i factors from the powers.
Lagrange form remainder bound for Taylor approximation.
If |f^(n)(x)| ≤ M for all x in [a, b], and c ∈ [a, b], then the Taylor polynomial
of degree n-1 (sum over range n) satisfies: for any x ∈ [a, b]:
|f(x) - T_{n-1}(x; c)| ≤ M * |x - c|^n / n!
Note: The sum ∑ i ∈ Finset.range n gives terms 0..n-1 (degree n-1 polynomial).
The remainder involves the n-th derivative, matching our bound on iteratedDeriv n f.
All cases are fully proved:
- Case n = 0: Direct bound. ✓
- Case n > 0, x = c: Trivial (both sides zero). ✓
- Case n > 0, c < x: Via
taylor_remainder_bound_c_lt_x. ✓ - Case n > 0, x < c: Via
taylor_remainder_bound_x_lt_c(reflection). ✓
Common Taylor expansions #
Taylor coefficients for exp at 0: 1/n!
Equations
- LeanCert.Core.expTaylorCoeff n = 1 / ↑n.factorial
Instances For
Derivative bounds for common functions #
All derivatives of sin and cos are bounded by 1. The derivatives cycle: sin → cos → -sin → -cos → sin → ...
All derivatives of sinh and cosh are bounded by exp(max(|a|, |b|)) on [a, b]. The derivatives cycle: sinh → cosh → sinh → cosh → ...
Rational Endpoint Intervals - Computable Taylor Series #
This file provides computable interval enclosures for transcendental functions using Taylor series with rational coefficients and rigorous remainder bounds.
Main definitions #
ratFactorial- Compute n! as a rationalpow- Compute interval powerabsInterval,maxAbs- Absolute value helpersevalTaylorSeries- Evaluate Taylor polynomial on an intervalexpComputable,sinComputable,cosComputable- Computable transcendental functionssinhComputable,coshComputable- Computable hyperbolic functions
Main theorems #
mem_pow- FTIA for interval powermem_evalTaylorSeries- General FTIA for Taylor seriesmem_expComputable,mem_sinComputable,mem_cosComputable- FTIA for computable functions
Design notes #
All definitions in this file use only rational arithmetic and are fully computable. The proofs connect these to the real-valued functions via Taylor's theorem.
Computable Taylor series helpers #
Compute n! as a Rational
Equations
Instances For
Compute the integer power of an interval using exponentiation by squaring. O(log n) interval multiplications instead of O(n).
Equations
Instances For
Compute the absolute value interval: |I| = [0, max(|lo|, |hi|)] if 0 ∈ I, or [min(|lo|,|hi|), max(|lo|,|hi|)] otherwise
Equations
Instances For
Evaluate Taylor series ∑_{i=0}^{n} c_i * x^i at interval I using Horner's method. Computes c₀ + I * (c₁ + I * (c₂ + ... + I * cₙ)), which is mathematically equivalent to the direct sum but uses fewer operations and often gives tighter bounds by reducing the dependency problem in interval arithmetic.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Computable exp via Taylor series #
Tail-recursive exp coefficient generator.
expTaylorCoeffsAux n k c produces n+1 coefficients starting at index k,
assuming c = 1 / k!.
Equations
- LeanCert.Core.IntervalRat.expTaylorCoeffsAux 0 x✝¹ x✝ = [x✝]
- LeanCert.Core.IntervalRat.expTaylorCoeffsAux n.succ x✝¹ x✝ = x✝ :: LeanCert.Core.IntervalRat.expTaylorCoeffsAux n (x✝¹ + 1) (x✝ / (↑x✝¹ + 1))
Instances For
Taylor coefficients for exp: 1/i! for i = 0, 1, ..., n. Implemented iteratively to avoid repeated factorial recomputation.
Equations
Instances For
Computable exp remainder bound using rational arithmetic. The Lagrange remainder is exp(ξ) * x^{n+1} / (n+1)! where ξ is between 0 and x. We use e < 3, so e^r ≤ 3^(⌈r⌉+1) as a conservative bound.
Returns an interval [-R, R] where R bounds the remainder.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The raw rational Taylor enclosure of the exponential at a point.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Heuristic reduction factor for exp evaluation.
We choose k = log2(ceil(|q|) + 1), so 2^k grows roughly with |q|.
No correctness depends on the specific choice; it only affects performance.
Instances For
Computable interval enclosure for exp at a single rational point.
Uses argument reduction: exp(q) = exp(q/2^k)^(2^k).
Equations
- One or more equations did not get rendered due to their size.
Instances For
Point exponential using Taylor coefficients prepared for depth n.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Hull of two intervals: smallest interval containing both.
Instances For
Membership in hull
Computable interval enclosure for exp using Taylor series with monotonicity optimization.
exp(x) = ∑_{i=0}^{n} x^i/i! + R where |R| ≤ exp(|x|) * |x|^{n+1} / (n+1)!
For intervals not crossing 0, we use endpoint evaluation and take the hull, which is tighter than direct Taylor evaluation due to interval widening.
This is fully computable using only rational arithmetic.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Interval exponential using Taylor coefficients prepared for depth n.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Computable sin via Taylor series #
Taylor coefficients for sin: 0, 1, 0, -1/6, 0, 1/120, ...
Equations
Instances For
Computable sin remainder bound. Since |sin^{(k)}(x)| ≤ 1 for all k, x, the remainder is bounded by |x|^{n+1}/(n+1)!
Equations
- One or more equations did not get rendered due to their size.
Instances For
Computable interval enclosure for sin using Taylor series.
sin(x) = ∑_{k=0}^{n/2} (-1)^k x^{2k+1}/(2k+1)! + R where |R| ≤ |x|^{n+1}/(n+1)! since all derivatives of sin are bounded by 1.
We intersect with [-1, 1] for tighter bounds on small intervals.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Interval sine using Taylor coefficients prepared for depth n.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Computable cos via Taylor series #
Taylor coefficients for cos: 1, 0, -1/2, 0, 1/24, 0, ...
Equations
- LeanCert.Core.IntervalRat.cosTaylorCoeffs n = List.map (fun (i : ℕ) => if i % 2 = 0 then (-1) ^ (i / 2) / LeanCert.Core.IntervalRat.ratFactorial i else 0) (List.range (n + 1))
Instances For
Computable cos remainder bound. Since |cos^{(k)}(x)| ≤ 1 for all k, x, the remainder is bounded by |x|^{n+1}/(n+1)!
Equations
- One or more equations did not get rendered due to their size.
Instances For
Computable interval enclosure for cos using Taylor series.
cos(x) = ∑_{k=0}^{n/2} (-1)^k x^{2k}/(2k)! + R where |R| ≤ |x|^{n+1}/(n+1)! since all derivatives of cos are bounded by 1.
We intersect with [-1, 1] for tighter bounds on small intervals.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Interval cosine using Taylor coefficients prepared for depth n.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Computable sinh and cosh via exp #
Computable interval enclosure for sinh at a single rational point. Uses the definition sinh(q) = (exp(q) - exp(-q)) / 2.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Computable interval enclosure for cosh at a single rational point. Uses the definition cosh(q) = (exp(q) + exp(-q)) / 2.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The lower bound of coshPointComputable is always at least 1.
Computable interval enclosure for sinh using exp with endpoint evaluation.
sinh(x) = (exp(x) - exp(-x)) / 2 Since sinh is strictly monotone increasing, sinh([a,b]) = [sinh(a), sinh(b)]. We use endpoint evaluation for tight bounds.
Equations
Instances For
Computable interval enclosure for cosh using exp with endpoint evaluation.
cosh(x) = (exp(x) + exp(-x)) / 2 cosh has minimum 1 at x = 0, and is symmetric: cosh(-x) = cosh(x).
- cosh is decreasing on (-∞, 0]
- cosh is increasing on [0, ∞)
We use endpoint evaluation with monotonicity for tight bounds.
Equations
- One or more equations did not get rendered due to their size.
Instances For
FTIA for pow #
FTIA for interval power (binary exponentiation version)
Helper lemmas for Taylor series membership #
Any x in I has |x| ≤ maxAbs I
Coefficient matching lemmas #
For exp, all iterated derivatives at 0 equal 1.
Helper lemmas for Taylor series membership #
General FTIA for evalTaylorSeries (Horner version): if coeffs has length n+1, then ∑_{i=0}^{n} coeffs[i] * x^i ∈ evalTaylorSeries coeffs I for x ∈ I.
The exp Taylor polynomial value matches our evalTaylorSeries. The proof shows that our list-based polynomial evaluation produces the same sum as the Finset.sum form used in Mathlib's Taylor theorem.
The sin Taylor polynomial value matches our evalTaylorSeries. Key: iteratedDeriv i sin 0 = 0, 1, 0, -1, 0, 1, ... matches sinTaylorCoeffs.
The cos Taylor polynomial value matches our evalTaylorSeries. Key: iteratedDeriv i cos 0 = 1, 0, -1, 0, 1, 0, ... matches cosTaylorCoeffs.
Taylor remainder micro-lemmas #
Unified Taylor remainder bound for exp: given x ∈ I with r = maxAbs I, the Taylor remainder |exp x - poly(x)| ≤ 3^(⌈r⌉+1) * r^(n+1) / (n+1)!. This encapsulates the domain setup and remainder calculation.
Unified Taylor remainder bound for sin: given x ∈ I with r = maxAbs I, the Taylor remainder |sin x - poly(x)| ≤ r^(n+1) / (n+1)!. Uses the fact that |sin^(k)(x)| ≤ 1 for all k, x.
Unified Taylor remainder bound for cos: given x ∈ I with r = maxAbs I, the Taylor remainder |cos x - poly(x)| ≤ r^(n+1) / (n+1)!. Uses the fact that |cos^(k)(x)| ≤ 1 for all k, x.
FTIA for computable functions #
FTIA for single-point exp: Real.exp q ∈ expPointComputable q n
FTIA for sinComputable: Real.sin x ∈ sinComputable I n for any x ∈ I.
The proof uses the Taylor remainder micro-lemma and the global bound sin ∈ [-1, 1].
FTIA for cosComputable: Real.cos x ∈ cosComputable I n for any x ∈ I.
The proof uses the Taylor remainder micro-lemma and the global bound cos ∈ [-1, 1].
FTIA for sinhPointComputable: Real.sinh q ∈ sinhPointComputable q n
FTIA for coshPointComputable: Real.cosh q ∈ coshPointComputable q n
FTIA for sinhComputable: Real.sinh x ∈ sinhComputable I n for any x ∈ I.
Uses endpoint evaluation and monotonicity of sinh.
FTIA for coshComputable: Real.cosh x ∈ coshComputable I n for any x ∈ I.
Uses endpoint evaluation and monotonicity properties of cosh.
Computable atanh via Taylor series #
For |y| < 1, atanh(y) = y + y³/3 + y⁵/5 + ... We compute this series for y ∈ [-1/3, 1/3] where it converges rapidly.
Taylor coefficients for atanh: 0, 1, 0, 1/3, 0, 1/5, ... atanh(y) = Σ y^(2k+1)/(2k+1) = y + y³/3 + y⁵/5 + ...
Equations
Instances For
Computable atanh remainder bound. For |y| ≤ r < 1, the remainder after n terms is bounded by r^(n+1)/(1 - r²). We use a conservative bound: r^(n+1) / ((n+1) * (1 - r)) for simplicity.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Computable interval enclosure for atanh at a single rational point. Requires |q| < 1 for convergence. For |q| ≤ 1/3, this is very accurate.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The atanh Taylor polynomial membership: the partial sum of atanh coefficients at q is in evalTaylorSeries (atanhTaylorCoeffs n) (singleton q).
Computable ln(2) via atanh #
ln(2) = 2 * atanh(1/3), since: 2 = (1 + 1/3) / (1 - 1/3) = (4/3) / (2/3) So atanh(1/3) = (1/2) * ln(2), giving ln(2) = 2 * atanh(1/3)
Compute ln(2) as an interval using 2 * atanh(1/3). This converges rapidly since atanh series at 1/3 has |y| = 1/3.
Equations
Instances For
FTIA for ln2Computable: Real.log 2 ∈ ln2Computable n. Uses the identity log(2) = 2 * atanh(1/3) from log_via_atanh.
Computable log via argument reduction #
For q > 0, we compute:
- Reduce q to m * 2^k where m ∈ [1/2, 2]
- Compute log(m) = 2 * atanh((m-1)/(m+1)), which has |arg| ≤ 1/3
- Result = log(m) + k * ln(2)
Reduced mantissa m = q * 2^(-k)
Equations
Instances For
Computable log at a single rational point q > 0. Returns log(q) = log(m) + k * ln(2) where m = q * 2^(-k).
Equations
- One or more equations did not get rendered due to their size.
Instances For
Logarithm evaluation using all configuration-dependent data prepared for depth n.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Computable interval enclosure for log using endpoint evaluation. Since log is strictly increasing on (0, ∞), we evaluate at endpoints.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Interval logarithm using all data prepared for depth n.
Equations
- One or more equations did not get rendered due to their size.
Instances For
FTIA for logPointComputable
FTIA for logComputable: if x ∈ I and I.lo > 0, then log(x) ∈ logComputable I n
Conditional version of mem_logComputable for use in correctness proofs. Requires I.lo > 0 so the log interval is well-defined and monotone.
Computable erf via Taylor series #
Interval containing 2/√π ≈ 1.128379... Used for erf calculations. 2/√π is in (1.128, 1.129).
Equations
- LeanCert.Core.IntervalRat.twoDivSqrtPi = { lo := 1128 / 1000, hi := 1129 / 1000, le := LeanCert.Core.IntervalRat.twoDivSqrtPi._proof_1 }
Instances For
Taylor coefficients for erf (without the 2/√π factor): erf(x) = (2/√π) * Σ_{n=0}^∞ (-1)^n * x^(2n+1) / (n! * (2n+1))
So the coefficient of x^k is:
- 0 if k is even
- (-1)^((k-1)/2) / (((k-1)/2)! * k) if k is odd
Equations
- One or more equations did not get rendered due to their size.
Instances For
Computable erf remainder bound. Since |erf^{(k)}(x)| ≤ (2/√π) * 2^k for all x (rough bound), and erf is bounded by 1, we use a combination.
For the Taylor remainder centered at 0, we use: |R_n(x)| ≤ sup|f^{(n+1)}(ξ)| * |x|^{n+1} / (n+1)!
A conservative bound: |erf^{(k)}(x)| ≤ (2/√π) * k! / (k/2)! ≤ 2 * k^{k/2} But since |erf| ≤ 1, we can intersect with [-1, 1].
We use: remainder ≤ 2 * |x|^{n+1} / (n+1)! (very conservative).
Equations
- One or more equations did not get rendered due to their size.
Instances For
Computable interval enclosure for erf at a single rational point.
Uses sign-aware clipped linear bounds:
|erf(q)| ≤ min(1, (2257/2000)*|q|).
Cases:
q < 0 => erf(q) ∈ [-1, 0]q = 0 => erf(q) = 0q > 0 => erf(q) ∈ [0, 1]
with tighter near-zero magnitude via (2257/2000)*|q|.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Computable interval enclosure for erf using Taylor series with monotonicity.
erf(x) = (2/√π) * Σ_{n=0}^∞ (-1)^n * x^(2n+1) / (n! * (2n+1))
Since erf is strictly monotone increasing (erf'(x) = (2/√π)e^{-x²} > 0), we use endpoint evaluation: erf([a,b]) ⊆ [erf(a), erf(b)].
We intersect with [-1, 1] for safety.
Equations
- One or more equations did not get rendered due to their size.
Instances For
2/√π is in the interval twoDivSqrtPi. 2/√π ≈ 1.1283791670955126, which is in (1.128, 1.129).
This is a helper theorem for correctness proofs. The computation of erfComputable is independent of this theorem.
The "inner" erf function without the 2/√π factor: erfInner(x) = ∫₀ˣ exp(-t²) dt = (√π/2) * erf(x)
This is the function whose Taylor series coefficients are erfTaylorCoeffs.
Instances For
exp(-x²) is analytic everywhere.
exp(-x²) is analytic on ℝ.
Computable atanh interval via endpoint evaluation #
Computable interval enclosure for atanh using endpoint evaluation. Since atanh is strictly increasing on (-1, 1), we evaluate at endpoints. Requires the interval to be strictly inside (-1, 1); returns a wide fallback otherwise.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Interval atanh using Taylor coefficients prepared for depth n.
Equations
- One or more equations did not get rendered due to their size.
Instances For
FTIA for atanhComputable: if x ∈ I and I ⊂ (-1, 1), then atanh(x) ∈ atanhComputable I n.
Rational Endpoint Intervals #
This file defines IntervalRat, a concrete interval type with rational endpoints
suitable for computation. We prove the Fundamental Theorem of Interval Arithmetic
(FTIA) for each operation.
Module Structure #
IntervalRat.Basic- Core types:IntervalRat, membership, basic operationsIntervalRat.Transcendental- Noncomputable transcendental bounds (exp, log, sqrt, atanh)IntervalRat.Taylor- Computable Taylor series evaluators
Main definitions #
LeanCert.Core.IntervalRat- Intervals with rational endpointsLeanCert.Core.IntervalRat.toSet- Semantic interpretation as a subset of ℝ- Operations:
add,neg,sub,mul,inv,div - Computable:
expComputable,sinComputable,cosComputable
Main theorems #
mem_add- FTIA for additionmem_neg- FTIA for negationmem_sub- FTIA for subtractionmem_mul- FTIA for multiplicationmem_expComputable,mem_sinComputable,mem_cosComputable- FTIA for computable functions
Design notes #
All operations maintain the invariant lo ≤ hi. Domain restrictions for partial
operations (like inv) are encoded via separate types or explicit hypotheses.
Dyadic Intervals #
Intervals with Dyadic endpoints. These support "Outward Rounding", ensuring mathematical soundness even when we limit numerical precision.
Main definitions #
IntervalDyadic- Interval with Dyadic endpointsIntervalDyadic.add,mul,neg- Interval arithmetic operationsIntervalDyadic.roundOut- Outward rounding to control precisionIntervalDyadic.toIntervalRat- Convert to rational interval for verification
Design notes #
The key feature is roundOut: after each operation, we can enforce a minimum
exponent to prevent precision explosion. When rounding:
- Lower bounds are shifted down (toward -∞)
- Upper bounds are shifted up (toward +∞)
This maintains the containment invariant: the rounded interval always contains the original interval, which contains the true mathematical value.
Performance #
In v1.0, Rat multiplication of 1/3 * 1/3 * ... * 1/3 (10 times) creates
a denominator of 3^10 = 59049. Each operation requires GCD computation.
In v1.1, with precision = -10, the denominator stays fixed at 2^10 = 1024.
The result is slightly less tight but computed significantly faster.
Equations
Equations
- One or more equations did not get rendered due to their size.
Instances For
Membership and Sets #
Membership in a Dyadic interval
Conversion to IntervalRat #
Convert to IntervalRat for verification with existing theorems
Instances For
Membership is preserved by conversion to IntervalRat
Construction #
Create a singleton interval from a Dyadic
Equations
- LeanCert.Core.IntervalDyadic.singleton d = { lo := d, hi := d, le := ⋯ }
Instances For
Default interval [0, 0]
Create an interval, checking the invariant
Equations
Instances For
The width of an interval
Instances For
Exact midpoint of a dyadic interval.
Dyadics are closed under division by two, so midpoint construction must lower the exponent rather than shift (and potentially round) the mantissa.
Instances For
The lower endpoint is at most the exact midpoint.
The exact midpoint is at most the upper endpoint.
Split a dyadic interval into two exact closed halves.
Equations
Instances For
A point in the original interval and left of the midpoint is in the left half.
A point in the original interval and right of the midpoint is in the right half.
Membership in the left half implies membership in the original interval.
Membership in the right half implies membership in the original interval.
The two closed halves cover the original interval, including their shared seam.
The left child has exactly half the semantic width of its parent.
The right child has exactly half the semantic width of its parent.
Outward Rounding #
Outward rounding: enforces a maximum precision (minimum exponent).
This is the key operation for preventing precision explosion.
minExp is the minimum allowed exponent (higher = coarser precision).
For example, minExp = -10 ensures all values are multiples of 2^(-10) ≈ 0.001.
Instances For
roundOut produces an interval containing the original
Interval Negation #
Negate an interval
Instances For
FTIA for negation
Interval Addition #
Add two intervals
Instances For
FTIA for addition
Add with precision control
Equations
- I.addRounded J prec = (I.add J).roundOut prec
Instances For
Interval Subtraction #
Subtract two intervals
Instances For
FTIA for subtraction
Interval Multiplication #
Multiply two intervals.
Uses min/max of all four endpoint products to handle signs correctly.
This is the exact multiplication - mantissas may grow. Use mulRounded or
mulNormalized for controlled precision.
Correctness: For x ∈ [a,b] and y ∈ [c,d], the product x*y lies in the interval [min(ac,ad,bc,bd), max(ac,ad,bc,bd)].
Equations
Instances For
Fast interval multiplication using sign-based case splitting. Reduces from 4 multiplications + 12 comparisons to 2 multiplications in the common case (both intervals positive or both negative). Falls back to the full 4-way product for mixed-sign intervals.
Equations
- One or more equations did not get rendered due to their size.
Instances For
FTIA for multiplication
mulFast preserves the containment property of mul.
This is retained as documentation and a future audited optimization hook;
production certificate checking currently uses mul directly.
Multiply with precision control (outward rounding)
Equations
- I.mulRounded J prec = (I.mul J).roundOut prec
Instances For
Multiply with mantissa normalization (prevents bit explosion)
Equations
- I.mulNormalized J maxBits = { lo := (I.mul J).lo.normalizeDown maxBits, hi := (I.mul J).hi.normalizeUp maxBits, le := ⋯ }
Instances For
Interval Scaling #
Scale an interval by a constant Dyadic
Equations
Instances For
Scale by a power of 2 (very efficient: just adjusts exponents)
Instances For
Square Root #
Square root of an interval. Returns a conservative bound [0, max(hi, 1)]. This is sound because:
- sqrt(x) = 0 for x < 0 (by definition in Mathlib)
- sqrt(x) ≥ 0 for all x
- sqrt(x) ≤ max(x, 1) for x ≥ 0 Therefore for any x ∈ [lo, hi], sqrt(x) ∈ [0, max(hi, 1)].
Equations
- I.sqrt _prec = { lo := LeanCert.Core.Dyadic.zero, hi := I.hi.max (LeanCert.Core.Dyadic.ofInt 1), le := ⋯ }
Instances For
Soundness of interval sqrt: if x ∈ I, x ≥ 0, then Real.sqrt x ∈ sqrt I
General soundness of interval sqrt for any real input. Handles both non-negative inputs and negative inputs (where Real.sqrt returns 0).
Comparison and Containment #
Check if interval contains zero
Equations
Instances For
Check if entire interval is positive
Equations
Instances For
Check if entire interval is negative
Equations
Instances For
Check if the upper bound is ≤ a rational
Instances For
Check if a rational is ≤ the lower bound
Instances For
Upper bound extraction from membership
Lower bound extraction from membership
What upperBoundedBy means: the interval's hi endpoint is ≤ q
What lowerBoundedBy means: q is ≤ the interval's lo endpoint
Helper for Transcendentals #
Convert from IntervalRat (for transcendental results)
Equations
- One or more equations did not get rendered due to their size.
Instances For
If x ∈ IntervalRat I, then x ∈ ofIntervalRat I prec (outward rounding preserves membership). Requires precision ≤ 0 (e.g. -53).
Intervals with Real Endpoints #
This file defines IntervalReal, an interval type with real (ℝ) endpoints.
Unlike IntervalRat (which has rational endpoints and is suitable for computation),
IntervalReal allows us to represent intervals involving transcendental values
like [1, Real.exp 1] or [Real.log 2, π].
Main definitions #
IntervalReal- Intervals with real endpointsexpInterval- Interval bound for explogInterval- Interval bound for log (on positive intervals)
Main theorems #
mem_expInterval- FTIA for exp: if x ∈ I, then exp(x) ∈ expInterval(I)
Design notes #
This type complements IntervalRat for proving facts about transcendental functions.
While IntervalRat is used for numerical computation (since rationals are computable),
IntervalReal is used for correctness proofs involving exp, log, etc.
Typical workflow:
- Use
IntervalRatfor actual interval arithmetic computations - Convert to
IntervalRealwhen proving facts about transcendental functions - Use mathlib's analysis lemmas directly on real intervals
The set of reals contained in this interval
Instances For
Membership in an interval
Create an interval from a single real
Equations
- LeanCert.Core.IntervalReal.singleton r = { lo := r, hi := r, le := ⋯ }
Instances For
Convert from IntervalRat to IntervalReal
Instances For
Interval addition #
Add two intervals
Instances For
FTIA for addition
Interval negation #
Negate an interval
Instances For
FTIA for negation
Interval multiplication #
The minimum of four real endpoints, used for interval multiplication.
Equations
- LeanCert.Core.IntervalReal.min4 a b c d = min (min a b) (min c d)
Instances For
The maximum of four real endpoints, used for interval multiplication.
Equations
- LeanCert.Core.IntervalReal.max4 a b c d = max (max a b) (max c d)
Instances For
Multiply two intervals
Equations
- One or more equations did not get rendered due to their size.
Instances For
Exponential interval #
Interval bound for exp. Since exp is strictly increasing, exp([a,b]) = [exp(a), exp(b)].
Instances For
FTIA for exp: if x ∈ [a,b], then exp(x) ∈ [exp(a), exp(b)]. This is FULLY PROVED - no sorry, no axioms.
Logarithm interval (for positive intervals) #
Interval bound for log on positive intervals. Since log is strictly increasing on (0, ∞), log([a,b]) = [log(a), log(b)] for a > 0.
Equations
Instances For
FTIA for log: if x ∈ [a,b] with a > 0, then log(x) ∈ [log(a), log(b)]. This is FULLY PROVED - no sorry, no axioms.
Trigonometric intervals (global bounds) #
Interval bound for sin. Since |sin x| ≤ 1 for all x, we use [-1, 1].
Equations
- _I.sinInterval = { lo := -1, hi := 1, le := LeanCert.Core.IntervalReal.sinInterval._proof_1 }
Instances For
FTIA for sin
Interval bound for cos. Since |cos x| ≤ 1 for all x, we use [-1, 1].
Equations
- _I.cosInterval = { lo := -1, hi := 1, le := LeanCert.Core.IntervalReal.sinInterval._proof_1 }
Instances For
FTIA for cos
Interval bound for atan. Since arctan x ∈ (-π/2, π/2) ⊂ [-2, 2] for all x.
Equations
- _I.atanInterval = { lo := -2, hi := 2, le := LeanCert.Core.IntervalReal.atanInterval._proof_1 }
Instances For
FTIA for atan
|arsinh x| ≤ |x| for all x. This follows from MVT and |arsinh'| ≤ 1.
FTIA for arsinh
Hyperbolic function intervals #
Interval bound for sinh. Since sinh is strictly monotonic increasing, sinh([a,b]) = [sinh(a), sinh(b)].
Instances For
FTIA for sinh: if x ∈ [a,b], then sinh(x) ∈ [sinh(a), sinh(b)]. This is FULLY PROVED - no sorry, no axioms.
Interval bound for cosh. cosh is convex with minimum at 0:
- If interval is all non-negative: cosh is increasing
- If interval is all non-positive: cosh is decreasing
- If interval contains 0: minimum is cosh(0) = 1, max is at endpoints
Equations
- One or more equations did not get rendered due to their size.
Instances For
FTIA for cosh: if x ∈ [a,b], then cosh(x) ∈ coshInterval([a,b]). This is FULLY PROVED - no sorry, no axioms.
Square root interval #
Interval bound for sqrt. For any interval I, sqrt(x) ∈ [0, max(hi, 1)] for x ∈ I. This is always sound because:
- sqrt(x) ≥ 0 for all x (Mathlib convention: sqrt(negative) = 0)
- sqrt(x) ≤ max(x, 1) for x ≥ 0, so sqrt(x) ≤ max(hi, 1)
Instances For
FTIA for sqrt: if x ∈ I, then sqrt(x) ∈ sqrtInterval(I). Works for all x including negative (where sqrt returns 0 by Mathlib convention).
Shared Trigonometric Range Reduction #
Common rational π bounds and interval-shifting proofs used by IntervalRat and
Taylor-model trigonometric evaluators.
Rational approximations of π and 2π #
Lower bound for π: 314159265/100000000 < π
Equations
- LeanCert.Core.TrigReduction.piRatLo = 314159265 / 100000000
Instances For
Lower bound for 2π
Instances For
Upper bound for 2π
Instances For
twoPiRatLo < 2π
2π < twoPiRatHi
twoPiRatLo ≤ twoPiRatHi
Range reduction #
Compute the shift amount k such that I.midpoint - k * 2π is approximately in [-π, π].
Equations
Instances For
Shift an interval by subtracting k * 2π using rational bounds.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Reduce interval to be approximately in [-π, π] by subtracting multiples of 2π.
Equations
Instances For
Correctness of range reduction #
If x ∈ I, then x - 2πk ∈ shiftInterval I k.
Convenience form: if x ∈ I, then x - 2πk ∈ (reduceToMainPeriod I).1.
Computable Range Reduction for Trigonometric Functions #
This file implements range reduction for sin and cos to improve Taylor series convergence for intervals far from 0.
Problem #
Standard Taylor series for sin/cos centered at 0 have remainder bounds of
|x|^{n+1} / (n+1)!. For intervals far from 0 (e.g., [10, 11]), this remainder
is huge even for moderate n.
Solution: Range Reduction #
Use the periodicity of sin/cos:
sin(x) = sin(x - 2πk)for any integer kcos(x) = cos(x - 2πk)for any integer k
By choosing k to bring x - 2πk into [-π, π], the Taylor series converges much faster since |x - 2πk| ≤ π ≈ 3.14.
Main definitions #
twoPiRatLo,twoPiRatHi- Rational bounds for 2πreduceToMainPeriod- Shift interval to be near 0sinComputableReduced,cosComputableReduced- Computable evaluation with range reduction
Shared range-reduction API #
The rational lower π bound from the trigonometric reduction implementation.
Instances For
The rational upper π bound from the trigonometric reduction implementation.
Instances For
The rational lower bound for twice π used in argument reduction.
Instances For
The rational upper bound for twice π used in argument reduction.
Instances For
Choose the integer number of periods used to reduce an input interval.
Instances For
Shift an interval by the selected integer multiple of the period enclosure.
Instances For
Return the reduced interval and its integer period shift.
Equations
Instances For
Computable reduced evaluation #
Computable sin evaluation with range reduction.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Computable cos evaluation with range reduction.
Equations
- One or more equations did not get rendered due to their size.
Instances For
sin x ∈ sinComputableReduced I for all x ∈ I
cos x ∈ cosComputableReduced I for all x ∈ I
Computable Interval Evaluation #
This file implements the computable interval evaluator for LeanCert.Core.Expr.
Given an expression and intervals for its variables, we compute an interval
guaranteed to contain all possible values.
Main definitions #
IntervalEnv- Variable assignment as intervalsEvalConfig- Configuration for evaluation parameters (Taylor depth)LeanCert.Internal.Rational.evalTotalCore- Computable interval evaluator for core expressionsevalIntervalCore_correct- Correctness theorem for core evaluation
Design notes #
This evaluator is COMPUTABLE, allowing use of native_decide for bound checking
in tactics. The transcendental functions (exp, sin, cos) use Taylor series with
configurable depth for precision control.
For inv: computes bounds using invInterval, but correctness is not covered by
evalIntervalCore_correct. Use evalIntervalOption for inv.
Interval bounds for transcendental functions #
Simple interval bound for sin. Since |sin x| ≤ 1 for all x, we use the global bound [-1, 1]. This is sound but not tight.
Equations
- LeanCert.Engine.sinInterval _I = { lo := -1, hi := 1, le := LeanCert.Core.IntervalRat.sinComputable._proof_3 }
Instances For
Correctness of sin interval: sin x ∈ [-1, 1] for all x
Simple interval bound for cos. Since |cos x| ≤ 1 for all x, we use the global bound [-1, 1]. This is sound but not tight.
Equations
- LeanCert.Engine.cosInterval _I = { lo := -1, hi := 1, le := LeanCert.Core.IntervalRat.sinComputable._proof_3 }
Instances For
Correctness of cos interval: cos x ∈ [-1, 1] for all x
Simple interval bound for atan. Since atan x ∈ (-π/2, π/2) for all x, we use the global bound [-2, 2]. This is sound but not tight (π/2 ≈ 1.57).
Equations
- LeanCert.Engine.atanInterval _I = { lo := -2, hi := 2, le := LeanCert.Engine.atanInterval._proof_1 }
Instances For
Correctness of atan interval: arctan x ∈ [-2, 2] for all x
Interval bound for erf using computable Taylor series. erf(x) = (2/√π) * ∫₀ˣ exp(-t²) dt, strictly monotone increasing. This computes tight bounds using verified Taylor series.
Equations
- LeanCert.Engine.erfInterval I taylorDepth = I.erfComputable taylorDepth
Instances For
erf is strictly monotone increasing. Proof: erf'(x) = (2/√π) * exp(-x²) > 0 for all x.
We use that for a < b, the integral ∫_{a}^{b} exp(-t²) dt > 0 since the integrand is strictly positive.
Correctness of erfPointComputable.
The enclosure is sign-aware and uses monotonicity of erf with erf(0)=0.
Correctness of erf interval using monotonicity and endpoint evaluation.
Since erf is strictly monotone increasing:
- For x ∈ [I.lo, I.hi], we have erf(I.lo) ≤ erf(x) ≤ erf(I.hi)
- erfPointComputable(I.lo) contains erf(I.lo)
- erfPointComputable(I.hi) contains erf(I.hi)
- hull of these intervals contains [erf(I.lo), erf(I.hi)]
- Therefore erf(x) ∈ hull(...) ∩ [-1, 1]
Simple interval bound for arsinh. arsinh is unbounded, so we use a very rough linear bound. We use max(|lo|, |hi|) + 1 as a safe bound that always works.
Equations
Instances For
Correctness of arsinh interval. Uses the bound |arsinh x| ≤ |x| for all x (from IntervalRealEndpoints).
Interval bound for atanh. atanh is defined for (-1, 1). If interval is within this range, we compute tight bounds using monotonicity. Otherwise returns default.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Correctness of atanh interval: when x ∈ I and I ⊂ (-1, 1), atanh(x) ∈ atanhInterval I.
Tight interval bound for tanh. Since tanh(x) ∈ (-1, 1) for all x ∈ ℝ, we use the global bound [-1, 1]. This avoids the interval explosion that occurs when desugaring to exp.
Equations
- LeanCert.Engine.tanhInterval _I = { lo := -1, hi := 1, le := LeanCert.Core.IntervalRat.sinComputable._proof_3 }
Instances For
Correctness of tanh interval: tanh x ∈ [-1, 1] for all x
Interval enclosure for π. Uses tight bounds from Mathlib's pi_gt_d20 and pi_lt_d20 which give 20 decimal digits. 3.14159265358979323846 < π < 3.14159265358979323847
Equations
- LeanCert.Engine.piInterval = { lo := 31415926535897932 / 10000000000000000, hi := 31415926535897933 / 10000000000000000, le := LeanCert.Engine.piInterval._proof_1 }
Instances For
Correctness of pi interval: Real.pi ∈ piInterval
Interval enclosure for the Euler–Mascheroni constant γ.
Tight bounds derived from eulerMascheroniSeq 100 < γ < eulerMascheroniSeq' 100
combined with explicit Taylor partial sums for log. The proofs below are
axiom-free (no native_decide): all rational arithmetic is certified by
norm_num, and the only analytic inputs are Mathlib's
abs_log_sub_add_sum_range_le and the d9 bounds on log 2.
Equations
- LeanCert.Engine.eulerMascheroniInterval = { lo := 5722 / 10000, hi := 5823 / 10000, le := LeanCert.Engine.eulerMascheroniInterval._proof_1 }
Instances For
Correctness of Euler–Mascheroni interval: γ ∈ eulerMascheroniInterval
Centralized interval lookup for named mathematical constants. Extending this table is the ONLY change needed to add a new constant.
Equations
Instances For
Interval bound for sinh using computable Taylor series for exp. sinh(x) = (exp(x) - exp(-x)) / 2, and sinh is strictly monotonic. This computes tight bounds using the verified exp implementation.
Equations
- LeanCert.Engine.sinhInterval I taylorDepth = I.sinhComputable taylorDepth
Instances For
Interval bound for cosh using computable Taylor series for exp. cosh(x) = (exp(x) + exp(-x)) / 2, with minimum 1 at x = 0. This computes tight bounds using the verified exp implementation.
Equations
- LeanCert.Engine.coshInterval I taylorDepth = I.coshComputable taylorDepth
Instances For
Interval inverse #
Wide bound constant for when inverse is undefined (denominator contains 0)
Equations
- LeanCert.Engine.invWideBound = 10 ^ 30
Instances For
Computable interval inverse.
For [a,b] with a > 0: returns [1/b, 1/a] (1/x is decreasing on positive reals)
For [a,b] with b < 0: returns [1/b, 1/a] (1/x is decreasing on negative reals)
For intervals containing 0: returns wide bounds [-M, M]. NOTE: this branch is
NOT a sound enclosure of x⁻¹ in general (1/x is unbounded near 0); the
correctness theorem mem_invInterval therefore requires the extra
hypothesis |x⁻¹| ≤ invWideBound in that case.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Correctness of invInterval when denominator interval is positive. For x ∈ [a,b] with a > 0, we have 1/x ∈ [1/b, 1/a]
Correctness of invInterval when denominator interval is negative. For x ∈ [a,b] with b < 0, we have 1/x ∈ [1/b, 1/a]
Correctness of invInterval when denominator interval contains zero. Requires a bound on |x⁻¹| to be provable, since x can be arbitrarily close to 0.
Main correctness theorem for invInterval. Fully proved for intervals bounded away from zero. For intervals containing zero, requires a bound on |x⁻¹|.
Correctness of invInterval for intervals bounded away from zero (no extra hypothesis needed)
Core interval evaluation (computable) #
Variable assignment as intervals
Equations
Instances For
Configuration for interval evaluation parameters. This allows certificates to specify the required precision.
- taylorDepth : ℕ
Number of Taylor series terms for transcendental functions
Instances For
Equations
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
Instances For
Default evaluation configuration with 10 Taylor terms
Internal total evaluator for the theorem-restricted core expression fragment.
For expressions in ExprSupportedCore, this computes correct interval
bounds with a fully-verified proof (given domain validity conditions).
For inv: computes bounds using invInterval, but correctness is not
covered by evalIntervalCore_correct. Use evalIntervalOption for inv.
For log: uses logComputable with Taylor series. Correctness requires
that the argument interval is positive (see evalDomainValid).
This evaluator is COMPUTABLE, allowing use of native_decide for
bound checking in tactics. The transcendental functions (exp, sin, cos, log)
use Taylor series with configurable depth for precision control.
Equations
- LeanCert.Internal.Rational.evalTotalCore (LeanCert.Core.Expr.const q) ρ cfg = LeanCert.Core.IntervalRat.singleton q
- LeanCert.Internal.Rational.evalTotalCore (LeanCert.Core.Expr.var idx) ρ cfg = ρ idx
- LeanCert.Internal.Rational.evalTotalCore (e₁.add e₂) ρ cfg = (LeanCert.Internal.Rational.evalTotalCore e₁ ρ cfg).add (LeanCert.Internal.Rational.evalTotalCore e₂ ρ cfg)
- LeanCert.Internal.Rational.evalTotalCore (e₁.mul e₂) ρ cfg = (LeanCert.Internal.Rational.evalTotalCore e₁ ρ cfg).mul (LeanCert.Internal.Rational.evalTotalCore e₂ ρ cfg)
- LeanCert.Internal.Rational.evalTotalCore e_1.neg ρ cfg = (LeanCert.Internal.Rational.evalTotalCore e_1 ρ cfg).neg
- LeanCert.Internal.Rational.evalTotalCore e_1.inv ρ cfg = LeanCert.Engine.invInterval (LeanCert.Internal.Rational.evalTotalCore e_1 ρ cfg)
- LeanCert.Internal.Rational.evalTotalCore e_1.exp ρ cfg = (LeanCert.Internal.Rational.evalTotalCore e_1 ρ cfg).expComputable cfg.taylorDepth
- LeanCert.Internal.Rational.evalTotalCore e_1.sin ρ cfg = (LeanCert.Internal.Rational.evalTotalCore e_1 ρ cfg).sinComputableReduced cfg.taylorDepth
- LeanCert.Internal.Rational.evalTotalCore e_1.cos ρ cfg = (LeanCert.Internal.Rational.evalTotalCore e_1 ρ cfg).cosComputableReduced cfg.taylorDepth
- LeanCert.Internal.Rational.evalTotalCore e_1.log ρ cfg = (LeanCert.Internal.Rational.evalTotalCore e_1 ρ cfg).logComputable cfg.taylorDepth
- LeanCert.Internal.Rational.evalTotalCore e_1.atan ρ cfg = LeanCert.Engine.atanInterval (LeanCert.Internal.Rational.evalTotalCore e_1 ρ cfg)
- LeanCert.Internal.Rational.evalTotalCore e_1.arsinh ρ cfg = LeanCert.Engine.arsinhInterval (LeanCert.Internal.Rational.evalTotalCore e_1 ρ cfg)
- LeanCert.Internal.Rational.evalTotalCore e_1.atanh ρ cfg = default
- LeanCert.Internal.Rational.evalTotalCore e_1.sinc ρ cfg = { lo := -1, hi := 1, le := LeanCert.Core.IntervalRat.sinComputable._proof_3 }
- LeanCert.Internal.Rational.evalTotalCore e_1.erf ρ cfg = LeanCert.Engine.erfInterval (LeanCert.Internal.Rational.evalTotalCore e_1 ρ cfg) cfg.taylorDepth
- LeanCert.Internal.Rational.evalTotalCore e_1.sinh ρ cfg = LeanCert.Engine.sinhInterval (LeanCert.Internal.Rational.evalTotalCore e_1 ρ cfg) cfg.taylorDepth
- LeanCert.Internal.Rational.evalTotalCore e_1.cosh ρ cfg = LeanCert.Engine.coshInterval (LeanCert.Internal.Rational.evalTotalCore e_1 ρ cfg) cfg.taylorDepth
- LeanCert.Internal.Rational.evalTotalCore e_1.tanh ρ cfg = LeanCert.Engine.tanhInterval (LeanCert.Internal.Rational.evalTotalCore e_1 ρ cfg)
- LeanCert.Internal.Rational.evalTotalCore e_1.sqrt ρ cfg = (LeanCert.Internal.Rational.evalTotalCore e_1 ρ cfg).sqrtIntervalTightPrec
- LeanCert.Internal.Rational.evalTotalCore (LeanCert.Core.Expr.namedConst c) ρ cfg = c.interval
Instances For
A real environment is contained in an interval environment
Equations
- LeanCert.Engine.envMem ρ_real ρ_int = ∀ (i : ℕ), ρ_real i ∈ ρ_int i
Instances For
Domain validity predicate for expressions with domain restrictions.
For log: requires the argument interval to be strictly positive. This ensures that logComputable returns correct bounds.
For other expressions: always true (no domain restrictions).
Equations
- LeanCert.Engine.evalDomainValid (LeanCert.Core.Expr.const q) ρ cfg = True
- LeanCert.Engine.evalDomainValid (LeanCert.Core.Expr.var idx) ρ cfg = True
- LeanCert.Engine.evalDomainValid (e₁.add e₂) ρ cfg = (LeanCert.Engine.evalDomainValid e₁ ρ cfg ∧ LeanCert.Engine.evalDomainValid e₂ ρ cfg)
- LeanCert.Engine.evalDomainValid (e₁.mul e₂) ρ cfg = (LeanCert.Engine.evalDomainValid e₁ ρ cfg ∧ LeanCert.Engine.evalDomainValid e₂ ρ cfg)
- LeanCert.Engine.evalDomainValid e_1.neg ρ cfg = LeanCert.Engine.evalDomainValid e_1 ρ cfg
- LeanCert.Engine.evalDomainValid e_1.inv ρ cfg = LeanCert.Engine.evalDomainValid e_1 ρ cfg
- LeanCert.Engine.evalDomainValid e_1.exp ρ cfg = LeanCert.Engine.evalDomainValid e_1 ρ cfg
- LeanCert.Engine.evalDomainValid e_1.sin ρ cfg = LeanCert.Engine.evalDomainValid e_1 ρ cfg
- LeanCert.Engine.evalDomainValid e_1.cos ρ cfg = LeanCert.Engine.evalDomainValid e_1 ρ cfg
- LeanCert.Engine.evalDomainValid e_1.log ρ cfg = (LeanCert.Engine.evalDomainValid e_1 ρ cfg ∧ (LeanCert.Internal.Rational.evalTotalCore e_1 ρ cfg).lo > 0)
- LeanCert.Engine.evalDomainValid e_1.atan ρ cfg = LeanCert.Engine.evalDomainValid e_1 ρ cfg
- LeanCert.Engine.evalDomainValid e_1.arsinh ρ cfg = LeanCert.Engine.evalDomainValid e_1 ρ cfg
- LeanCert.Engine.evalDomainValid e_1.atanh ρ cfg = LeanCert.Engine.evalDomainValid e_1 ρ cfg
- LeanCert.Engine.evalDomainValid e_1.sinc ρ cfg = LeanCert.Engine.evalDomainValid e_1 ρ cfg
- LeanCert.Engine.evalDomainValid e_1.erf ρ cfg = LeanCert.Engine.evalDomainValid e_1 ρ cfg
- LeanCert.Engine.evalDomainValid e_1.sinh ρ cfg = LeanCert.Engine.evalDomainValid e_1 ρ cfg
- LeanCert.Engine.evalDomainValid e_1.cosh ρ cfg = LeanCert.Engine.evalDomainValid e_1 ρ cfg
- LeanCert.Engine.evalDomainValid e_1.tanh ρ cfg = LeanCert.Engine.evalDomainValid e_1 ρ cfg
- LeanCert.Engine.evalDomainValid e_1.sqrt ρ cfg = LeanCert.Engine.evalDomainValid e_1 ρ cfg
- LeanCert.Engine.evalDomainValid (LeanCert.Core.Expr.namedConst c) ρ cfg = True
Instances For
Single-variable domain validity
Equations
- LeanCert.Engine.evalDomainValid1 e I cfg = LeanCert.Engine.evalDomainValid e (fun (x : ℕ) => I) cfg
Instances For
Computable (decidable) check for domain validity
Equations
- LeanCert.Engine.checkDomainValid (LeanCert.Core.Expr.const q) ρ cfg = true
- LeanCert.Engine.checkDomainValid (LeanCert.Core.Expr.var idx) ρ cfg = true
- LeanCert.Engine.checkDomainValid (e₁.add e₂) ρ cfg = (LeanCert.Engine.checkDomainValid e₁ ρ cfg && LeanCert.Engine.checkDomainValid e₂ ρ cfg)
- LeanCert.Engine.checkDomainValid (e₁.mul e₂) ρ cfg = (LeanCert.Engine.checkDomainValid e₁ ρ cfg && LeanCert.Engine.checkDomainValid e₂ ρ cfg)
- LeanCert.Engine.checkDomainValid e_1.neg ρ cfg = LeanCert.Engine.checkDomainValid e_1 ρ cfg
- LeanCert.Engine.checkDomainValid e_1.inv ρ cfg = LeanCert.Engine.checkDomainValid e_1 ρ cfg
- LeanCert.Engine.checkDomainValid e_1.exp ρ cfg = LeanCert.Engine.checkDomainValid e_1 ρ cfg
- LeanCert.Engine.checkDomainValid e_1.sin ρ cfg = LeanCert.Engine.checkDomainValid e_1 ρ cfg
- LeanCert.Engine.checkDomainValid e_1.cos ρ cfg = LeanCert.Engine.checkDomainValid e_1 ρ cfg
- LeanCert.Engine.checkDomainValid e_1.log ρ cfg = (LeanCert.Engine.checkDomainValid e_1 ρ cfg && decide ((LeanCert.Internal.Rational.evalTotalCore e_1 ρ cfg).lo > 0))
- LeanCert.Engine.checkDomainValid e_1.atan ρ cfg = LeanCert.Engine.checkDomainValid e_1 ρ cfg
- LeanCert.Engine.checkDomainValid e_1.arsinh ρ cfg = LeanCert.Engine.checkDomainValid e_1 ρ cfg
- LeanCert.Engine.checkDomainValid e_1.atanh ρ cfg = LeanCert.Engine.checkDomainValid e_1 ρ cfg
- LeanCert.Engine.checkDomainValid e_1.sinc ρ cfg = LeanCert.Engine.checkDomainValid e_1 ρ cfg
- LeanCert.Engine.checkDomainValid e_1.erf ρ cfg = LeanCert.Engine.checkDomainValid e_1 ρ cfg
- LeanCert.Engine.checkDomainValid e_1.sinh ρ cfg = LeanCert.Engine.checkDomainValid e_1 ρ cfg
- LeanCert.Engine.checkDomainValid e_1.cosh ρ cfg = LeanCert.Engine.checkDomainValid e_1 ρ cfg
- LeanCert.Engine.checkDomainValid e_1.tanh ρ cfg = LeanCert.Engine.checkDomainValid e_1 ρ cfg
- LeanCert.Engine.checkDomainValid e_1.sqrt ρ cfg = LeanCert.Engine.checkDomainValid e_1 ρ cfg
- LeanCert.Engine.checkDomainValid (LeanCert.Core.Expr.namedConst c) ρ cfg = true
Instances For
Single-variable domain check
Equations
- LeanCert.Engine.checkDomainValid1 e I cfg = LeanCert.Engine.checkDomainValid e (fun (x : ℕ) => I) cfg
Instances For
checkDomainValid = true implies evalDomainValid
checkDomainValid1 = true implies evalDomainValid1
evalDomainValid is equivalent to checkDomainValid = true
Decidability instance for domain validity
Equations
- LeanCert.Engine.decidableEvalDomainValid e ρ cfg = decidable_of_iff' (LeanCert.Engine.checkDomainValid e ρ cfg = true) ⋯
Decidability instance for single-variable domain validity
Equations
- LeanCert.Engine.decidableEvalDomainValid1 e I cfg = LeanCert.Engine.decidableEvalDomainValid e (fun (x : ℕ) => I) cfg
ADSupported expressions (which don't include log) always have valid domains. This is because only log has domain restrictions (positive argument).
Single-variable version of domainValid for ADSupported
Fundamental correctness theorem for core evaluation.
This theorem is FULLY PROVED for core expressions (no sorry, no axioms).
The hsupp hypothesis ensures we only consider expressions in the
computable verified subset. The hdom hypothesis ensures domain validity
(e.g., log arguments are positive). Works for any Taylor depth.
Convenience functions #
Computable single-variable evaluation for core expressions
Equations
- LeanCert.Internal.Rational.evalTotalCore1 e I cfg = LeanCert.Internal.Rational.evalTotalCore e (fun (x : ℕ) => I) cfg
Instances For
Correctness for single-variable core evaluation
Smart constructors for supported expressions #
Build a constant expression (always supported)
Equations
Instances For
Build a variable expression (always supported)
Equations
- LeanCert.Engine.mkVar idx = ⟨LeanCert.Core.Expr.var idx, ⋯⟩
Instances For
Build an addition (supported if both operands are supported)
Equations
- LeanCert.Engine.mkAdd e₁ e₂ = ⟨(↑e₁).add ↑e₂, ⋯⟩
Instances For
Build a multiplication (supported if both operands are supported)
Equations
- LeanCert.Engine.mkMul e₁ e₂ = ⟨(↑e₁).mul ↑e₂, ⋯⟩
Instances For
Build a negation (supported if operand is supported)
Equations
- LeanCert.Engine.mkNeg e = ⟨(↑e).neg, ⋯⟩
Instances For
Build a sin (supported if operand is supported)
Equations
- LeanCert.Engine.mkSin e = ⟨(↑e).sin, ⋯⟩
Instances For
Build a cos (supported if operand is supported)
Equations
- LeanCert.Engine.mkCos e = ⟨(↑e).cos, ⋯⟩
Instances For
Build an exp (supported if operand is supported)
Equations
- LeanCert.Engine.mkExp e = ⟨(↑e).exp, ⋯⟩
Instances For
Checked evaluation results #
Certified evaluators return a finite enclosure only after all partial-domain conditions have been checked. Failures are data: callers must propagate them instead of substituting a finite sentinel that could be mistaken for an enclosure.
Why a checked evaluator could not produce a finite certified enclosure.
- reciprocalContainsZero (interval : Core.IntervalRat) : EvalError
- logNonpositive (interval : Core.IntervalRat) : EvalError
- atanhOutsideUnitBall (interval : Core.IntervalRat) : EvalError
- unsupportedBackend (operation : String) : EvalError
- unsupportedFeature (feature : String) : EvalError
- invalidConfiguration (message : String) : EvalError
- nestedFailure (operation : String) (cause : EvalError) : EvalError
Instances For
Equations
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
- LeanCert.Engine.instDecidableEqEvalError.decEq (LeanCert.Engine.EvalError.reciprocalContainsZero interval) (LeanCert.Engine.EvalError.logNonpositive interval_1) = isFalse ⋯
- LeanCert.Engine.instDecidableEqEvalError.decEq (LeanCert.Engine.EvalError.reciprocalContainsZero interval) (LeanCert.Engine.EvalError.atanhOutsideUnitBall interval_1) = isFalse ⋯
- LeanCert.Engine.instDecidableEqEvalError.decEq (LeanCert.Engine.EvalError.reciprocalContainsZero interval) (LeanCert.Engine.EvalError.unsupportedBackend operation) = isFalse ⋯
- LeanCert.Engine.instDecidableEqEvalError.decEq (LeanCert.Engine.EvalError.reciprocalContainsZero interval) (LeanCert.Engine.EvalError.unsupportedFeature feature) = isFalse ⋯
- LeanCert.Engine.instDecidableEqEvalError.decEq (LeanCert.Engine.EvalError.reciprocalContainsZero interval) (LeanCert.Engine.EvalError.invalidConfiguration message) = isFalse ⋯
- LeanCert.Engine.instDecidableEqEvalError.decEq (LeanCert.Engine.EvalError.reciprocalContainsZero interval) (LeanCert.Engine.EvalError.nestedFailure operation cause) = isFalse ⋯
- LeanCert.Engine.instDecidableEqEvalError.decEq (LeanCert.Engine.EvalError.logNonpositive interval) (LeanCert.Engine.EvalError.reciprocalContainsZero interval_1) = isFalse ⋯
- LeanCert.Engine.instDecidableEqEvalError.decEq (LeanCert.Engine.EvalError.logNonpositive a) (LeanCert.Engine.EvalError.logNonpositive b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
- LeanCert.Engine.instDecidableEqEvalError.decEq (LeanCert.Engine.EvalError.logNonpositive interval) (LeanCert.Engine.EvalError.atanhOutsideUnitBall interval_1) = isFalse ⋯
- LeanCert.Engine.instDecidableEqEvalError.decEq (LeanCert.Engine.EvalError.logNonpositive interval) (LeanCert.Engine.EvalError.unsupportedBackend operation) = isFalse ⋯
- LeanCert.Engine.instDecidableEqEvalError.decEq (LeanCert.Engine.EvalError.logNonpositive interval) (LeanCert.Engine.EvalError.unsupportedFeature feature) = isFalse ⋯
- LeanCert.Engine.instDecidableEqEvalError.decEq (LeanCert.Engine.EvalError.logNonpositive interval) (LeanCert.Engine.EvalError.invalidConfiguration message) = isFalse ⋯
- LeanCert.Engine.instDecidableEqEvalError.decEq (LeanCert.Engine.EvalError.logNonpositive interval) (LeanCert.Engine.EvalError.nestedFailure operation cause) = isFalse ⋯
- LeanCert.Engine.instDecidableEqEvalError.decEq (LeanCert.Engine.EvalError.atanhOutsideUnitBall interval) (LeanCert.Engine.EvalError.reciprocalContainsZero interval_1) = isFalse ⋯
- LeanCert.Engine.instDecidableEqEvalError.decEq (LeanCert.Engine.EvalError.atanhOutsideUnitBall interval) (LeanCert.Engine.EvalError.logNonpositive interval_1) = isFalse ⋯
- LeanCert.Engine.instDecidableEqEvalError.decEq (LeanCert.Engine.EvalError.atanhOutsideUnitBall interval) (LeanCert.Engine.EvalError.unsupportedBackend operation) = isFalse ⋯
- LeanCert.Engine.instDecidableEqEvalError.decEq (LeanCert.Engine.EvalError.atanhOutsideUnitBall interval) (LeanCert.Engine.EvalError.unsupportedFeature feature) = isFalse ⋯
- LeanCert.Engine.instDecidableEqEvalError.decEq (LeanCert.Engine.EvalError.atanhOutsideUnitBall interval) (LeanCert.Engine.EvalError.invalidConfiguration message) = isFalse ⋯
- LeanCert.Engine.instDecidableEqEvalError.decEq (LeanCert.Engine.EvalError.atanhOutsideUnitBall interval) (LeanCert.Engine.EvalError.nestedFailure operation cause) = isFalse ⋯
- LeanCert.Engine.instDecidableEqEvalError.decEq (LeanCert.Engine.EvalError.unsupportedBackend operation) (LeanCert.Engine.EvalError.reciprocalContainsZero interval) = isFalse ⋯
- LeanCert.Engine.instDecidableEqEvalError.decEq (LeanCert.Engine.EvalError.unsupportedBackend operation) (LeanCert.Engine.EvalError.logNonpositive interval) = isFalse ⋯
- LeanCert.Engine.instDecidableEqEvalError.decEq (LeanCert.Engine.EvalError.unsupportedBackend operation) (LeanCert.Engine.EvalError.atanhOutsideUnitBall interval) = isFalse ⋯
- LeanCert.Engine.instDecidableEqEvalError.decEq (LeanCert.Engine.EvalError.unsupportedBackend a) (LeanCert.Engine.EvalError.unsupportedBackend b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
- LeanCert.Engine.instDecidableEqEvalError.decEq (LeanCert.Engine.EvalError.unsupportedBackend operation) (LeanCert.Engine.EvalError.unsupportedFeature feature) = isFalse ⋯
- LeanCert.Engine.instDecidableEqEvalError.decEq (LeanCert.Engine.EvalError.unsupportedBackend operation) (LeanCert.Engine.EvalError.invalidConfiguration message) = isFalse ⋯
- LeanCert.Engine.instDecidableEqEvalError.decEq (LeanCert.Engine.EvalError.unsupportedBackend operation) (LeanCert.Engine.EvalError.nestedFailure operation_1 cause) = isFalse ⋯
- LeanCert.Engine.instDecidableEqEvalError.decEq (LeanCert.Engine.EvalError.unsupportedFeature feature) (LeanCert.Engine.EvalError.reciprocalContainsZero interval) = isFalse ⋯
- LeanCert.Engine.instDecidableEqEvalError.decEq (LeanCert.Engine.EvalError.unsupportedFeature feature) (LeanCert.Engine.EvalError.logNonpositive interval) = isFalse ⋯
- LeanCert.Engine.instDecidableEqEvalError.decEq (LeanCert.Engine.EvalError.unsupportedFeature feature) (LeanCert.Engine.EvalError.atanhOutsideUnitBall interval) = isFalse ⋯
- LeanCert.Engine.instDecidableEqEvalError.decEq (LeanCert.Engine.EvalError.unsupportedFeature feature) (LeanCert.Engine.EvalError.unsupportedBackend operation) = isFalse ⋯
- LeanCert.Engine.instDecidableEqEvalError.decEq (LeanCert.Engine.EvalError.unsupportedFeature a) (LeanCert.Engine.EvalError.unsupportedFeature b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
- LeanCert.Engine.instDecidableEqEvalError.decEq (LeanCert.Engine.EvalError.unsupportedFeature feature) (LeanCert.Engine.EvalError.invalidConfiguration message) = isFalse ⋯
- LeanCert.Engine.instDecidableEqEvalError.decEq (LeanCert.Engine.EvalError.unsupportedFeature feature) (LeanCert.Engine.EvalError.nestedFailure operation cause) = isFalse ⋯
- LeanCert.Engine.instDecidableEqEvalError.decEq (LeanCert.Engine.EvalError.invalidConfiguration message) (LeanCert.Engine.EvalError.reciprocalContainsZero interval) = isFalse ⋯
- LeanCert.Engine.instDecidableEqEvalError.decEq (LeanCert.Engine.EvalError.invalidConfiguration message) (LeanCert.Engine.EvalError.logNonpositive interval) = isFalse ⋯
- LeanCert.Engine.instDecidableEqEvalError.decEq (LeanCert.Engine.EvalError.invalidConfiguration message) (LeanCert.Engine.EvalError.atanhOutsideUnitBall interval) = isFalse ⋯
- LeanCert.Engine.instDecidableEqEvalError.decEq (LeanCert.Engine.EvalError.invalidConfiguration message) (LeanCert.Engine.EvalError.unsupportedBackend operation) = isFalse ⋯
- LeanCert.Engine.instDecidableEqEvalError.decEq (LeanCert.Engine.EvalError.invalidConfiguration message) (LeanCert.Engine.EvalError.unsupportedFeature feature) = isFalse ⋯
- LeanCert.Engine.instDecidableEqEvalError.decEq (LeanCert.Engine.EvalError.invalidConfiguration message) (LeanCert.Engine.EvalError.nestedFailure operation cause) = isFalse ⋯
- LeanCert.Engine.instDecidableEqEvalError.decEq (LeanCert.Engine.EvalError.nestedFailure operation cause) (LeanCert.Engine.EvalError.reciprocalContainsZero interval) = isFalse ⋯
- LeanCert.Engine.instDecidableEqEvalError.decEq (LeanCert.Engine.EvalError.nestedFailure operation cause) (LeanCert.Engine.EvalError.logNonpositive interval) = isFalse ⋯
- LeanCert.Engine.instDecidableEqEvalError.decEq (LeanCert.Engine.EvalError.nestedFailure operation cause) (LeanCert.Engine.EvalError.atanhOutsideUnitBall interval) = isFalse ⋯
- LeanCert.Engine.instDecidableEqEvalError.decEq (LeanCert.Engine.EvalError.nestedFailure operation cause) (LeanCert.Engine.EvalError.unsupportedBackend operation_1) = isFalse ⋯
- LeanCert.Engine.instDecidableEqEvalError.decEq (LeanCert.Engine.EvalError.nestedFailure operation cause) (LeanCert.Engine.EvalError.unsupportedFeature feature) = isFalse ⋯
- LeanCert.Engine.instDecidableEqEvalError.decEq (LeanCert.Engine.EvalError.nestedFailure operation cause) (LeanCert.Engine.EvalError.invalidConfiguration message) = isFalse ⋯
Instances For
Result type used by checked evaluators and public computation APIs.
Equations
Instances For
Extended (Noncomputable) Interval Evaluation #
This file implements the noncomputable interval evaluator for LeanCert.Core.Expr,
supporting exp with floor/ceil bounds and partial evaluation for inv/log.
Main definitions #
evalInterval- Noncomputable interval evaluator supporting expevalInterval_correct- Correctness theorem for extended evaluationevalIntervalOption- Partial (Option-returning) evaluator with inv/log supportevalIntervalOption_correct- Correctness theorem for partial evaluation
Design notes #
The extended evaluator uses Real.exp with floor/ceil bounds, which requires
noncomputability. For computability, use LeanCert.Internal.Rational.evalTotalCore instead.
The partial evaluator evalIntervalOption returns none when:
- The denominator interval for
invcontains zero - The argument interval for
logis not strictly positive - The argument for
atanhis not in (-1, 1)
When it returns some I, correctness is guaranteed.
Extended interval evaluation (noncomputable, supports exp) #
Noncomputable interval evaluator supporting exp.
For supported expressions (const, var, add, mul, neg, sin, cos, exp), this computes correct interval bounds with a fully-verified proof.
For unsupported expressions (inv, log), returns a default interval. Do not rely on results for expressions containing inv or log. Use evalIntervalOption for partial functions like inv and log.
This evaluator is NONCOMPUTABLE due to exp using Real.exp with floor/ceil.
Equations
- LeanCert.Internal.Rational.evalUnchecked (LeanCert.Core.Expr.const q) ρ = LeanCert.Core.IntervalRat.singleton q
- LeanCert.Internal.Rational.evalUnchecked (LeanCert.Core.Expr.var idx) ρ = ρ idx
- LeanCert.Internal.Rational.evalUnchecked (e₁.add e₂) ρ = (LeanCert.Internal.Rational.evalUnchecked e₁ ρ).add (LeanCert.Internal.Rational.evalUnchecked e₂ ρ)
- LeanCert.Internal.Rational.evalUnchecked (e₁.mul e₂) ρ = (LeanCert.Internal.Rational.evalUnchecked e₁ ρ).mul (LeanCert.Internal.Rational.evalUnchecked e₂ ρ)
- LeanCert.Internal.Rational.evalUnchecked e_1.neg ρ = (LeanCert.Internal.Rational.evalUnchecked e_1 ρ).neg
- LeanCert.Internal.Rational.evalUnchecked e_1.inv ρ = default
- LeanCert.Internal.Rational.evalUnchecked e_1.exp ρ = (LeanCert.Internal.Rational.evalUnchecked e_1 ρ).expInterval
- LeanCert.Internal.Rational.evalUnchecked e_1.sin ρ = LeanCert.Engine.sinInterval (LeanCert.Internal.Rational.evalUnchecked e_1 ρ)
- LeanCert.Internal.Rational.evalUnchecked e_1.cos ρ = LeanCert.Engine.cosInterval (LeanCert.Internal.Rational.evalUnchecked e_1 ρ)
- LeanCert.Internal.Rational.evalUnchecked e_1.log ρ = default
- LeanCert.Internal.Rational.evalUnchecked e_1.atan ρ = LeanCert.Engine.atanInterval (LeanCert.Internal.Rational.evalUnchecked e_1 ρ)
- LeanCert.Internal.Rational.evalUnchecked e_1.arsinh ρ = LeanCert.Engine.arsinhInterval (LeanCert.Internal.Rational.evalUnchecked e_1 ρ)
- LeanCert.Internal.Rational.evalUnchecked e_1.atanh ρ = default
- LeanCert.Internal.Rational.evalUnchecked e_1.sinc ρ = { lo := -1, hi := 1, le := LeanCert.Core.IntervalRat.sinComputable._proof_3 }
- LeanCert.Internal.Rational.evalUnchecked e_1.erf ρ = { lo := -1, hi := 1, le := LeanCert.Core.IntervalRat.sinComputable._proof_3 }
- LeanCert.Internal.Rational.evalUnchecked e_1.sinh ρ = default
- LeanCert.Internal.Rational.evalUnchecked e_1.cosh ρ = default
- LeanCert.Internal.Rational.evalUnchecked e_1.tanh ρ = default
- LeanCert.Internal.Rational.evalUnchecked e_1.sqrt ρ = (LeanCert.Internal.Rational.evalUnchecked e_1 ρ).sqrtInterval
- LeanCert.Internal.Rational.evalUnchecked (LeanCert.Core.Expr.namedConst c) ρ = c.interval
Instances For
Fundamental correctness theorem for extended evaluation.
This theorem is FULLY PROVED (no sorry, no axioms) for supported expressions.
The hsupp hypothesis ensures we only consider expressions in the verified subset.
Convenience functions #
Note: LeanCert.Internal.Rational.evalTotalCore now uses Taylor series for exp/sin/cos, which gives different (often tighter) intervals than evalInterval's floor/ceil bounds. Both are correct, but they are not necessarily equal.
For purely algebraic expressions (const, var, add, mul, neg), both evaluators give identical results.
Internal single-variable wrapper around evalUnchecked.
Equations
- LeanCert.Internal.Rational.evalUnchecked1 e I = LeanCert.Internal.Rational.evalUnchecked e fun (x : ℕ) => I
Instances For
Correctness for single-variable extended evaluation
Partial interval evaluation with inv support #
Partial (Option-returning) interval evaluator supporting inv.
For expressions with inv, this evaluator returns none if the denominator
interval contains zero, and some I with a correct enclosure otherwise.
This allows safe interval evaluation of expressions like 1/x when we can verify the denominator is bounded away from zero.
For expressions without inv, this always returns some with the same
result as evalInterval.
Equations
Instances For
The Taylor truncation depth used by the checked exponential evaluator.
Equations
Instances For
Evaluate an expression by rational intervals, failing when a domain check fails.
Equations
- One or more equations did not get rendered due to their size.
- LeanCert.Engine.evalIntervalOption (LeanCert.Core.Expr.const q) ρ = some (LeanCert.Core.IntervalRat.singleton q)
- LeanCert.Engine.evalIntervalOption (LeanCert.Core.Expr.var idx) ρ = some (ρ idx)
- LeanCert.Engine.evalIntervalOption e_1.neg ρ = match LeanCert.Engine.evalIntervalOption e_1 ρ with | some I => some I.neg | none => none
- LeanCert.Engine.evalIntervalOption e_1.exp ρ = match LeanCert.Engine.evalIntervalOption e_1 ρ with | some I => some (I.expComputable LeanCert.Engine.evalIntervalExpDepth) | none => none
- LeanCert.Engine.evalIntervalOption e_1.sin ρ = match LeanCert.Engine.evalIntervalOption e_1 ρ with | some I => some (LeanCert.Engine.sinInterval I) | none => none
- LeanCert.Engine.evalIntervalOption e_1.cos ρ = match LeanCert.Engine.evalIntervalOption e_1 ρ with | some I => some (LeanCert.Engine.cosInterval I) | none => none
- LeanCert.Engine.evalIntervalOption e_1.atan ρ = match LeanCert.Engine.evalIntervalOption e_1 ρ with | some I => some (LeanCert.Engine.atanInterval I) | none => none
- LeanCert.Engine.evalIntervalOption e_1.arsinh ρ = match LeanCert.Engine.evalIntervalOption e_1 ρ with | some I => some (LeanCert.Engine.arsinhInterval I) | none => none
- LeanCert.Engine.evalIntervalOption e_1.sinh ρ = match LeanCert.Engine.evalIntervalOption e_1 ρ with | some I => some (LeanCert.Engine.sinhInterval I) | none => none
- LeanCert.Engine.evalIntervalOption e_1.cosh ρ = match LeanCert.Engine.evalIntervalOption e_1 ρ with | some I => some (LeanCert.Engine.coshInterval I) | none => none
- LeanCert.Engine.evalIntervalOption e_1.tanh ρ = match LeanCert.Engine.evalIntervalOption e_1 ρ with | some I => some (LeanCert.Engine.tanhInterval I) | none => none
- LeanCert.Engine.evalIntervalOption e_1.sqrt ρ = match LeanCert.Engine.evalIntervalOption e_1 ρ with | some I => some I.sqrtInterval | none => none
- LeanCert.Engine.evalIntervalOption (LeanCert.Core.Expr.namedConst c) ρ = some c.interval
Instances For
Main correctness theorem for evalIntervalOption (approach 1 from plan).
When evalIntervalOption returns some I:
- The expression evaluates to a value in I for all ρ_real ∈ ρ_int
- All inv denominators along the evaluation are guaranteed nonzero (because their intervals don't contain zero)
This follows your suggestion to keep ADSupported syntactic and add separate semantic hypotheses. The key insight is that if evalIntervalOption succeeds (returns Some), the interval arithmetic has already verified that no denominator interval contains zero.
Checked API with diagnostics #
Diagnose the first partial-domain failure after evalIntervalOption returned
none. This function is deliberately separate from the trusted computation:
soundness depends only on successful evalIntervalOption, while diagnostics may be
refined without changing the correctness theorem.
Equations
- One or more equations did not get rendered due to their size.
- LeanCert.Engine.diagnoseEvalIntervalFailure e_2.neg ρ = LeanCert.Engine.EvalError.nestedFailure "unary operand" (LeanCert.Engine.diagnoseEvalIntervalFailure e_2 ρ)
- LeanCert.Engine.diagnoseEvalIntervalFailure e_2.exp ρ = LeanCert.Engine.EvalError.nestedFailure "unary operand" (LeanCert.Engine.diagnoseEvalIntervalFailure e_2 ρ)
- LeanCert.Engine.diagnoseEvalIntervalFailure e_2.sin ρ = LeanCert.Engine.EvalError.nestedFailure "unary operand" (LeanCert.Engine.diagnoseEvalIntervalFailure e_2 ρ)
- LeanCert.Engine.diagnoseEvalIntervalFailure e_2.cos ρ = LeanCert.Engine.EvalError.nestedFailure "unary operand" (LeanCert.Engine.diagnoseEvalIntervalFailure e_2 ρ)
- LeanCert.Engine.diagnoseEvalIntervalFailure e_2.atan ρ = LeanCert.Engine.EvalError.nestedFailure "unary operand" (LeanCert.Engine.diagnoseEvalIntervalFailure e_2 ρ)
- LeanCert.Engine.diagnoseEvalIntervalFailure e_2.arsinh ρ = LeanCert.Engine.EvalError.nestedFailure "unary operand" (LeanCert.Engine.diagnoseEvalIntervalFailure e_2 ρ)
- LeanCert.Engine.diagnoseEvalIntervalFailure e_2.sinc ρ = LeanCert.Engine.EvalError.nestedFailure "unary operand" (LeanCert.Engine.diagnoseEvalIntervalFailure e_2 ρ)
- LeanCert.Engine.diagnoseEvalIntervalFailure e_2.erf ρ = LeanCert.Engine.EvalError.nestedFailure "unary operand" (LeanCert.Engine.diagnoseEvalIntervalFailure e_2 ρ)
- LeanCert.Engine.diagnoseEvalIntervalFailure e_2.sinh ρ = LeanCert.Engine.EvalError.nestedFailure "unary operand" (LeanCert.Engine.diagnoseEvalIntervalFailure e_2 ρ)
- LeanCert.Engine.diagnoseEvalIntervalFailure e_2.cosh ρ = LeanCert.Engine.EvalError.nestedFailure "unary operand" (LeanCert.Engine.diagnoseEvalIntervalFailure e_2 ρ)
- LeanCert.Engine.diagnoseEvalIntervalFailure e_2.tanh ρ = LeanCert.Engine.EvalError.nestedFailure "unary operand" (LeanCert.Engine.diagnoseEvalIntervalFailure e_2 ρ)
- LeanCert.Engine.diagnoseEvalIntervalFailure e_2.sqrt ρ = LeanCert.Engine.EvalError.nestedFailure "unary operand" (LeanCert.Engine.diagnoseEvalIntervalFailure e_2 ρ)
- LeanCert.Engine.diagnoseEvalIntervalFailure (LeanCert.Core.Expr.const q) ρ = LeanCert.Engine.EvalError.unsupportedBackend "internal: total expression unexpectedly failed"
- LeanCert.Engine.diagnoseEvalIntervalFailure (LeanCert.Core.Expr.var idx) ρ = LeanCert.Engine.EvalError.unsupportedBackend "internal: total expression unexpectedly failed"
- LeanCert.Engine.diagnoseEvalIntervalFailure (LeanCert.Core.Expr.namedConst c) ρ = LeanCert.Engine.EvalError.unsupportedBackend "internal: total expression unexpectedly failed"
Instances For
Checked rational evaluator. Every successful result is a certified finite enclosure; domain-invalid expressions return a structured error.
Equations
- LeanCert.Engine.evalIntervalChecked e ρ = match LeanCert.Engine.evalIntervalOption e ρ with | some I => Except.ok I | none => Except.error (LeanCert.Engine.diagnoseEvalIntervalFailure e ρ)
Instances For
Success of evalIntervalChecked is sufficient for enclosure correctness
for every expression constructor.
Checked Rational evaluation with a tight path for the verified computable core. Unsupported syntax or a failed core-domain check falls back to the general checked evaluator, preserving its structured domain errors.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Every successful tight checked Rational evaluation encloses the expression value. The core branch uses the core correctness theorem; the fallback uses the general checked evaluator theorem.
Single-variable version of evalIntervalOption
Equations
- LeanCert.Engine.evalIntervalOption1 e I = LeanCert.Engine.evalIntervalOption e fun (x : ℕ) => I
Instances For
Correctness for single-variable partial evaluation
When evalIntervalOption succeeds, we get bounds
When evalIntervalOption succeeds, we get lower bounds
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 endpointexprCore_ge_of_interval_lo- Lower bound from interval low endpointexprCore_lt_of_interval_hi_lt- Strict upper boundexprCore_gt_of_interval_lo_gt- Strict lower bound
Extended (noncomputable) lemmas #
expr_le_of_interval_hi- Upper bound from interval high endpointexpr_ge_of_interval_lo- Lower bound from interval low endpointexpr_lt_of_interval_hi_lt- Strict upper boundexpr_gt_of_interval_lo_gt- Strict lower boundexpr_le_of_mem_interval- Single-point variantexpr_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) #
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).
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).
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).
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) #
Upper bound lemma for extended expressions. FULLY PROVED - no sorry, no axioms.
Lower bound lemma for extended expressions. FULLY PROVED - no sorry, no axioms.
Strict upper bound for extended expressions. FULLY PROVED - no sorry, no axioms.
Strict lower bound for extended expressions. FULLY PROVED - no sorry, no axioms.
Variant for single point (extended).
Variant for single point (extended).
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 for total core evaluation and automatic differentiationLeanCert.Engine.Eval.Core- Computable interval evaluator (LeanCert.Internal.Rational.evalTotalCore) and transcendental interval boundsLeanCert.Engine.Eval.Extended- Internal noncomputable evaluator and the partial evaluator with inv/log support (evalIntervalOption)LeanCert.Engine.Bounds.Lemmas- Semantic lemmas for deriving real bounds
Main definitions (re-exported) #
Expression support predicates #
ExprSupportedCore- Computable subset (const, var, add, mul, neg, sin, cos, exp, sqrt, sinh, cosh, tanh, pi)ADSupported- Noncomputable AD subset (const, var, add, mul, neg, sin, cos, exp)
Evaluators #
LeanCert.Internal.Rational.evalTotalCore- Computable interval evaluator (uses Taylor series)LeanCert.Internal.Rational.evalUnchecked- Internal noncomputable evaluatorevalIntervalOption- Partial evaluator with inv/log support
Correctness theorems #
evalIntervalCore_correct- Core evaluator correctnessevalInterval_correct- Extended evaluator correctnessevalIntervalOption_correct- Partial evaluator correctness
Tactic lemmas #
exprCore_le_of_interval_hi/exprCore_ge_of_interval_lo- Core boundsexpr_le_of_interval_hi/expr_ge_of_interval_lo- Extended bounds
Design notes #
The evaluators are split by computability:
LeanCert.Internal.Rational.evalTotalCoreis COMPUTABLE, enablingnative_decidein tacticsevalIntervalis NONCOMPUTABLE, using Real.exp with floor/ceil bounds- Both are fully verified (no sorry, no axioms)
Automatic Differentiation - Basic Definitions #
This file provides the core types and algebraic operations for forward-mode automatic differentiation using interval arithmetic.
Main definitions #
DualInterval- A pair of intervals representing (value, derivative)DualInterval.const- Constant dual (derivative is zero)DualInterval.varActive- Active variable (derivative is 1)DualInterval.varPassive- Passive variable (derivative is 0)DualInterval.add- Addition with sum ruleDualInterval.mul- Multiplication with product ruleDualInterval.neg- Negation
Dual number with interval components: represents (value, derivative)
- val : Core.IntervalRat
The interval enclosing the function value.
- der : Core.IntervalRat
The interval enclosing the derivative.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
Default DualInterval for unsupported expression branches
Dual interval for a constant (derivative is zero)
Equations
Instances For
Dual interval for the constant π (derivative is zero)
Equations
Instances For
Dual interval for the Euler–Mascheroni constant γ (derivative is zero)
Equations
Instances For
Dual interval for a named mathematical constant (derivative is zero)
Equations
- LeanCert.Engine.DualInterval.ofMathConst c = { val := c.interval, der := LeanCert.Core.IntervalRat.singleton 0 }
Instances For
Dual interval for the variable we're differentiating with respect to
Equations
- LeanCert.Engine.DualInterval.varActive I = { val := I, der := LeanCert.Core.IntervalRat.singleton 1 }
Instances For
Dual interval for a passive variable
Equations
- LeanCert.Engine.DualInterval.varPassive I = { val := I, der := LeanCert.Core.IntervalRat.singleton 0 }
Instances For
Add two dual intervals
Instances For
Negate a dual interval
Instances For
Inverse of a dual interval (quotient rule: d(1/f) = -f'/f²) Uses invInterval for the value component. For intervals containing zero, returns wide bounds.
Equations
- d.inv = { val := LeanCert.Engine.invInterval d.val, der := (d.der.mul ((LeanCert.Engine.invInterval d.val).mul (LeanCert.Engine.invInterval d.val))).neg }
Instances For
Automatic Differentiation - Transcendental Functions #
This file provides dual interval implementations for transcendental functions, implementing the chain rule for each.
Main definitions #
Total functions (always succeed) #
DualInterval.sin- Sine with chain ruleDualInterval.cos- Cosine with chain ruleDualInterval.exp- Exponential with chain ruleDualInterval.atan- Arctangent with chain ruleDualInterval.arsinh- Inverse hyperbolic sineDualInterval.sinh,cosh,tanh- Hyperbolic functionsDualInterval.erf- Error functionDualInterval.sqrt- Square root (conservative derivative bound)DualInterval.sinc- sinc function
Partial functions (return Option) #
DualInterval.atanhOption- Inverse hyperbolic tangent (requires |x| < 1)DualInterval.inv?- Inverse (requires nonzero)DualInterval.logOption- Logarithm (requires positive)DualInterval.sqrt?- Square root with tight bounds (requires positive)
Dual for sin (chain rule: d(sin f) = cos(f) * f')
Equations
- d.sin = { val := LeanCert.Engine.sinInterval d.val, der := (LeanCert.Engine.cosInterval d.val).mul d.der }
Instances For
Dual for cos (chain rule: d(cos f) = -sin(f) * f')
Equations
Instances For
Dual for exp (chain rule: d(exp f) = exp(f) * f')
Equations
- d.exp = { val := d.val.expInterval, der := d.val.expInterval.mul d.der }
Instances For
The interval [0, 1] used to bound derivative factors in (0, 1]
Equations
- LeanCert.Engine.DualInterval.unitInterval = { lo := 0, hi := 1, le := LeanCert.Engine.DualInterval.unitInterval._proof_1 }
Instances For
The derivative factor for arctan: 1/(1+x²) is in [0, 1]
The derivative factor for arsinh: 1/√(1+x²) is in [0, 1]
Dual for atan (chain rule: d(atan f) = f' / (1 + f²))
Equations
- d.atan = { val := LeanCert.Engine.atanInterval d.val, der := d.der.mul LeanCert.Engine.DualInterval.unitInterval }
Instances For
Dual for arsinh (chain rule: d(arsinh f) = f' / √(1 + f²))
Equations
- d.arsinh = { val := LeanCert.Engine.arsinhInterval d.val, der := d.der.mul LeanCert.Engine.DualInterval.unitInterval }
Instances For
Dual for sinh (chain rule: d(sinh f) = cosh(f) * f')
Equations
- d.sinh = { val := LeanCert.Engine.sinhInterval d.val, der := (LeanCert.Engine.coshInterval d.val).mul d.der }
Instances For
Dual for cosh (chain rule: d(cosh f) = sinh(f) * f')
Equations
- d.cosh = { val := LeanCert.Engine.coshInterval d.val, der := (LeanCert.Engine.sinhInterval d.val).mul d.der }
Instances For
Dual for tanh (chain rule: d(tanh f) = sech²(f) * f' = (1 - tanh²(f)) * f') Since sech²(x) = 1 - tanh²(x) ∈ (0, 1] for all x, we use [0, 1] as bound.
Equations
- d.tanh = { val := LeanCert.Engine.tanhInterval d.val, der := d.der.mul LeanCert.Engine.DualInterval.unitInterval }
Instances For
Interval containing 2/√π ≈ 1.128379...
Equations
- LeanCert.Engine.DualInterval.twoDivSqrtPi = { lo := 1128 / 1000, hi := 1129 / 1000, le := LeanCert.Core.IntervalRat.twoDivSqrtPi._proof_1 }
Instances For
Dual for erf (chain rule: d(erf f) = (2/√π) * exp(-f²) * f') erf'(x) = (2/√π) * exp(-x²), which is always positive and bounded by 2/√π ≈ 1.13
Equations
- One or more equations did not get rendered due to their size.
Instances For
Computable dual for erf using expComputable
Equations
- One or more equations did not get rendered due to their size.
Instances For
Dual for sqrt (chain rule: d(sqrt f) = f' / (2 * sqrt(f))) sqrt'(x) = 1/(2*sqrt(x)) for x > 0, undefined at x = 0. We use sqrtInterval for the value and a conservative bound for the derivative. Note: The derivative blows up as x → 0+, so this uses a wide conservative bound.
Equations
Instances For
Conservative derivative bound [-1, 1] for sinc derivative
Equations
- LeanCert.Engine.DualInterval.sincDerivBound = { lo := -1, hi := 1, le := LeanCert.Core.IntervalRat.sinComputable._proof_3 }
Instances For
Dual for sinc (chain rule: d(sinc f) = sinc'(f) * f') sinc'(x) = (x cos x - sin x) / x² for x ≠ 0, limit 0 at x = 0. We use conservative bound: |sinc'(x)| ≤ 1 for all x.
Equations
- d.sinc = { val := { lo := -1, hi := 1, le := LeanCert.Core.IntervalRat.sinComputable._proof_3 }, der := LeanCert.Engine.DualInterval.sincDerivBound.mul d.der }
Instances For
Partial functions (domain-restricted) #
Partial dual for atanh (chain rule: d(atanh f) = f' / (1 - f²)) Returns None if the value interval is not contained in (-1, 1).
Equations
- One or more equations did not get rendered due to their size.
Instances For
Partial dual for inv (chain rule: d(1/f) = -f'/f²) Returns None if the value interval contains zero.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Partial dual for log (chain rule: d(log f) = f'/f) Returns None if the value interval is not strictly positive.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Compute a conservative upper bound on 1/(2*sqrt(lo)) for lo > 0. Uses the fact that:
- For 0 < lo ≤ 1: sqrt(lo) ≥ lo, so 1/(2sqrt(lo)) ≤ 1/(2lo)
- For lo > 1: sqrt(lo) > 1, so 1/(2*sqrt(lo)) < 1/2
Equations
- One or more equations did not get rendered due to their size.
Instances For
Partial dual for sqrt (chain rule: d(sqrt f) = f' / (2 * sqrt(f))) Returns None if the value interval is not strictly positive.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Automatic Differentiation - Evaluators #
This file provides the evaluation functions for automatic differentiation, mapping expressions to dual intervals.
Main definitions #
DualEnv- Environment mapping variable indices to dual intervalsLeanCert.Internal.AD.evalUnchecked- Main evaluator for supported expressions (total)evalDualOption- Partial evaluator supporting domain-checked functions (returns Option)evalDualOption1- Single-variable version of evalDualOptionmkDualEnv- Create a dual environment for differentiation w.r.t. a variableevalWithDeriv- Evaluate and differentiate w.r.t. a variable indexderivInterval- Get just the derivative intervalevalWithDeriv1- Single-variable evaluation and differentiation
Dual evaluation #
Environment for dual evaluation
Equations
Instances For
Evaluate expression in dual interval mode.
For supported expressions (const, var, add, mul, neg, sin, cos, exp), this computes correct dual interval bounds with a fully-verified proof.
For unsupported expressions (inv, log), returns a default interval. Do not rely on results for expressions containing inv or log. Use evalDualOption for partial functions like inv and log.
Equations
- LeanCert.Internal.AD.evalUnchecked (LeanCert.Core.Expr.const q) ρ = LeanCert.Engine.DualInterval.const q
- LeanCert.Internal.AD.evalUnchecked (LeanCert.Core.Expr.var idx) ρ = ρ idx
- LeanCert.Internal.AD.evalUnchecked (e₁.add e₂) ρ = (LeanCert.Internal.AD.evalUnchecked e₁ ρ).add (LeanCert.Internal.AD.evalUnchecked e₂ ρ)
- LeanCert.Internal.AD.evalUnchecked (e₁.mul e₂) ρ = (LeanCert.Internal.AD.evalUnchecked e₁ ρ).mul (LeanCert.Internal.AD.evalUnchecked e₂ ρ)
- LeanCert.Internal.AD.evalUnchecked e_1.neg ρ = (LeanCert.Internal.AD.evalUnchecked e_1 ρ).neg
- LeanCert.Internal.AD.evalUnchecked e_1.inv ρ = default
- LeanCert.Internal.AD.evalUnchecked e_1.exp ρ = (LeanCert.Internal.AD.evalUnchecked e_1 ρ).exp
- LeanCert.Internal.AD.evalUnchecked e_1.sin ρ = (LeanCert.Internal.AD.evalUnchecked e_1 ρ).sin
- LeanCert.Internal.AD.evalUnchecked e_1.cos ρ = (LeanCert.Internal.AD.evalUnchecked e_1 ρ).cos
- LeanCert.Internal.AD.evalUnchecked e_1.log ρ = default
- LeanCert.Internal.AD.evalUnchecked e_1.atan ρ = (LeanCert.Internal.AD.evalUnchecked e_1 ρ).atan
- LeanCert.Internal.AD.evalUnchecked e_1.arsinh ρ = (LeanCert.Internal.AD.evalUnchecked e_1 ρ).arsinh
- LeanCert.Internal.AD.evalUnchecked e_1.atanh ρ = default
- LeanCert.Internal.AD.evalUnchecked e_1.sinc ρ = (LeanCert.Internal.AD.evalUnchecked e_1 ρ).sinc
- LeanCert.Internal.AD.evalUnchecked e_1.erf ρ = (LeanCert.Internal.AD.evalUnchecked e_1 ρ).erf
- LeanCert.Internal.AD.evalUnchecked e_1.sinh ρ = (LeanCert.Internal.AD.evalUnchecked e_1 ρ).sinh
- LeanCert.Internal.AD.evalUnchecked e_1.cosh ρ = (LeanCert.Internal.AD.evalUnchecked e_1 ρ).cosh
- LeanCert.Internal.AD.evalUnchecked e_1.tanh ρ = (LeanCert.Internal.AD.evalUnchecked e_1 ρ).tanh
- LeanCert.Internal.AD.evalUnchecked e_1.sqrt ρ = (LeanCert.Internal.AD.evalUnchecked e_1 ρ).sqrt
- LeanCert.Internal.AD.evalUnchecked (LeanCert.Core.Expr.namedConst c) ρ = LeanCert.Engine.DualInterval.ofMathConst c
Instances For
Partial dual evaluation #
Partial dual evaluator that supports domain-checked functions.
Returns none if any domain error would occur:
- inv of an interval containing zero
- log of an interval not strictly positive
When it returns
some, the result is guaranteed to be correct.
The total and computable dual evaluators support tanh, but this
Option-returning evaluator deliberately keeps tanh disabled until the
evalDualOption-specific value/differentiability/derivative correctness path
is wired for that constructor.
Equations
- LeanCert.Engine.evalDualOption (LeanCert.Core.Expr.const q) ρ = some (LeanCert.Engine.DualInterval.const q)
- LeanCert.Engine.evalDualOption (LeanCert.Core.Expr.var idx) ρ = some (ρ idx)
- LeanCert.Engine.evalDualOption (e₁.add e₂) ρ = match LeanCert.Engine.evalDualOption e₁ ρ, LeanCert.Engine.evalDualOption e₂ ρ with | some d₁, some d₂ => some (d₁.add d₂) | x, x_1 => none
- LeanCert.Engine.evalDualOption (e₁.mul e₂) ρ = match LeanCert.Engine.evalDualOption e₁ ρ, LeanCert.Engine.evalDualOption e₂ ρ with | some d₁, some d₂ => some (d₁.mul d₂) | x, x_1 => none
- LeanCert.Engine.evalDualOption e_1.neg ρ = match LeanCert.Engine.evalDualOption e_1 ρ with | some d => some d.neg | none => none
- LeanCert.Engine.evalDualOption e_1.inv ρ = match LeanCert.Engine.evalDualOption e_1 ρ with | none => none | some d => d.inv?
- LeanCert.Engine.evalDualOption e_1.exp ρ = match LeanCert.Engine.evalDualOption e_1 ρ with | some d => some d.exp | none => none
- LeanCert.Engine.evalDualOption e_1.sin ρ = match LeanCert.Engine.evalDualOption e_1 ρ with | some d => some d.sin | none => none
- LeanCert.Engine.evalDualOption e_1.cos ρ = match LeanCert.Engine.evalDualOption e_1 ρ with | some d => some d.cos | none => none
- LeanCert.Engine.evalDualOption e_1.log ρ = match LeanCert.Engine.evalDualOption e_1 ρ with | none => none | some d => d.logOption
- LeanCert.Engine.evalDualOption e_1.atan ρ = match LeanCert.Engine.evalDualOption e_1 ρ with | some d => some d.atan | none => none
- LeanCert.Engine.evalDualOption e_1.arsinh ρ = match LeanCert.Engine.evalDualOption e_1 ρ with | some d => some d.arsinh | none => none
- LeanCert.Engine.evalDualOption e_1.atanh ρ = none
- LeanCert.Engine.evalDualOption e_1.sinc ρ = match LeanCert.Engine.evalDualOption e_1 ρ with | some d => some d.sinc | none => none
- LeanCert.Engine.evalDualOption e_1.erf ρ = match LeanCert.Engine.evalDualOption e_1 ρ with | some d => some d.erf | none => none
- LeanCert.Engine.evalDualOption e_1.sinh ρ = match LeanCert.Engine.evalDualOption e_1 ρ with | some d => some d.sinh | none => none
- LeanCert.Engine.evalDualOption e_1.cosh ρ = match LeanCert.Engine.evalDualOption e_1 ρ with | some d => some d.cosh | none => none
- LeanCert.Engine.evalDualOption e_1.tanh ρ = none
- LeanCert.Engine.evalDualOption e_1.sqrt ρ = match LeanCert.Engine.evalDualOption e_1 ρ with | some d => d.sqrt? | none => none
- LeanCert.Engine.evalDualOption (LeanCert.Core.Expr.namedConst c) ρ = some (LeanCert.Engine.DualInterval.ofMathConst c)
Instances For
Single-variable version of evalDualOption
Equations
Instances For
Single variable differentiation #
Create dual environment for differentiating with respect to variable idx
Equations
- LeanCert.Engine.mkDualEnv ρ idx i = if i = idx then LeanCert.Engine.DualInterval.varActive (ρ i) else LeanCert.Engine.DualInterval.varPassive (ρ i)
Instances For
Evaluate and differentiate with respect to variable idx
Equations
Instances For
Get just the derivative interval
Equations
- LeanCert.Engine.derivInterval e ρ idx = (LeanCert.Engine.evalWithDeriv e ρ idx).der
Instances For
Evaluate and differentiate a single-variable expression
Equations
Instances For
Automatic Differentiation - Correctness Theorems #
This file proves the correctness of forward-mode automatic differentiation for supported expressions (ADSupported).
Main theorems #
LeanCert.Engine.evalDualUnchecked_val_correct- Value component is correctLeanCert.Engine.evalDualUnchecked_der_correct- Derivative component is correctevalFunc1_differentiable- Supported expressions are differentiablederiv_mem_dualDer- Key theorem: computed derivative contains true derivativeLeanCert.Engine.evalDualUnchecked_der_correct_idx- n-variable derivative correctnessevalWithDeriv1_correct- Single-variable correctness
Design notes #
All theorems in this file are FULLY PROVED with no sorry or axioms. The correctness relies on the chain rule for each supported operation.
Correctness #
The value component is correct for supported expressions.
This theorem is FULLY PROVED (no sorry, no axioms) for supported expressions.
The hsupp hypothesis ensures we only consider expressions in the verified subset.
Single-variable evaluation for derivative proofs #
The function t ↦ Expr.eval (fun _ => t) e for single-variable expressions
Equations
- LeanCert.Engine.evalFunc1 e t = LeanCert.Core.Expr.eval (fun (x : ℕ) => t) e
Instances For
Differentiability of supported expressions #
Supported expressions are differentiable as single-variable functions.
This theorem shows that for any supported expression,
the function evalFunc1 e is differentiable.
FULLY PROVED - no sorry, no axioms.
Core derivative correctness micro-lemmas #
Real.cos y is always in cosInterval I (which is [-1, 1]). This micro-lemma encapsulates the fact that cosInterval uses the global bound.
Real.sin y is always in sinInterval I (which is [-1, 1]). This micro-lemma encapsulates the fact that sinInterval uses the global bound.
-Real.sin y is always in IntervalRat.neg (sinInterval I). This combines the sin global bound with negation for the cos derivative rule.
The key lemma for n-variable AD: updateVar ρ_real idx x respects mkDualEnv ρ_int idx. This encapsulates the repeated proof that appears in mul/exp cases.
evalFunc1 unfolding lemmas #
Helper lemma: evalFunc1 for atan unfolds correctly
Helper lemma: evalFunc1 for arsinh unfolds correctly
Helper lemma: evalFunc1 for atanh unfolds correctly
Helper lemma: evalFunc1 for erf unfolds correctly
Helper lemma: evalFunc1 for const
Helper lemma: evalFunc1 for var
Helper lemma: evalFunc1 for namedConst (constant function)
Helper lemma: evalFunc1 for pi (constant function)
Helper lemma: evalFunc1 for eulerMascheroni (constant function)
Helper: the dual environment evaluation gives correct derivative. This connects the interval-based AD to actual calculus derivatives.
FULLY PROVED - no sorry, no axioms.
The derivative component of dual interval evaluation is correct. For a supported expression evaluated at a point x in the interval I, the derivative of the expression (as a function of x) lies in the computed derivative interval.
This is the fundamental correctness theorem for forward-mode AD: the derivative bounds computed by interval arithmetic contain the true derivative at every point in the domain.
FULLY PROVED - no sorry, no axioms.
Generalized n-variable derivative correctness #
Helper: evalAlong is differentiable for supported expressions
The derivative of evalAlong with respect to coordinate idx lies in the
computed derivative interval from mkDualEnv.
This is the fundamental n-variable derivative correctness theorem.
It shows that for any expression, if we differentiate along coordinate idx
while holding all other coordinates fixed according to ρ, the derivative
at any point x in the interval ρ_int idx lies in the computed interval.
FULLY PROVED - no sorry, no axioms.
Convenience theorem: derivInterval correctness for n-variable expressions.
The derivative of evalAlong e ρ idx at any point x in the interval
lies in derivInterval e ρ_int idx.
Single-variable expressions #
Predicate: expression only uses variable index 0. This is useful for proving that different environments give the same result when they agree at index 0.
- const (q : ℚ) : UsesOnlyVar0 (Core.Expr.const q)
- var0 : UsesOnlyVar0 (Core.Expr.var 0)
- add (e₁ e₂ : Core.Expr) (h₁ : UsesOnlyVar0 e₁) (h₂ : UsesOnlyVar0 e₂) : UsesOnlyVar0 (e₁.add e₂)
- mul (e₁ e₂ : Core.Expr) (h₁ : UsesOnlyVar0 e₁) (h₂ : UsesOnlyVar0 e₂) : UsesOnlyVar0 (e₁.mul e₂)
- neg (e : Core.Expr) (h : UsesOnlyVar0 e) : UsesOnlyVar0 e.neg
- inv (e : Core.Expr) (h : UsesOnlyVar0 e) : UsesOnlyVar0 e.inv
- sin (e : Core.Expr) (h : UsesOnlyVar0 e) : UsesOnlyVar0 e.sin
- cos (e : Core.Expr) (h : UsesOnlyVar0 e) : UsesOnlyVar0 e.cos
- exp (e : Core.Expr) (h : UsesOnlyVar0 e) : UsesOnlyVar0 e.exp
- log (e : Core.Expr) (h : UsesOnlyVar0 e) : UsesOnlyVar0 e.log
- atan (e : Core.Expr) (h : UsesOnlyVar0 e) : UsesOnlyVar0 e.atan
- arsinh (e : Core.Expr) (h : UsesOnlyVar0 e) : UsesOnlyVar0 e.arsinh
- atanh (e : Core.Expr) (h : UsesOnlyVar0 e) : UsesOnlyVar0 e.atanh
- sinc (e : Core.Expr) (h : UsesOnlyVar0 e) : UsesOnlyVar0 e.sinc
- erf (e : Core.Expr) (h : UsesOnlyVar0 e) : UsesOnlyVar0 e.erf
- sinh (e : Core.Expr) (h : UsesOnlyVar0 e) : UsesOnlyVar0 e.sinh
- cosh (e : Core.Expr) (h : UsesOnlyVar0 e) : UsesOnlyVar0 e.cosh
- tanh (e : Core.Expr) (h : UsesOnlyVar0 e) : UsesOnlyVar0 e.tanh
- sqrt (e : Core.Expr) (h : UsesOnlyVar0 e) : UsesOnlyVar0 e.sqrt
- namedConst (c : Core.MathConst) : UsesOnlyVar0 (Core.Expr.namedConst c)
Instances For
Bridge between the canonical boolean predicate and the proof-carrying
UsesOnlyVar0 predicate used by AD correctness lemmas.
For expressions using only var 0, LeanCert.Internal.AD.evalUnchecked agrees for environments that match at 0
mkDualEnv at index 0 equals varActive at 0
For expressions using only var 0, derivInterval equals evalWithDeriv1
Correctness of single-variable derivative bounds
Automatic Differentiation - Computable Evaluators #
This file provides computable dual evaluators using Taylor-based approximations
for transcendental functions. This enables native_decide for derivative-based
bound checking.
Main definitions #
DualInterval.expCore,sinCore,cosCore- Taylor-based dual functionsDualInterval.sinhCore,coshCore,tanhCore- Hyperbolic Taylor-based dualsLeanCert.Internal.AD.evalTotalCore- Computable dual evaluator for ExprSupportedCorederivIntervalCore- Computable single-variable derivative interval
Main theorems #
LeanCert.Engine.evalDualTotalCore_val_correct- Value component is correctLeanCert.Engine.evalDualTotalCore_der_correct- Derivative component is correctderivIntervalCore_correct- Derivative interval correctnessstrictMonoOn_of_derivIntervalCore_pos- Monotonicity from positive derivativestrictAntiOn_of_derivIntervalCore_neg- Antitonicity from negative derivative
Computable Dual Evaluation for ExprSupportedCore #
This section provides a fully computable dual evaluator that uses Taylor-based
approximations for transcendental functions. This enables native_decide for
derivative-based bound checking.
Computable dual for exp using Taylor series (chain rule: d(exp f) = exp(f) * f')
Equations
- d.expCore n = { val := d.val.expComputable n, der := (d.val.expComputable n).mul d.der }
Instances For
Computable dual for sin using Taylor series
Equations
- d.sinCore n = { val := d.val.sinComputable n, der := (d.val.cosComputable n).mul d.der }
Instances For
Computable dual for cos using Taylor series
Equations
Instances For
Computable dual for log using Taylor series via atanh reduction. Chain rule: d(log f) = f' / f
Equations
- d.logCore n = { val := d.val.logComputable n, der := (LeanCert.Engine.invInterval d.val).mul d.der }
Instances For
Computable dual for sinh using Taylor series (chain rule: d(sinh f) = cosh(f) * f')
Equations
- d.sinhCore n = { val := d.val.sinhComputable n, der := (d.val.coshComputable n).mul d.der }
Instances For
Computable dual for cosh using Taylor series (chain rule: d(cosh f) = sinh(f) * f')
Equations
- d.coshCore n = { val := d.val.coshComputable n, der := (d.val.sinhComputable n).mul d.der }
Instances For
Computable dual for tanh (chain rule: d(tanh f) = sech²(f) * f') Since sech²(x) ∈ (0, 1], we use [0, 1] as a conservative bound.
Equations
Instances For
Computable dual interval evaluator for ExprSupportedCore expressions.
This uses Taylor series approximations for transcendental functions,
making it fully computable and usable with native_decide.
For inv and log, use evalDualChecked or the bounded-denominator
evalDualDyadicChecked; they validate the actual input box before exposing
this total kernel's result. Correctness is not claimed for unchecked
partial-operation branches here.
Equations
- LeanCert.Internal.AD.evalTotalCore (LeanCert.Core.Expr.const q) ρ cfg = LeanCert.Engine.DualInterval.const q
- LeanCert.Internal.AD.evalTotalCore (LeanCert.Core.Expr.var idx) ρ cfg = ρ idx
- LeanCert.Internal.AD.evalTotalCore (e₁.add e₂) ρ cfg = (LeanCert.Internal.AD.evalTotalCore e₁ ρ cfg).add (LeanCert.Internal.AD.evalTotalCore e₂ ρ cfg)
- LeanCert.Internal.AD.evalTotalCore (e₁.mul e₂) ρ cfg = (LeanCert.Internal.AD.evalTotalCore e₁ ρ cfg).mul (LeanCert.Internal.AD.evalTotalCore e₂ ρ cfg)
- LeanCert.Internal.AD.evalTotalCore e_1.neg ρ cfg = (LeanCert.Internal.AD.evalTotalCore e_1 ρ cfg).neg
- LeanCert.Internal.AD.evalTotalCore e_1.inv ρ cfg = (LeanCert.Internal.AD.evalTotalCore e_1 ρ cfg).inv
- LeanCert.Internal.AD.evalTotalCore e_1.exp ρ cfg = (LeanCert.Internal.AD.evalTotalCore e_1 ρ cfg).expCore cfg.taylorDepth
- LeanCert.Internal.AD.evalTotalCore e_1.sin ρ cfg = (LeanCert.Internal.AD.evalTotalCore e_1 ρ cfg).sinCore cfg.taylorDepth
- LeanCert.Internal.AD.evalTotalCore e_1.cos ρ cfg = (LeanCert.Internal.AD.evalTotalCore e_1 ρ cfg).cosCore cfg.taylorDepth
- LeanCert.Internal.AD.evalTotalCore e_1.log ρ cfg = (LeanCert.Internal.AD.evalTotalCore e_1 ρ cfg).logCore cfg.taylorDepth
- LeanCert.Internal.AD.evalTotalCore e_1.atan ρ cfg = (LeanCert.Internal.AD.evalTotalCore e_1 ρ cfg).atan
- LeanCert.Internal.AD.evalTotalCore e_1.arsinh ρ cfg = (LeanCert.Internal.AD.evalTotalCore e_1 ρ cfg).arsinh
- LeanCert.Internal.AD.evalTotalCore e_1.atanh ρ cfg = default
- LeanCert.Internal.AD.evalTotalCore e_1.sinc ρ cfg = (LeanCert.Internal.AD.evalTotalCore e_1 ρ cfg).sinc
- LeanCert.Internal.AD.evalTotalCore e_1.erf ρ cfg = (LeanCert.Internal.AD.evalTotalCore e_1 ρ cfg).erfCore cfg.taylorDepth
- LeanCert.Internal.AD.evalTotalCore e_1.sinh ρ cfg = (LeanCert.Internal.AD.evalTotalCore e_1 ρ cfg).sinhCore cfg.taylorDepth
- LeanCert.Internal.AD.evalTotalCore e_1.cosh ρ cfg = (LeanCert.Internal.AD.evalTotalCore e_1 ρ cfg).coshCore cfg.taylorDepth
- LeanCert.Internal.AD.evalTotalCore e_1.tanh ρ cfg = (LeanCert.Internal.AD.evalTotalCore e_1 ρ cfg).tanhCore cfg.taylorDepth
- LeanCert.Internal.AD.evalTotalCore e_1.sqrt ρ cfg = (LeanCert.Internal.AD.evalTotalCore e_1 ρ cfg).sqrt
- LeanCert.Internal.AD.evalTotalCore (LeanCert.Core.Expr.namedConst c) ρ cfg = LeanCert.Engine.DualInterval.ofMathConst c
Instances For
Computable single-variable derivative interval
Equations
- LeanCert.Engine.derivIntervalCore e I cfg = (LeanCert.Internal.AD.evalTotalCore e (fun (x : ℕ) => LeanCert.Engine.DualInterval.varActive I) cfg).der
Instances For
Domain validity for dual evaluation. This is defined directly in terms of LeanCert.Internal.AD.evalTotalCore to ensure compatibility. For log, we require the argument interval to have positive lower bound.
Equations
- LeanCert.Engine.evalDomainValidDual (LeanCert.Core.Expr.const q) ρ cfg = True
- LeanCert.Engine.evalDomainValidDual (LeanCert.Core.Expr.var idx) ρ cfg = True
- LeanCert.Engine.evalDomainValidDual (e₁.add e₂) ρ cfg = (LeanCert.Engine.evalDomainValidDual e₁ ρ cfg ∧ LeanCert.Engine.evalDomainValidDual e₂ ρ cfg)
- LeanCert.Engine.evalDomainValidDual (e₁.mul e₂) ρ cfg = (LeanCert.Engine.evalDomainValidDual e₁ ρ cfg ∧ LeanCert.Engine.evalDomainValidDual e₂ ρ cfg)
- LeanCert.Engine.evalDomainValidDual e_1.neg ρ cfg = LeanCert.Engine.evalDomainValidDual e_1 ρ cfg
- LeanCert.Engine.evalDomainValidDual e_1.inv ρ cfg = LeanCert.Engine.evalDomainValidDual e_1 ρ cfg
- LeanCert.Engine.evalDomainValidDual e_1.exp ρ cfg = LeanCert.Engine.evalDomainValidDual e_1 ρ cfg
- LeanCert.Engine.evalDomainValidDual e_1.sin ρ cfg = LeanCert.Engine.evalDomainValidDual e_1 ρ cfg
- LeanCert.Engine.evalDomainValidDual e_1.cos ρ cfg = LeanCert.Engine.evalDomainValidDual e_1 ρ cfg
- LeanCert.Engine.evalDomainValidDual e_1.log ρ cfg = (LeanCert.Engine.evalDomainValidDual e_1 ρ cfg ∧ (LeanCert.Internal.AD.evalTotalCore e_1 ρ cfg).val.lo > 0)
- LeanCert.Engine.evalDomainValidDual e_1.atan ρ cfg = LeanCert.Engine.evalDomainValidDual e_1 ρ cfg
- LeanCert.Engine.evalDomainValidDual e_1.arsinh ρ cfg = LeanCert.Engine.evalDomainValidDual e_1 ρ cfg
- LeanCert.Engine.evalDomainValidDual e_1.atanh ρ cfg = LeanCert.Engine.evalDomainValidDual e_1 ρ cfg
- LeanCert.Engine.evalDomainValidDual e_1.sinc ρ cfg = LeanCert.Engine.evalDomainValidDual e_1 ρ cfg
- LeanCert.Engine.evalDomainValidDual e_1.erf ρ cfg = LeanCert.Engine.evalDomainValidDual e_1 ρ cfg
- LeanCert.Engine.evalDomainValidDual e_1.sinh ρ cfg = LeanCert.Engine.evalDomainValidDual e_1 ρ cfg
- LeanCert.Engine.evalDomainValidDual e_1.cosh ρ cfg = LeanCert.Engine.evalDomainValidDual e_1 ρ cfg
- LeanCert.Engine.evalDomainValidDual e_1.tanh ρ cfg = LeanCert.Engine.evalDomainValidDual e_1 ρ cfg
- LeanCert.Engine.evalDomainValidDual e_1.sqrt ρ cfg = LeanCert.Engine.evalDomainValidDual e_1 ρ cfg
- LeanCert.Engine.evalDomainValidDual (LeanCert.Core.Expr.namedConst c) ρ cfg = True
Instances For
Correctness theorem for computable dual value component.
Note: Requires domain validity for log (positive argument interval).
For ADSupported expressions (which exclude log), domain validity is trivially true. This is because ADSupported has no log constructor.
Correctness theorem for computable dual derivative component. Uses ADSupported since derivative correctness requires differentiability.
Convenience theorem: derivIntervalCore correctness
If derivIntervalCore doesn't contain zero, the derivative is nonzero everywhere on I. This is a key theorem for Newton contraction analysis.
If derivIntervalCore.lo > 0, then the derivative is positive everywhere on I.
If derivIntervalCore.hi < 0, then the derivative is negative everywhere on I.
Strictly positive derivative (via Core bounds) implies strict monotonicity
Strictly negative derivative (via Core bounds) implies strict antitonicity
Computable domain-aware automatic differentiation #
This module extends LeanCert's computable forward-mode AD path with checked
reciprocal and logarithm nodes. The existing ADSupported fragment remains
the domain-free fast path. Here, successful evaluation itself certifies both
syntactic support and every partial-domain side condition.
The computable domain-aware AD fragment. Unlike ADSupported, this is a
box-dependent check because reciprocal and logarithm have partial domains.
Equations
- LeanCert.Engine.checkADDomain (LeanCert.Core.Expr.const q) ρ cfg = true
- LeanCert.Engine.checkADDomain (LeanCert.Core.Expr.var idx) ρ cfg = true
- LeanCert.Engine.checkADDomain (a.add b) ρ cfg = (LeanCert.Engine.checkADDomain a ρ cfg && LeanCert.Engine.checkADDomain b ρ cfg)
- LeanCert.Engine.checkADDomain (a.mul b) ρ cfg = (LeanCert.Engine.checkADDomain a ρ cfg && LeanCert.Engine.checkADDomain b ρ cfg)
- LeanCert.Engine.checkADDomain a.neg ρ cfg = LeanCert.Engine.checkADDomain a ρ cfg
- LeanCert.Engine.checkADDomain a.exp ρ cfg = LeanCert.Engine.checkADDomain a ρ cfg
- LeanCert.Engine.checkADDomain a.sin ρ cfg = LeanCert.Engine.checkADDomain a ρ cfg
- LeanCert.Engine.checkADDomain a.cos ρ cfg = LeanCert.Engine.checkADDomain a ρ cfg
- LeanCert.Engine.checkADDomain a.inv ρ cfg = (LeanCert.Engine.checkADDomain a ρ cfg && decide ¬(LeanCert.Internal.AD.evalTotalCore a ρ cfg).val.containsZero)
- LeanCert.Engine.checkADDomain a.log ρ cfg = (LeanCert.Engine.checkADDomain a ρ cfg && decide (LeanCert.Internal.AD.evalTotalCore a ρ cfg).val.isPositive)
- LeanCert.Engine.checkADDomain e ρ cfg = false
Instances For
Best-effort structured explanation for a failed domain-aware AD check.
Equations
- One or more equations did not get rendered due to their size.
- LeanCert.Engine.diagnoseADDomainFailure a.neg ρ cfg = LeanCert.Engine.EvalError.nestedFailure "unary operand" (LeanCert.Engine.diagnoseADDomainFailure a ρ cfg)
- LeanCert.Engine.diagnoseADDomainFailure a.exp ρ cfg = LeanCert.Engine.EvalError.nestedFailure "unary operand" (LeanCert.Engine.diagnoseADDomainFailure a ρ cfg)
- LeanCert.Engine.diagnoseADDomainFailure a.sin ρ cfg = LeanCert.Engine.EvalError.nestedFailure "unary operand" (LeanCert.Engine.diagnoseADDomainFailure a ρ cfg)
- LeanCert.Engine.diagnoseADDomainFailure a.cos ρ cfg = LeanCert.Engine.EvalError.nestedFailure "unary operand" (LeanCert.Engine.diagnoseADDomainFailure a ρ cfg)
- LeanCert.Engine.diagnoseADDomainFailure (LeanCert.Core.Expr.const q) ρ cfg = LeanCert.Engine.EvalError.invalidConfiguration "successful AD expression diagnosed as failure"
- LeanCert.Engine.diagnoseADDomainFailure (LeanCert.Core.Expr.var idx) ρ cfg = LeanCert.Engine.EvalError.invalidConfiguration "successful AD expression diagnosed as failure"
- LeanCert.Engine.diagnoseADDomainFailure e ρ cfg = LeanCert.Engine.EvalError.unsupportedFeature "domain-aware automatic differentiation"
Instances For
Computable checked dual evaluation. No finite derivative enclosure is returned unless every reciprocal denominator excludes zero and every logarithm argument is strictly positive on the input box.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Checked value-and-derivative evaluation along coordinate idx.
Equations
- LeanCert.Engine.evalWithDerivChecked e ρ idx cfg = LeanCert.Engine.evalDualChecked e (LeanCert.Engine.mkDualEnv ρ idx) cfg
Instances For
Checked derivative enclosure along coordinate idx.
Equations
- LeanCert.Engine.derivIntervalChecked e ρ idx cfg = do let __do_lift ← LeanCert.Engine.evalWithDerivChecked e ρ idx cfg pure __do_lift.der
Instances For
Checked derivative enclosure for a single-variable expression.
Equations
- LeanCert.Engine.derivIntervalChecked1 e I cfg = LeanCert.Engine.derivIntervalChecked e (fun (x : ℕ) => I) 0 cfg
Instances For
Successful checked dual evaluation encloses the expression value for every real environment represented by the dual environment.
A successful checked evaluation proves differentiability at every point in the input box along the selected coordinate.
Successful checked indexed AD encloses the true partial derivative.
Golden soundness theorem for the checked derivative-only API.