Numerics Examples

This file demonstrates numerical integration, optimization, and root finding using LeanCert.

Verified Integration Examples

The integrateInterval_correct_n1 theorem is FULLY PROVED for the supported expression subset {const, var, add, mul, neg, sin, cos}. This demonstrates end-to-end verified numerical integration.

Verified Integration Examples

def LeanCert.Examples.Numerics.constOne : Core.Expr

The constant function 1

Equations

• LeanCert.Examples.Numerics.constOne = LeanCert.Core.Expr.const 1

def LeanCert.Examples.Numerics.constOne_supported : Core.ExprSupported constOne

Proof that constOne is in the supported subset

Equations

• LeanCert.Examples.Numerics.constOne_supported = ⋯

def LeanCert.Examples.Numerics.identity : Core.Expr

The identity function x

Equations

• LeanCert.Examples.Numerics.identity = LeanCert.Core.Expr.var 0

def LeanCert.Examples.Numerics.identity_supported : Core.ExprSupported identity

Proof that identity is supported

Equations

• LeanCert.Examples.Numerics.identity_supported = ⋯

def LeanCert.Examples.Numerics.xSquared : Core.Expr

The expression x²

Equations

• LeanCert.Examples.Numerics.xSquared = (LeanCert.Core.Expr.var 0).mul (LeanCert.Core.Expr.var 0)

def LeanCert.Examples.Numerics.xSquared_supported : Core.ExprSupported xSquared

Proof that xSquared is supported

Equations

• LeanCert.Examples.Numerics.xSquared_supported = ⋯

def LeanCert.Examples.Numerics.unitInterval : Core.IntervalRat

Unit interval for integration

Equations

• LeanCert.Examples.Numerics.unitInterval = { lo := 0, hi := 1, le := LeanCert.Examples.Numerics.unitInterval._proof_1 }

Example: Verified integration of constant function

For the constant function 1 over [0,1], the integral is exactly 1. We can prove that our computed interval bound contains this value.

This uses the FULLY PROVED integrateInterval_correct_n1 theorem.

noncomputable def LeanCert.Examples.Numerics.constOne_integral_bound : Core.IntervalRat

The computed interval bound for ∫₀¹ 1 dx

Equations

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

theorem LeanCert.Examples.Numerics.constOne_integral_verified (hInt : IntervalIntegrable (fun (x : ℝ) => Core.Expr.eval (fun (x_1 : ℕ) => x) constOne) MeasureTheory.volume ↑unitInterval.lo ↑unitInterval.hi) : ∫ (x : ℝ) in ↑unitInterval.lo..↑unitInterval.hi, Core.Expr.eval (fun (x_1 : ℕ) => x) constOne ∈ constOne_integral_bound

Verified: the true integral ∫₀¹ 1 dx lies in our computed bound. This theorem has NO SORRY - it's a direct application of the fully-verified integrateInterval_correct_n1.

Example: Verified integration of x²

For x² over [0,1], the true integral is 1/3. Our interval bound is guaranteed to contain this value.

noncomputable def LeanCert.Examples.Numerics.xSquared_integral_bound : Core.IntervalRat

The computed interval bound for ∫₀¹ x² dx

Equations

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

theorem LeanCert.Examples.Numerics.xSquared_integral_verified (hInt : IntervalIntegrable (fun (x : ℝ) => Core.Expr.eval (fun (x_1 : ℕ) => x) xSquared) MeasureTheory.volume ↑unitInterval.lo ↑unitInterval.hi) : ∫ (x : ℝ) in ↑unitInterval.lo..↑unitInterval.hi, Core.Expr.eval (fun (x_1 : ℕ) => x) xSquared ∈ xSquared_integral_bound

Verified: the true integral ∫₀¹ x² dx lies in our computed bound.

Example: Verified integration with sin

For sin(x) over [0, 1], we get verified bounds using the global [-1,1] bound.

def LeanCert.Examples.Numerics.exprSin : Core.Expr

The expression sin(x)

Equations

• LeanCert.Examples.Numerics.exprSin = (LeanCert.Core.Expr.var 0).sin

def LeanCert.Examples.Numerics.exprSin_supported : Core.ExprSupported exprSin

Proof that sin(x) is supported

Equations

• LeanCert.Examples.Numerics.exprSin_supported = ⋯

noncomputable def LeanCert.Examples.Numerics.sin_integral_bound : Core.IntervalRat

The computed interval bound for ∫₀¹ sin(x) dx

Equations

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

theorem LeanCert.Examples.Numerics.sin_integral_verified (hInt : IntervalIntegrable (fun (x : ℝ) => Core.Expr.eval (fun (x_1 : ℕ) => x) exprSin) MeasureTheory.volume ↑unitInterval.lo ↑unitInterval.hi) : ∫ (x : ℝ) in ↑unitInterval.lo..↑unitInterval.hi, Core.Expr.eval (fun (x_1 : ℕ) => x) exprSin ∈ sin_integral_bound

Verified: the true integral ∫₀¹ sin(x) dx lies in our computed bound.

Optimization examples

The optimization module (LeanCert.Engine.Optimize) is fully verified with theorems like minimizeInterval_correct for the ExprSupported subset.

def LeanCert.Examples.Numerics.quadratic : Core.Expr

The expression x² - 2x + 1 = (x-1)² with minimum at x = 1

Equations

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

Root finding examples

The root finding module (LeanCert.Engine.RootFinding.Main) is fully verified with all theorems proved including newton_contraction_has_root and bisection correctness.

def LeanCert.Examples.Numerics.xSquaredMinus2 : Core.Expr

x² - 2 has root at √2 ≈ 1.414

Equations

• LeanCert.Examples.Numerics.xSquaredMinus2 = ((LeanCert.Core.Expr.var 0).mul (LeanCert.Core.Expr.var 0)).sub (LeanCert.Core.Expr.const 2)

def LeanCert.Examples.Numerics.searchInterval : Core.IntervalRat

Search interval for √2

Equations

• LeanCert.Examples.Numerics.searchInterval = { lo := 1, hi := 2, le := LeanCert.Examples.Numerics.searchInterval._proof_1 }

def LeanCert.Examples.Numerics.xSquaredMinus2_supported : Core.ExprSupported xSquaredMinus2

ExprSupported proof for x² - 2

Equations

• LeanCert.Examples.Numerics.xSquaredMinus2_supported = ⋯

Bisection root finding example

For x² - 2, we know the root is √2 ∈ [1, 2]. We demonstrate bisection and prove that when it reports hasRoot, there truly exists a root.

noncomputable def LeanCert.Examples.Numerics.sqrt2_bisect_result : Engine.BisectionResult

Bisection result for x² - 2 on [1, 2] with 20 iterations and tol = 1/100

Equations

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

theorem LeanCert.Examples.Numerics.xSquaredMinus2_continuous : ContinuousOn (fun (x : ℝ) => Core.Expr.eval (fun (x_1 : ℕ) => x) xSquaredMinus2) (Set.Icc ↑searchInterval.lo ↑searchInterval.hi)

x² - 2 evaluates to a polynomial in x, which is continuous

theorem LeanCert.Examples.Numerics.sqrt2_bisect_hasRoot_correct (J : Core.IntervalRat) (s : Engine.RootStatus) : (J, s) ∈ sqrt2_bisect_result.intervals → s = Engine.RootStatus.hasRoot → ∃ x ∈ J, Core.Expr.eval (fun (x_1 : ℕ) => x) xSquaredMinus2 = 0

Correctness: every interval marked hasRoot in bisection result contains a true root. This uses bisectRoot_hasRoot_correct from the verified bisection module.

Optimization example

The quadratic (x-1)² = x² - 2x + 1 has minimum value 0 at x = 1. We demonstrate using minimizeInterval to get verified bounds.

def LeanCert.Examples.Numerics.quadratic_supported : Core.ExprSupported quadratic

ExprSupported proof for quadratic (x² - 2x + 1)

Equations

• LeanCert.Examples.Numerics.quadratic_supported = ⋯

def LeanCert.Examples.Numerics.I02 : Core.IntervalRat

Interval [0, 2] for optimization

Equations

• LeanCert.Examples.Numerics.I02 = { lo := 0, hi := 2, le := LeanCert.Examples.Numerics.I02._proof_1 }

noncomputable def LeanCert.Examples.Numerics.quad_min_result : Engine.OptResult

Minimization result for quadratic on [0, 2]

Equations

• LeanCert.Examples.Numerics.quad_min_result = LeanCert.Engine.minimizeInterval LeanCert.Examples.Numerics.quadratic LeanCert.Examples.Numerics.I02 0 5

def LeanCert.Examples.Numerics.quadratic_var0 : Engine.UsesOnlyVar0 quadratic

UsesOnlyVar0 proof for quadratic

Equations

• LeanCert.Examples.Numerics.quadratic_var0 = ⋯

theorem LeanCert.Examples.Numerics.quad_min_correct (x : ℝ) : x ∈ I02 → ↑quad_min_result.valueBound.lo ≤ Core.Expr.eval (fun (x_1 : ℕ) => x) quadratic

Correctness: the computed lower bound is indeed a lower bound on the true minimum.

For all x in [0, 2], we have quad_min_result.valueBound.lo ≤ quadratic(x). This uses minimizeInterval_correct from the verified optimization module.

Inverse function example

The partial evaluator evalInterval? supports expressions with division (Expr.inv) when the divisor interval excludes zero. This example demonstrates its usage.

def LeanCert.Examples.Numerics.invX : Core.Expr

The expression 1/x (inverse of x)

Equations

• LeanCert.Examples.Numerics.invX = (LeanCert.Core.Expr.var 0).inv

def LeanCert.Examples.Numerics.invX_supported : Core.ExprSupportedWithInv invX

ExprSupportedWithInv proof for 1/x

Equations

• LeanCert.Examples.Numerics.invX_supported = ⋯

def LeanCert.Examples.Numerics.I12 : Core.IntervalRat

Interval [1, 2] - excludes zero, so 1/x is safe to evaluate

Equations

• LeanCert.Examples.Numerics.I12 = { lo := 1, hi := 2, le := LeanCert.Examples.Numerics.searchInterval._proof_1 }

theorem LeanCert.Examples.Numerics.I12_excludes_zero : ¬I12.containsZero

The interval [1, 2] doesn't contain zero

theorem LeanCert.Examples.Numerics.invX_eval_some : Engine.evalInterval?1 invX I12 = some (Core.IntervalRat.invNonzero { toIntervalRat := I12, nonzero := I12_excludes_zero })

Evaluation of 1/x on [1, 2] succeeds because the interval excludes zero

theorem LeanCert.Examples.Numerics.invX_eval_succeeds : (Engine.evalInterval?1 invX I12).isSome = true

Evaluation succeeds

noncomputable def LeanCert.Examples.Numerics.invX_bound : Core.IntervalRat

Get the bound result when evaluation succeeds

Equations

• LeanCert.Examples.Numerics.invX_bound = LeanCert.Core.IntervalRat.invNonzero { toIntervalRat := LeanCert.Examples.Numerics.I12, nonzero := LeanCert.Examples.Numerics.I12_excludes_zero }

theorem LeanCert.Examples.Numerics.invX_correct (x : ℝ) (hx : x ∈ I12) : Core.Expr.eval (fun (x_1 : ℕ) => x) invX ∈ invX_bound

Correctness: if evaluation succeeds, the result contains the true value.

For 1/x on [1, 2], we have 1/x ∈ [1/2, 1] (since x ∈ [1, 2] implies 1/x ∈ [1/2, 1]). The computed bound is guaranteed to contain this.

Refined evaluation example

The refined evaluators use Taylor models for tighter bounds on transcendentals.

noncomputable def LeanCert.Examples.Numerics.sinSmall_refined : Core.IntervalRat

sin(x) on [0, 0.5] - the refined evaluator gives tighter bounds than [-1, 1]

Equations

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

theorem LeanCert.Examples.Numerics.sinSmall_refined_correct (x : ℝ) (hx : x ∈ { lo := 0, hi := 1 / 2, le := ⋯ }) : Core.Expr.eval (fun (x_1 : ℕ) => x) exprSin ∈ sinSmall_refined

Correctness of refined evaluation