Verified Numerical Integration

This file implements numerical integration with rigorous error bounds. Given an expression and an interval, we compute an interval guaranteed to contain the definite integral.

Main definitions

• integrateInterval - Compute bounds on ∫_a^b f(x) dx
• integrateInterval_correct_n1 - Correctness theorem for n=1 (FULLY PROVED)

Algorithm

We use uniform partitioning with interval evaluation:

1. Partition [a, b] into n subintervals
2. On each subinterval, bound f using interval arithmetic
3. Sum the bounds: ∫ ≤ Σ (width * upper_bound)

Verification status

The integrateInterval_correct_n1 theorem is fully proved for ExprSupported expressions. This demonstrates the end-to-end verification pipeline.

Auxiliary lemmas for integration bounds

theorem LeanCert.Engine.integral_bounds_of_bounds {a b lo hi : ℝ} (hab : a ≤ b) {f : ℝ → ℝ} (hf : IntervalIntegrable f MeasureTheory.volume a b) (hlo : ∀ x ∈ Set.Icc a b, lo ≤ f x) (hhi : ∀ x ∈ Set.Icc a b, f x ≤ hi) : lo * (b - a) ≤ ∫ (x : ℝ) in a..b, f x ∧ ∫ (x : ℝ) in a..b, f x ≤ hi * (b - a)

If lo ≤ f(x) ≤ hi for all x ∈ [a, b], then lo * (b - a) ≤ ∫_a^b f ≤ hi * (b - a). This is the fundamental lemma for bounding integrals.

Uniform partition integration

def LeanCert.Engine.uniformPartition (I : Core.IntervalRat) (n : ℕ) (hn : 0 < n) : List Core.IntervalRat

Partition an interval into n equal parts

Equations

• LeanCert.Engine.uniformPartition I n hn = List.ofFn fun (i : Fin n) => { lo := I.lo + (I.hi - I.lo) / ↑n * ↑↑i, hi := I.lo + (I.hi - I.lo) / ↑n * (↑↑i + 1), le := ⋯ }

noncomputable def LeanCert.Engine.sumIntervalBounds (e : Core.Expr) (parts : List Core.IntervalRat) : Core.IntervalRat

Sum of interval bounds over a partition

Equations

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

noncomputable def LeanCert.Engine.integrateInterval (e : Core.Expr) (I : Core.IntervalRat) (n : ℕ) (hn : 0 < n) : Core.IntervalRat

Compute interval bounds on ∫_a^b f(x) dx using uniform partitioning

Equations

• LeanCert.Engine.integrateInterval e I n hn = LeanCert.Engine.sumIntervalBounds e (LeanCert.Engine.uniformPartition I n hn)

Integration correctness for n = 1

noncomputable def LeanCert.Engine.integrateInterval1 (e : Core.Expr) (I : Core.IntervalRat) : Core.IntervalRat

For single-interval integration (n=1), we can compute the result directly.

Equations

• LeanCert.Engine.integrateInterval1 e I = (LeanCert.Core.IntervalRat.singleton I.width).mul (LeanCert.Engine.evalInterval1 e I)

theorem LeanCert.Engine.integrateInterval1_eq (e : Core.Expr) (I : Core.IntervalRat) : integrateInterval e I 1 ⋯ = (Core.IntervalRat.singleton 0).add (integrateInterval1 e I)

The single-interval integration is contained in the general integration for n=1

theorem LeanCert.Engine.integrateInterval1_correct (e : Core.Expr) (hsupp : ExprSupported e) (I : Core.IntervalRat) (hInt : IntervalIntegrable (fun (x : ℝ) => Core.Expr.eval (fun (x_1 : ℕ) => x) e) MeasureTheory.volume ↑I.lo ↑I.hi) : ∫ (x : ℝ) in ↑I.lo..↑I.hi, Core.Expr.eval (fun (x_1 : ℕ) => x) e ∈ integrateInterval1 e I

The single-interval correctness theorem. This is FULLY PROVED - no sorry, no axioms.

theorem LeanCert.Engine.add_zero_left_mem {r : ℝ} {I : Core.IntervalRat} (hr : r ∈ I) : r ∈ (Core.IntervalRat.singleton 0).add I

Adding zero on the left preserves interval membership

theorem LeanCert.Engine.integrateInterval_correct_n1 (e : Core.Expr) (hsupp : ExprSupported e) (I : Core.IntervalRat) (hInt : IntervalIntegrable (fun (x : ℝ) => Core.Expr.eval (fun (x_1 : ℕ) => x) e) MeasureTheory.volume ↑I.lo ↑I.hi) : ∫ (x : ℝ) in ↑I.lo..↑I.hi, Core.Expr.eval (fun (x_1 : ℕ) => x) e ∈ integrateInterval e I 1 ⋯

Correctness for n = 1 (single interval, no partition). This is FULLY PROVED - no sorry, no axioms.

Integration correctness for general n

noncomputable def LeanCert.Engine.partitionPoints (I : Core.IntervalRat) (n i : ℕ) : ℝ

The real sequence of partition points for uniform partition. x_i = I.lo + (I.hi - I.lo) * i / n

Equations

• LeanCert.Engine.partitionPoints I n i = ↑I.lo + (↑I.hi - ↑I.lo) * ↑i / ↑n

theorem LeanCert.Engine.partitionPoints_zero (I : Core.IntervalRat) (n : ℕ) (_hn : 0 < n) : partitionPoints I n 0 = ↑I.lo

x_0 = I.lo

theorem LeanCert.Engine.partitionPoints_n (I : Core.IntervalRat) (n : ℕ) (hn : 0 < n) : partitionPoints I n n = ↑I.hi

x_n = I.hi

theorem LeanCert.Engine.partitionPoints_mono (I : Core.IntervalRat) (n : ℕ) (_hn : 0 < n) (i j : ℕ) (hij : i ≤ j) (_hjn : j ≤ n) : partitionPoints I n i ≤ partitionPoints I n j

The partition points are monotone

def LeanCert.Engine.partitionInterval (I : Core.IntervalRat) (n : ℕ) (hn : 0 < n) (k : ℕ) (hk : k < n) : Core.IntervalRat

The i-th subinterval of the uniform partition

Equations

• LeanCert.Engine.partitionInterval I n hn k hk = (LeanCert.Engine.uniformPartition I n hn).get ⟨k, ⋯⟩

theorem LeanCert.Engine.partitionInterval_lo (I : Core.IntervalRat) (n : ℕ) (hn : 0 < n) (k : ℕ) (hk : k < n) : (partitionInterval I n hn k hk).lo = I.lo + (I.hi - I.lo) / ↑n * ↑k

The lo of the k-th partition interval

theorem LeanCert.Engine.partitionInterval_hi (I : Core.IntervalRat) (n : ℕ) (hn : 0 < n) (k : ℕ) (hk : k < n) : (partitionInterval I n hn k hk).hi = I.lo + (I.hi - I.lo) / ↑n * (↑k + 1)

The hi of the k-th partition interval

theorem LeanCert.Engine.partitionPoints_eq_lo (I : Core.IntervalRat) (n : ℕ) (hn : 0 < n) (k : ℕ) (hk : k < n) : partitionPoints I n k = ↑(partitionInterval I n hn k hk).lo

Partition points match partition interval bounds (real version)

theorem LeanCert.Engine.partitionPoints_eq_hi (I : Core.IntervalRat) (n : ℕ) (hn : 0 < n) (k : ℕ) (hk : k < n) : partitionPoints I n (k + 1) = ↑(partitionInterval I n hn k hk).hi

theorem LeanCert.Engine.intervalIntegrable_on_partition (e : Core.Expr) (I : Core.IntervalRat) (n : ℕ) (hn : 0 < n) (hInt : IntervalIntegrable (fun (x : ℝ) => Core.Expr.eval (fun (x_1 : ℕ) => x) e) MeasureTheory.volume ↑I.lo ↑I.hi) (k : ℕ) (hk : k < n) : IntervalIntegrable (fun (x : ℝ) => Core.Expr.eval (fun (x_1 : ℕ) => x) e) MeasureTheory.volume ↑(partitionInterval I n hn k hk).lo ↑(partitionInterval I n hn k hk).hi

Integrability on a subinterval

theorem LeanCert.Engine.intervalIntegrable_partitionPoints (e : Core.Expr) (I : Core.IntervalRat) (n : ℕ) (hn : 0 < n) (hInt : IntervalIntegrable (fun (x : ℝ) => Core.Expr.eval (fun (x_1 : ℕ) => x) e) MeasureTheory.volume ↑I.lo ↑I.hi) (k : ℕ) (hk : k < n) : IntervalIntegrable (fun (x : ℝ) => Core.Expr.eval (fun (x_1 : ℕ) => x) e) MeasureTheory.volume (partitionPoints I n k) (partitionPoints I n (k + 1))

Integrability using partition points

theorem LeanCert.Engine.integral_partition_sum (e : Core.Expr) (I : Core.IntervalRat) (n : ℕ) (hn : 0 < n) (hInt : IntervalIntegrable (fun (x : ℝ) => Core.Expr.eval (fun (x_1 : ℕ) => x) e) MeasureTheory.volume ↑I.lo ↑I.hi) : ∫ (x : ℝ) in ↑I.lo..↑I.hi, Core.Expr.eval (fun (x_1 : ℕ) => x) e = ∑ k ∈ Finset.range n, ∫ (x : ℝ) in partitionPoints I n k..partitionPoints I n (k + 1), Core.Expr.eval (fun (x_1 : ℕ) => x) e

The integral decomposes over the partition

Summing interval bounds over partitions

theorem LeanCert.Engine.integral_subinterval_bounded (e : Core.Expr) (hsupp : ExprSupported e) (I : Core.IntervalRat) (n : ℕ) (hn : 0 < n) (k : ℕ) (hk : k < n) (hInt : IntervalIntegrable (fun (x : ℝ) => Core.Expr.eval (fun (x_1 : ℕ) => x) e) MeasureTheory.volume ↑I.lo ↑I.hi) : ∫ (x : ℝ) in partitionPoints I n k..partitionPoints I n (k + 1), Core.Expr.eval (fun (x_1 : ℕ) => x) e ∈ integrateInterval1 e (partitionInterval I n hn k hk)

Each subinterval integral is bounded by integrateInterval1 on that subinterval

theorem LeanCert.Engine.IntervalRat_add_assoc (I J K : Core.IntervalRat) : (I.add J).add K = I.add (J.add K)

IntervalRat.add is associative

theorem LeanCert.Engine.foldl_add_concat (acc I : Core.IntervalRat) (Is : List Core.IntervalRat) : List.foldl Core.IntervalRat.add (acc.add I) Is = acc.add (List.foldl Core.IntervalRat.add I Is)

Helper: foldl add distributes: foldl (acc.add I) Is = acc.add (foldl I Is)

theorem LeanCert.Engine.add_singleton_zero_left (I : Core.IntervalRat) : (Core.IntervalRat.singleton 0).add I = I

Adding singleton 0 on the left is identity

theorem LeanCert.Engine.add_singleton_zero_right (I : Core.IntervalRat) : I.add (Core.IntervalRat.singleton 0) = I

Adding singleton 0 on the right is identity

theorem LeanCert.Engine.sum_mem_foldl_add {values : List ℝ} {intervals : List Core.IntervalRat} (hlen : values.length = intervals.length) (hmem : ∀ (i : ℕ) (hi : i < values.length), values[i] ∈ intervals[i]) : values.sum ∈ List.foldl Core.IntervalRat.add (Core.IntervalRat.singleton 0) intervals

Helper: the sum of values in intervals is in the foldl of interval sums

theorem LeanCert.Engine.foldl_sumBound_eq_foldl_add (e : Core.Expr) (parts : List Core.IntervalRat) (acc : Core.IntervalRat) : List.foldl (fun (a I : Core.IntervalRat) => a.add ((Core.IntervalRat.singleton I.width).mul (evalInterval1 e I))) acc parts = List.foldl Core.IntervalRat.add acc (List.map (integrateInterval1 e) parts)

Helper: generalized foldl lemma relating sumIntervalBounds-style fold with add fold

theorem LeanCert.Engine.sumIntervalBounds_eq_foldl_map (e : Core.Expr) (parts : List Core.IntervalRat) : sumIntervalBounds e parts = List.foldl Core.IntervalRat.add (Core.IntervalRat.singleton 0) (List.map (integrateInterval1 e) parts)

sumIntervalBounds equals foldl over mapped integrateInterval1

theorem LeanCert.Engine.integrateInterval_correct (e : Core.Expr) (hsupp : ExprSupported e) (I : Core.IntervalRat) (n : ℕ) (hn : 0 < n) (hInt : IntervalIntegrable (fun (x : ℝ) => Core.Expr.eval (fun (x_1 : ℕ) => x) e) MeasureTheory.volume ↑I.lo ↑I.hi) : ∫ (x : ℝ) in ↑I.lo..↑I.hi, Core.Expr.eval (fun (x_1 : ℕ) => x) e ∈ integrateInterval e I n hn

Main theorem: the integral lies in integrateInterval for general n

Adaptive integration

Interval operations for error estimation

def LeanCert.Engine.intervalInter (I J : Core.IntervalRat) : Core.IntervalRat

Interval intersection (returns the tighter bound). If intervals don't overlap, returns the first one (conservative).

Equations

• LeanCert.Engine.intervalInter I J = if h : max I.lo J.lo ≤ min I.hi J.hi then { lo := max I.lo J.lo, hi := min I.hi J.hi, le := h } else if I.width ≤ J.width then I else J

theorem LeanCert.Engine.mem_intervalInter {x : ℝ} {I J : Core.IntervalRat} (hI : x ∈ I) (hJ : x ∈ J) : x ∈ intervalInter I J

Intersection is sound: if x ∈ I and x ∈ J, then x ∈ inter I J

def LeanCert.Engine.intervalUnion (I J : Core.IntervalRat) : Core.IntervalRat

Union of intervals (convex hull)

Equations

• LeanCert.Engine.intervalUnion I J = { lo := min I.lo J.lo, hi := max I.hi J.hi, le := ⋯ }

theorem LeanCert.Engine.mem_intervalUnion_left {x : ℝ} {I J : Core.IntervalRat} (hI : x ∈ I) : x ∈ intervalUnion I J

Union is sound: if x ∈ I then x ∈ union I J

theorem LeanCert.Engine.mem_intervalUnion_right {x : ℝ} {I J : Core.IntervalRat} (hJ : x ∈ J) : x ∈ intervalUnion I J

Union is sound: if x ∈ J then x ∈ union I J

Splitting intervals

theorem LeanCert.Engine.midpoint_def (I : Core.IntervalRat) : I.midpoint = (I.lo + I.hi) / 2

Midpoint definition helper

theorem LeanCert.Engine.midpoint_lo_le (I : Core.IntervalRat) : I.lo ≤ I.midpoint

Midpoint is at least lo

theorem LeanCert.Engine.midpoint_le_hi' (I : Core.IntervalRat) : I.midpoint ≤ I.hi

Midpoint is at most hi

def LeanCert.Engine.splitMid (I : Core.IntervalRat) : Core.IntervalRat × Core.IntervalRat

Split an interval at its midpoint

Equations

• LeanCert.Engine.splitMid I = ({ lo := I.lo, hi := I.midpoint, le := ⋯ }, { lo := I.midpoint, hi := I.hi, le := ⋯ })

theorem LeanCert.Engine.splitMid_left_lo (I : Core.IntervalRat) : (splitMid I).1.lo = I.lo

The left half of a split covers [lo, mid]

theorem LeanCert.Engine.splitMid_left_hi (I : Core.IntervalRat) : (splitMid I).1.hi = I.midpoint

theorem LeanCert.Engine.splitMid_right_lo (I : Core.IntervalRat) : (splitMid I).2.lo = I.midpoint

The right half of a split covers [mid, hi]

theorem LeanCert.Engine.splitMid_right_hi (I : Core.IntervalRat) : (splitMid I).2.hi = I.hi

theorem LeanCert.Engine.mem_splitMid {x : ℝ} {I : Core.IntervalRat} (hx : x ∈ I) : x ∈ (splitMid I).1 ∨ x ∈ (splitMid I).2

Splitting preserves coverage: any x in I is in one of the halves

Adaptive integration result and algorithm

structure LeanCert.Engine.AdaptiveResult : Type

Adaptive integration result

• bound : Core.IntervalRat

  Interval containing the integral

• evals : ℕ

  Number of function evaluations used

noncomputable def LeanCert.Engine.integrateRefined (e : Core.Expr) (I : Core.IntervalRat) : Core.IntervalRat

Compute integration bound for a single interval using n=2 panels

Equations

• LeanCert.Engine.integrateRefined e I = LeanCert.Engine.integrateInterval e I 2 LeanCert.Engine.integrateRefined._proof_1

noncomputable def LeanCert.Engine.integrateCoarse (e : Core.Expr) (I : Core.IntervalRat) : Core.IntervalRat

Compute integration bound for a single interval using n=1 panel (coarse)

Equations

• LeanCert.Engine.integrateCoarse e I = LeanCert.Engine.integrateInterval e I 1 LeanCert.Engine.integrateCoarse._proof_1

def LeanCert.Engine.errorEstimate (refined : Core.IntervalRat) : ℚ

Error estimate: width of the refined bound (Conservative: could use intersection, but width of refined is simpler)

Equations

• LeanCert.Engine.errorEstimate refined = refined.width

noncomputable def LeanCert.Engine.integrateAdaptiveAux (e : Core.Expr) (I : Core.IntervalRat) (tol : ℚ) (maxDepth : ℕ) : AdaptiveResult

Recursive adaptive integration. At each level, computes refined bound and either:

• Returns if error ≤ tol or maxDepth = 0
• Subdivides and recurses

Equations

• One or more equations did not get rendered due to their size.
• LeanCert.Engine.integrateAdaptiveAux e I tol 0 = { bound := LeanCert.Engine.integrateRefined e I, evals := 2 }

noncomputable def LeanCert.Engine.integrateAdaptive (e : Core.Expr) (I : Core.IntervalRat) (tol : ℚ) (_htol : 0 < tol) (maxDepth : ℕ) : AdaptiveResult

Adaptive integration with error tolerance. Keeps subdividing until the uncertainty is below tol.

Equations

• LeanCert.Engine.integrateAdaptive e I tol _htol maxDepth = LeanCert.Engine.integrateAdaptiveAux e I tol maxDepth

Correctness proofs for adaptive integration

theorem LeanCert.Engine.integrateRefined_correct (e : Core.Expr) (hsupp : ExprSupported e) (I : Core.IntervalRat) (hInt : IntervalIntegrable (fun (x : ℝ) => Core.Expr.eval (fun (x_1 : ℕ) => x) e) MeasureTheory.volume ↑I.lo ↑I.hi) : ∫ (x : ℝ) in ↑I.lo..↑I.hi, Core.Expr.eval (fun (x_1 : ℕ) => x) e ∈ integrateRefined e I

integrateRefined is correct (direct from integrateInterval_correct)

theorem LeanCert.Engine.integrateCoarse_correct (e : Core.Expr) (hsupp : ExprSupported e) (I : Core.IntervalRat) (hInt : IntervalIntegrable (fun (x : ℝ) => Core.Expr.eval (fun (x_1 : ℕ) => x) e) MeasureTheory.volume ↑I.lo ↑I.hi) : ∫ (x : ℝ) in ↑I.lo..↑I.hi, Core.Expr.eval (fun (x_1 : ℕ) => x) e ∈ integrateCoarse e I

integrateCoarse is correct

theorem LeanCert.Engine.midpoint_ge_lo_real (I : Core.IntervalRat) : ↑I.lo ≤ ↑I.midpoint

Helper: midpoint is between lo and hi (real version)

theorem LeanCert.Engine.midpoint_le_hi_real (I : Core.IntervalRat) : ↑I.midpoint ≤ ↑I.hi

theorem LeanCert.Engine.midpoint_mem_uIcc (I : Core.IntervalRat) : ↑I.midpoint ∈ Set.uIcc ↑I.lo ↑I.hi

Midpoint is in the interval

theorem LeanCert.Engine.integral_split_mid (e : Core.Expr) (I : Core.IntervalRat) (hInt : IntervalIntegrable (fun (x : ℝ) => Core.Expr.eval (fun (x_1 : ℕ) => x) e) MeasureTheory.volume ↑I.lo ↑I.hi) : ∫ (x : ℝ) in ↑I.lo..↑I.hi, Core.Expr.eval (fun (x_1 : ℕ) => x) e = (∫ (x : ℝ) in ↑I.lo..↑I.midpoint, Core.Expr.eval (fun (x_1 : ℕ) => x) e) + ∫ (x : ℝ) in ↑I.midpoint..↑I.hi, Core.Expr.eval (fun (x_1 : ℕ) => x) e

Helper: integral over split interval equals sum of integrals over halves

theorem LeanCert.Engine.intervalIntegrable_splitMid_left (e : Core.Expr) (I : Core.IntervalRat) (hInt : IntervalIntegrable (fun (x : ℝ) => Core.Expr.eval (fun (x_1 : ℕ) => x) e) MeasureTheory.volume ↑I.lo ↑I.hi) : IntervalIntegrable (fun (x : ℝ) => Core.Expr.eval (fun (x_1 : ℕ) => x) e) MeasureTheory.volume ↑(splitMid I).1.lo ↑(splitMid I).1.hi

Integrability on left half

theorem LeanCert.Engine.intervalIntegrable_splitMid_right (e : Core.Expr) (I : Core.IntervalRat) (hInt : IntervalIntegrable (fun (x : ℝ) => Core.Expr.eval (fun (x_1 : ℕ) => x) e) MeasureTheory.volume ↑I.lo ↑I.hi) : IntervalIntegrable (fun (x : ℝ) => Core.Expr.eval (fun (x_1 : ℕ) => x) e) MeasureTheory.volume ↑(splitMid I).2.lo ↑(splitMid I).2.hi

Integrability on right half

theorem LeanCert.Engine.integrateAdaptiveAux_correct (e : Core.Expr) (hsupp : ExprSupported e) (I : Core.IntervalRat) (tol : ℚ) (maxDepth : ℕ) (hInt : IntervalIntegrable (fun (x : ℝ) => Core.Expr.eval (fun (x_1 : ℕ) => x) e) MeasureTheory.volume ↑I.lo ↑I.hi) : ∫ (x : ℝ) in ↑I.lo..↑I.hi, Core.Expr.eval (fun (x_1 : ℕ) => x) e ∈ (integrateAdaptiveAux e I tol maxDepth).bound

Main soundness theorem: adaptive integration returns a bound containing the true integral. This is proved by induction on maxDepth.

theorem LeanCert.Engine.integrateAdaptive_correct (e : Core.Expr) (hsupp : ExprSupported e) (I : Core.IntervalRat) (tol : ℚ) (htol : 0 < tol) (maxDepth : ℕ) (hInt : IntervalIntegrable (fun (x : ℝ) => Core.Expr.eval (fun (x_1 : ℕ) => x) e) MeasureTheory.volume ↑I.lo ↑I.hi) : ∫ (x : ℝ) in ↑I.lo..↑I.hi, Core.Expr.eval (fun (x_1 : ℕ) => x) e ∈ (integrateAdaptive e I tol htol maxDepth).bound

Soundness of the main adaptive integration function

Non-uniform (geometric) partitioning

def LeanCert.Engine.geometricBreakpoints (start stop w₀ ratio : ℚ) (maxN : ℕ) : List ℚ

Build geometric breakpoints from start, growing by ratio each step. Returns list of breakpoints (not intervals). Stops at stop or after maxN steps.

Equations

• LeanCert.Engine.geometricBreakpoints start stop w₀ ratio maxN = (LeanCert.Engine.geometricBreakpoints.go stop ratio start w₀ maxN []).reverse

@[irreducible]

def LeanCert.Engine.geometricBreakpoints.go (stop ratio cur w : ℚ) (fuel : ℕ) (acc : List ℚ) : List ℚ

Equations

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

def LeanCert.Engine.nonUniformPartition (I : Core.IntervalRat) (edgeWidth edgeRatio edgeCutoff : ℚ) (nMid : ℕ) (maxEdgeParts : ℕ := 200) : List Core.IntervalRat

Build a non-uniform partition: geometric near both edges, uniform in the middle. Returns List IntervalRat. Intervals with lo ≥ hi are dropped.

Equations

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