Integration Certificates

This module provides certificate-driven verification for definite integrals using interval arithmetic with both computable (Core) and noncomputable (Checked) evaluation.

Main definitions

Computable Integration (Core)

• uniformPartitionCore - Computable uniform partition
• integrateInterval1Core - Single-interval integration
• integrateIntervalCore - Multi-partition integration
• checkIntegralBoundsCore - Boolean checker for integral bounds
• verify_integral_bound - Golden theorem for integration bounds

Integration with Inverse Support (Checked)

• integrateInterval1Checked - Single-interval integration with inv/log support
• integratePartitionChecked - Partitioned integration with inv/log support
• collectBoundsChecked - Collect bounds over partition

Adaptive Integration

• AdaptiveResultChecked - Result structure for adaptive integration
• integrateAdaptiveChecked - Adaptive integration with error tolerance
• checkIntegralAdaptiveLowerBound - Boolean checker for adaptive lower bounds
• checkIntegralAdaptiveUpperBound - Boolean checker for adaptive upper bounds

Exponential Search

• searchPartitionLower - Find minimum partitions for lower bound
• searchPartitionUpper - Find minimum partitions for upper bound
• searchPartitionLowerCandidate / searchPartitionUpperCandidate - retained untrusted search results with partition counts and enclosures
• checkIntegralPartitionLowerBound / checkIntegralPartitionUpperBound - fixed-candidate certificate checkers

Computable Integration Infrastructure

For the checked integral engine, we need:

1. A computable integration function using LeanCert.Internal.Rational.evalTotalCore1
2. A theorem that ExprSupportedCore implies IntervalIntegrable
3. A verification theorem linking the computation to the real integral

def LeanCert.Validity.Integration.uniformPartitionCore (I : Core.IntervalRat) (n : ℕ) (hn : 0 < n) : List Core.IntervalRat

Computable uniform partition using LeanCert.Internal.Rational.evalTotalCore1

Equations

• LeanCert.Validity.Integration.uniformPartitionCore 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 := ⋯ }

def LeanCert.Validity.Integration.sumIntervalBoundsCore (e : Core.Expr) (parts : List Core.IntervalRat) (cfg : Engine.EvalConfig) : Core.IntervalRat

Sum of interval bounds over a partition using computable LeanCert.Internal.Rational.evalTotalCore1

Equations

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

def LeanCert.Validity.Integration.integrateIntervalCore (e : Core.Expr) (I : Core.IntervalRat) (n : ℕ) (hn : 0 < n) (cfg : Engine.EvalConfig := default) : Core.IntervalRat

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

Equations

• LeanCert.Validity.Integration.integrateIntervalCore e I n hn cfg = LeanCert.Validity.Integration.sumIntervalBoundsCore e (LeanCert.Validity.Integration.uniformPartitionCore I n hn) cfg

def LeanCert.Validity.Integration.integrateInterval1Core (e : Core.Expr) (I : Core.IntervalRat) (cfg : Engine.EvalConfig := default) : Core.IntervalRat

For single-interval integration (n=1), computable version

Equations

• LeanCert.Validity.Integration.integrateInterval1Core e I cfg = (LeanCert.Core.IntervalRat.singleton I.width).mul (LeanCert.Internal.Rational.evalTotalCore1 e I cfg)

IntervalIntegrable from ExprSupportedCore

All ExprSupportedCore expressions are continuous, hence integrable on compact intervals.

theorem LeanCert.Validity.Integration.exprSupportedCore_intervalIntegrable (e : Core.Expr) (hsupp : Core.ExprSupportedCore e) (I : Core.IntervalRat) (hdom : Meta.exprContinuousDomainValid e (Set.Icc ↑I.lo ↑I.hi)) : IntervalIntegrable (fun (x : ℝ) => Core.Expr.eval (fun (x_1 : ℕ) => x) e) MeasureTheory.volume ↑I.lo ↑I.hi

All ExprSupportedCore expressions are interval integrable on any compact interval.

This follows because ExprSupportedCore expressions are continuous (see exprSupportedCore_continuousOn), and continuous functions on compact intervals are integrable.

Note: Requires domain validity for expressions with log.

Correctness of Computable Integration

theorem LeanCert.Validity.Integration.integrateInterval1Core_correct (e : Core.Expr) (hsupp : Core.ExprSupportedCore e) (I : Core.IntervalRat) (cfg : Engine.EvalConfig) (hdom : Engine.evalDomainValid1 e I cfg) (hcontdom : Meta.exprContinuousDomainValid e (Set.Icc ↑I.lo ↑I.hi)) : ∫ (x : ℝ) in ↑I.lo..↑I.hi, Core.Expr.eval (fun (x_1 : ℕ) => x) e ∈ integrateInterval1Core e I cfg

Single-interval integration correctness for ExprSupportedCore.

This is proved directly using the same structure as integrateInterval1_correct but with the computable LeanCert.Internal.Rational.evalTotalCore1 instead of noncomputable LeanCert.Internal.Rational.evalUnchecked1.

The hdom hypothesis ensures evaluation domain validity (e.g., log arguments have positive interval bounds). The hcontdom hypothesis ensures continuity domain validity (e.g., log arguments are positive on the set).

def LeanCert.Validity.Integration.checkIntegralBoundsCore (e : Core.Expr) (I : Core.IntervalRat) (target : ℚ) (cfg : Engine.EvalConfig := default) : Bool

Check if the integral bound contains a given rational value. Returns true if domain is valid and the computed integral bound contains the target value.

Equations

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

theorem LeanCert.Validity.Integration.verify_integral_bound (e : Core.Expr) (hsupp : Core.ExprSupportedCore e) (I : Core.IntervalRat) (_target : ℚ) (cfg : Engine.EvalConfig) (h_cert : checkIntegralBoundsCore e I _target cfg = true) (hcontdom : Meta.exprContinuousDomainValid e (Set.Icc ↑I.lo ↑I.hi)) : ∫ (x : ℝ) in ↑I.lo..↑I.hi, Core.Expr.eval (fun (x_1 : ℕ) => x) e ∈ integrateInterval1Core e I cfg

Golden Theorem for Integration Bounds

If checkIntegralBoundsCore e I target cfg = true, then the integral is bounded by the computed interval.

Note: The target parameter and h_cert hypothesis are used for the native_decide workflow where we verify at compile time that target is in the computed interval. The actual proof of interval membership uses integrateInterval1Core_correct directly.

This theorem allows proving statements like "∫_a^b f(x) dx ∈ [lo, hi]".

Note: Requires continuity domain validity for expressions with log.

def LeanCert.Validity.Integration.getIntegralBound (e : Core.Expr) (I : Core.IntervalRat) (cfg : Engine.EvalConfig := default) : Core.IntervalRat

Extract the computed integral bound as an interval

Equations

• LeanCert.Validity.Integration.getIntegralBound e I cfg = LeanCert.Validity.Integration.integrateInterval1Core e I cfg

theorem LeanCert.Validity.Integration.integral_in_bound (e : Core.Expr) (hsupp : Core.ExprSupportedCore e) (I : Core.IntervalRat) (cfg : Engine.EvalConfig) (hdom : Engine.evalDomainValid1 e I cfg) (hcontdom : Meta.exprContinuousDomainValid e (Set.Icc ↑I.lo ↑I.hi)) : ↑(getIntegralBound e I cfg).lo ≤ ∫ (x : ℝ) in ↑I.lo..↑I.hi, Core.Expr.eval (fun (x_1 : ℕ) => x) e ∧ ∫ (x : ℝ) in ↑I.lo..↑I.hi, Core.Expr.eval (fun (x_1 : ℕ) => x) e ≤ ↑(getIntegralBound e I cfg).hi

The integral lies within the computed bound (computable version)

Note: Requires continuity domain validity for expressions with log.

Single-interval integration for arbitrary expressions

def LeanCert.Validity.Integration.integrateInterval1Checked (e : Core.Expr) (I : Core.IntervalRat) : Option Core.IntervalRat

Computable single-interval integration using evalInterval?1. Returns none if interval evaluation fails (e.g., log domain invalid).

Equations

• LeanCert.Validity.Integration.integrateInterval1Checked e I = match LeanCert.Engine.evalInterval?1 e I with | some J => some ((LeanCert.Core.IntervalRat.singleton I.width).mul J) | none => none

theorem LeanCert.Validity.Integration.integrateInterval1Checked_correct (e : Core.Expr) (I bound : Core.IntervalRat) (hsome : integrateInterval1Checked e I = some bound) (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 ∈ bound

Single-interval integration correctness for arbitrary expressions. Requires that evalInterval?1 succeeds on the interval.

def LeanCert.Validity.Integration.checkIntegralBoundsChecked (e : Core.Expr) (I : Core.IntervalRat) (target : ℚ) : Bool

Check if the computed integration bound contains a target value. Returns false if interval evaluation fails.

Equations

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

theorem LeanCert.Validity.Integration.verify_integral_bound_checked (e : Core.Expr) (I : Core.IntervalRat) (_target : ℚ) (h_cert : checkIntegralBoundsChecked e I _target = true) (hInt : IntervalIntegrable (fun (x : ℝ) => Core.Expr.eval (fun (x_1 : ℕ) => x) e) MeasureTheory.volume ↑I.lo ↑I.hi) : ∃ (bound : Core.IntervalRat), integrateInterval1Checked e I = some bound ∧ ∫ (x : ℝ) in ↑I.lo..↑I.hi, Core.Expr.eval (fun (x_1 : ℕ) => x) e ∈ bound

Golden Theorem for Integration Bounds (Checked)

If checkIntegralBoundsChecked e I target = true, then the integral lies in the computed bound. The target parameter is for the native_decide workflow.

Partitioned integration for arbitrary expressions

def LeanCert.Validity.Integration.collectBoundsChecked (e : Core.Expr) (parts : List Core.IntervalRat) : Option (List Core.IntervalRat)

Collect per-subinterval bounds using evalInterval?1. Returns none if any subinterval fails.

Equations

• One or more equations did not get rendered due to their size.
• LeanCert.Validity.Integration.collectBoundsChecked e [] = some []

def LeanCert.Validity.Integration.integratePartitionChecked (e : Core.Expr) (I : Core.IntervalRat) (n : ℕ) : Option Core.IntervalRat

Sum bounds over a uniform partition using evalInterval?1.

Equations

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

theorem LeanCert.Validity.Integration.collectBoundsChecked_length (e : Core.Expr) (parts bounds : List Core.IntervalRat) : collectBoundsChecked e parts = some bounds → bounds.length = parts.length

theorem LeanCert.Validity.Integration.collectBoundsChecked_getElem (e : Core.Expr) (parts bounds : List Core.IntervalRat) (h : collectBoundsChecked e parts = some bounds) (i : ℕ) (hi : i < parts.length) : integrateInterval1Checked e parts[i] = some bounds[i]

theorem LeanCert.Validity.Integration.integral_subinterval_bounded_checked (e : Core.Expr) (I : Core.IntervalRat) (n : ℕ) (hn : 0 < n) (k : ℕ) (hk : k < n) (bound : Core.IntervalRat) (hsome : integrateInterval1Checked e (Engine.partitionInterval I n hn k hk) = some bound) (hInt : IntervalIntegrable (fun (x : ℝ) => Core.Expr.eval (fun (x_1 : ℕ) => x) e) MeasureTheory.volume ↑I.lo ↑I.hi) : ∫ (x : ℝ) in Engine.partitionPoints I n k..Engine.partitionPoints I n (k + 1), Core.Expr.eval (fun (x_1 : ℕ) => x) e ∈ bound

theorem LeanCert.Validity.Integration.integratePartitionChecked_correct (e : Core.Expr) (I : Core.IntervalRat) (n : ℕ) (hn : 0 < n) (bound : Core.IntervalRat) (hsome : integratePartitionChecked e I n = some bound) (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 ∈ bound

Adaptive Integration for arbitrary expressions

Adaptive integration concentrates partitions where the error is high (near singularities), dramatically reducing the number of function evaluations compared to uniform partitioning.

The algorithm:

1. Compute a refined bound (n=2) on the current interval
2. If error (width of bound) is below tolerance, return
3. Otherwise, split at midpoint and recurse with half tolerance
4. Sum the bounds from sub-intervals

This naturally concentrates partitions near singularities where the function varies rapidly.

structure LeanCert.Validity.Integration.AdaptiveResultChecked : Type

Result of adaptive integration with inverse support

• bound : Core.IntervalRat

  Interval containing the integral

• partitions : ℕ

  Number of subintervals used

@[instance_reducible]

instance LeanCert.Validity.Integration.instReprAdaptiveResultChecked : Repr AdaptiveResultChecked

Equations

• LeanCert.Validity.Integration.instReprAdaptiveResultChecked = { reprPrec := LeanCert.Validity.Integration.instReprAdaptiveResultChecked.repr }

def LeanCert.Validity.Integration.instReprAdaptiveResultChecked.repr : AdaptiveResultChecked → ℕ → Std.Format

Equations

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

def LeanCert.Validity.Integration.adaptiveErrorEstimate (bound : Core.IntervalRat) : ℚ

Error estimate for adaptive integration: width of the refined bound

Equations

• LeanCert.Validity.Integration.adaptiveErrorEstimate bound = bound.width

def LeanCert.Validity.Integration.integrateRefinedChecked (e : Core.Expr) (I : Core.IntervalRat) : Option Core.IntervalRat

Compute a refined bound (n=2) on a single interval using Checked support. Returns none if evaluation fails (domain issues).

Equations

• LeanCert.Validity.Integration.integrateRefinedChecked e I = LeanCert.Validity.Integration.integratePartitionChecked e I 2

def LeanCert.Validity.Integration.integrateAdaptiveAuxChecked (e : Core.Expr) (I : Core.IntervalRat) (tol : ℚ) (maxDepth : ℕ) : Option AdaptiveResultChecked

Recursive adaptive integration with inverse support. 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.

def LeanCert.Validity.Integration.integrateAdaptiveChecked (e : Core.Expr) (I : Core.IntervalRat) (tol : ℚ) (maxDepth : ℕ) : Option AdaptiveResultChecked

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

Equations

• LeanCert.Validity.Integration.integrateAdaptiveChecked e I tol maxDepth = LeanCert.Validity.Integration.integrateAdaptiveAuxChecked e I tol maxDepth

Correctness proofs for adaptive integration with inverse support

theorem LeanCert.Validity.Integration.integrateRefinedChecked_correct (e : Core.Expr) (I bound : Core.IntervalRat) (hsome : integrateRefinedChecked e I = some bound) (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 ∈ bound

integrateRefinedChecked is correct (direct from integratePartitionChecked_correct)

theorem LeanCert.Validity.Integration.intervalIntegrable_splitMid_left_checked (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 ↑(Engine.splitMid I).1.lo ↑(Engine.splitMid I).1.hi

Integrability on left half after midpoint split

theorem LeanCert.Validity.Integration.intervalIntegrable_splitMid_right_checked (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 ↑(Engine.splitMid I).2.lo ↑(Engine.splitMid I).2.hi

Integrability on right half after midpoint split

theorem LeanCert.Validity.Integration.integral_split_mid_checked (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

Integral over split interval equals sum of integrals over halves

theorem LeanCert.Validity.Integration.integrateAdaptiveAuxChecked_correct (e : Core.Expr) (I : Core.IntervalRat) (tol : ℚ) (maxDepth : ℕ) (result : AdaptiveResultChecked) (hsome : integrateAdaptiveAuxChecked e I tol maxDepth = some result) (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 ∈ result.bound

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

theorem LeanCert.Validity.Integration.integrateAdaptiveChecked_correct (e : Core.Expr) (I : Core.IntervalRat) (tol : ℚ) (maxDepth : ℕ) (result : AdaptiveResultChecked) (hsome : integrateAdaptiveChecked e I tol maxDepth = some result) (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 ∈ result.bound

Soundness of the main adaptive integration function with inverse support

Adaptive integral bound checkers for native_decide

def LeanCert.Validity.Integration.checkIntegralAdaptiveLowerBound (e : Core.Expr) (I : Core.IntervalRat) (tol : ℚ) (maxDepth : ℕ) (c : ℚ) : Bool

Boolean checker for adaptive integral lower bounds. More efficient than uniform partitioning for functions with singularities.

Equations

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

def LeanCert.Validity.Integration.checkIntegralAdaptiveUpperBound (e : Core.Expr) (I : Core.IntervalRat) (tol : ℚ) (maxDepth : ℕ) (c : ℚ) : Bool

Boolean checker for adaptive integral upper bounds. More efficient than uniform partitioning for functions with singularities.

Equations

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

theorem LeanCert.Validity.Integration.integral_adaptive_lower_of_check (e : Core.Expr) (I : Core.IntervalRat) (tol : ℚ) (maxDepth : ℕ) (c : ℚ) (hcheck : checkIntegralAdaptiveLowerBound e I tol maxDepth c = true) (hInt : IntervalIntegrable (fun (x : ℝ) => Core.Expr.eval (fun (x_1 : ℕ) => x) e) MeasureTheory.volume ↑I.lo ↑I.hi) : ↑c ≤ ∫ (x : ℝ) in ↑I.lo..↑I.hi, Core.Expr.eval (fun (x_1 : ℕ) => x) e

Bridge theorem: if checkIntegralAdaptiveLowerBound returns true, the integral is ≥ c.

theorem LeanCert.Validity.Integration.integral_adaptive_upper_of_check (e : Core.Expr) (I : Core.IntervalRat) (tol : ℚ) (maxDepth : ℕ) (c : ℚ) (hcheck : checkIntegralAdaptiveUpperBound e I tol maxDepth c = true) (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 ≤ ↑c

Bridge theorem: if checkIntegralAdaptiveUpperBound returns true, the integral is ≤ c.

Exponential Search for Optimal Partition Count

Instead of using a fixed large N or deep adaptive recursion, we can search for the minimum partition count that achieves the desired bound. This is often much faster because many integrals only need N=100-500 instead of N=3000.

Algorithm:

1. Start with N=startN (e.g., 32)
2. Double N until the bound is achieved (exponential search)
3. Return the first N that works

This finds the optimal N in O(log(N)) integration attempts.

inductive LeanCert.Validity.Integration.IntegralPartitionSearchResult : Type

Retained result of the untrusted exponential partition search. The selected partition count is certified separately by a fixed-candidate checker, so the search itself never needs to be executed by the verifier.

• success (partitions : ℕ) (enclosure : Core.IntervalRat) (attempts : ℕ) : IntegralPartitionSearchResult
• exhausted (lastPartitions : Option ℕ) (lastEnclosure : Option Core.IntervalRat) (attempts : ℕ) : IntegralPartitionSearchResult
• domainObstruction (partitions attempts : ℕ) : IntegralPartitionSearchResult
• invalidStart : IntegralPartitionSearchResult

def LeanCert.Validity.Integration.instReprIntegralPartitionSearchResult.repr : IntegralPartitionSearchResult → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance LeanCert.Validity.Integration.instReprIntegralPartitionSearchResult : Repr IntegralPartitionSearchResult

Equations

• LeanCert.Validity.Integration.instReprIntegralPartitionSearchResult = { reprPrec := LeanCert.Validity.Integration.instReprIntegralPartitionSearchResult.repr }

@[instance_reducible]

instance LeanCert.Validity.Integration.instInhabitedIntegralPartitionSearchResult : Inhabited IntegralPartitionSearchResult

Equations

• LeanCert.Validity.Integration.instInhabitedIntegralPartitionSearchResult = { default := LeanCert.Validity.Integration.instInhabitedIntegralPartitionSearchResult.default }

def LeanCert.Validity.Integration.searchPartitionLowerCandidateAux (e : Core.Expr) (I : Core.IntervalRat) (n maxN : ℕ) (c : ℚ) (fuel attempts : ℕ) (lastPartitions : Option ℕ := none) (lastEnclosure : Option Core.IntervalRat := none) : IntegralPartitionSearchResult

Structured exponential search for a lower integral bound. This function is candidate generation only; soundness comes from checkIntegralPartitionLowerBound below.

Equations

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

def LeanCert.Validity.Integration.searchPartitionUpperCandidateAux (e : Core.Expr) (I : Core.IntervalRat) (n maxN : ℕ) (c : ℚ) (fuel attempts : ℕ) (lastPartitions : Option ℕ := none) (lastEnclosure : Option Core.IntervalRat := none) : IntegralPartitionSearchResult

Structured exponential search for an upper integral bound.

Equations

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

def LeanCert.Validity.Integration.searchPartitionLowerCandidate (e : Core.Expr) (I : Core.IntervalRat) (startN maxN : ℕ) (c : ℚ) : IntegralPartitionSearchResult

Equations

• LeanCert.Validity.Integration.searchPartitionLowerCandidate e I startN maxN c = LeanCert.Validity.Integration.searchPartitionLowerCandidateAux e I startN maxN c 20 0

def LeanCert.Validity.Integration.searchPartitionUpperCandidate (e : Core.Expr) (I : Core.IntervalRat) (startN maxN : ℕ) (c : ℚ) : IntegralPartitionSearchResult

Equations

• LeanCert.Validity.Integration.searchPartitionUpperCandidate e I startN maxN c = LeanCert.Validity.Integration.searchPartitionUpperCandidateAux e I startN maxN c 20 0

def LeanCert.Validity.Integration.checkIntegralPartitionLowerBound (e : Core.Expr) (I : Core.IntervalRat) (partitions : ℕ) (c : ℚ) : Bool

Fixed-candidate checker for an integral lower bound.

Equations

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

def LeanCert.Validity.Integration.checkIntegralPartitionUpperBound (e : Core.Expr) (I : Core.IntervalRat) (partitions : ℕ) (c : ℚ) : Bool

Fixed-candidate checker for an integral upper bound.

Equations

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

theorem LeanCert.Validity.Integration.integral_partition_lower_of_check (e : Core.Expr) (I : Core.IntervalRat) (partitions : ℕ) (hpartitions : 0 < partitions) (c : ℚ) (hcheck : checkIntegralPartitionLowerBound e I partitions c = true) (hInt : IntervalIntegrable (fun (x : ℝ) => Core.Expr.eval (fun (x_1 : ℕ) => x) e) MeasureTheory.volume ↑I.lo ↑I.hi) : ↑c ≤ ∫ (x : ℝ) in ↑I.lo..↑I.hi, Core.Expr.eval (fun (x_1 : ℕ) => x) e

Golden theorem for a retained lower-bound partition candidate.

theorem LeanCert.Validity.Integration.integral_partition_upper_of_check (e : Core.Expr) (I : Core.IntervalRat) (partitions : ℕ) (hpartitions : 0 < partitions) (c : ℚ) (hcheck : checkIntegralPartitionUpperBound e I partitions c = true) (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 ≤ ↑c

Golden theorem for a retained upper-bound partition candidate.

def LeanCert.Validity.Integration.searchPartitionLowerAux (e : Core.Expr) (I : Core.IntervalRat) (n maxN : ℕ) (c : ℚ) (fuel : ℕ) : Option Core.IntervalRat

Exponential search with explicit fuel for termination. Returns the computed bound if found within fuel doublings, or none otherwise.

Equations

• One or more equations did not get rendered due to their size.
• LeanCert.Validity.Integration.searchPartitionLowerAux e I n maxN c 0 = none

def LeanCert.Validity.Integration.searchPartitionLower (e : Core.Expr) (I : Core.IntervalRat) (startN maxN : ℕ) (c : ℚ) : Option Core.IntervalRat

Exponential search for minimum partition count that achieves a lower bound.

Equations

• LeanCert.Validity.Integration.searchPartitionLower e I startN maxN c = LeanCert.Validity.Integration.searchPartitionLowerAux e I startN maxN c 20

def LeanCert.Validity.Integration.searchPartitionUpperAux (e : Core.Expr) (I : Core.IntervalRat) (n maxN : ℕ) (c : ℚ) (fuel : ℕ) : Option Core.IntervalRat

Exponential search with explicit fuel for upper bounds.

Equations

• One or more equations did not get rendered due to their size.
• LeanCert.Validity.Integration.searchPartitionUpperAux e I n maxN c 0 = none

def LeanCert.Validity.Integration.searchPartitionUpper (e : Core.Expr) (I : Core.IntervalRat) (startN maxN : ℕ) (c : ℚ) : Option Core.IntervalRat

Exponential search for minimum partition count that achieves an upper bound.

Equations

• LeanCert.Validity.Integration.searchPartitionUpper e I startN maxN c = LeanCert.Validity.Integration.searchPartitionUpperAux e I startN maxN c 20

def LeanCert.Validity.Integration.checkIntegralSearchLowerBound (e : Core.Expr) (I : Core.IntervalRat) (startN maxN : ℕ) (c : ℚ) : Bool

Check lower bound using exponential search to find optimal N. Much faster than fixed large N when fewer partitions suffice. startN: initial partition count (e.g., 32) maxN: maximum partitions to try (e.g., 8192)

Equations

• LeanCert.Validity.Integration.checkIntegralSearchLowerBound e I startN maxN c = (LeanCert.Validity.Integration.searchPartitionLower e I startN maxN c).isSome

def LeanCert.Validity.Integration.checkIntegralSearchUpperBound (e : Core.Expr) (I : Core.IntervalRat) (startN maxN : ℕ) (c : ℚ) : Bool

Check upper bound using exponential search to find optimal N.

Equations

• LeanCert.Validity.Integration.checkIntegralSearchUpperBound e I startN maxN c = (LeanCert.Validity.Integration.searchPartitionUpper e I startN maxN c).isSome

theorem LeanCert.Validity.Integration.searchPartitionLowerAux_spec (e : Core.Expr) (I : Core.IntervalRat) (n maxN : ℕ) (c : ℚ) (fuel : ℕ) (J : Core.IntervalRat) (hfind : searchPartitionLowerAux e I n maxN c fuel = some J) : c ≤ J.lo

Helper: if searchPartitionLowerAux succeeds, the result satisfies the bound.

theorem LeanCert.Validity.Integration.searchPartitionUpperAux_spec (e : Core.Expr) (I : Core.IntervalRat) (n maxN : ℕ) (c : ℚ) (fuel : ℕ) (J : Core.IntervalRat) (hfind : searchPartitionUpperAux e I n maxN c fuel = some J) : J.hi ≤ c

Helper: if searchPartitionUpperAux succeeds, the result satisfies the bound.

theorem LeanCert.Validity.Integration.searchPartitionLowerAux_valid (e : Core.Expr) (I : Core.IntervalRat) (n maxN : ℕ) (_hn : 0 < n) (c : ℚ) (fuel : ℕ) (J : Core.IntervalRat) (hfind : searchPartitionLowerAux e I n maxN c fuel = some J) (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 ∈ J

Helper: searchPartitionLowerAux returns a valid integration bound.

theorem LeanCert.Validity.Integration.searchPartitionUpperAux_valid (e : Core.Expr) (I : Core.IntervalRat) (n maxN : ℕ) (_hn : 0 < n) (c : ℚ) (fuel : ℕ) (J : Core.IntervalRat) (hfind : searchPartitionUpperAux e I n maxN c fuel = some J) (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 ∈ J

Helper: searchPartitionUpperAux returns a valid integration bound.

theorem LeanCert.Validity.Integration.integral_search_lower_of_check (e : Core.Expr) (I : Core.IntervalRat) (startN maxN : ℕ) (hstart : 0 < startN) (c : ℚ) (hcheck : checkIntegralSearchLowerBound e I startN maxN c = true) (hInt : IntervalIntegrable (fun (x : ℝ) => Core.Expr.eval (fun (x_1 : ℕ) => x) e) MeasureTheory.volume ↑I.lo ↑I.hi) : ↑c ≤ ∫ (x : ℝ) in ↑I.lo..↑I.hi, Core.Expr.eval (fun (x_1 : ℕ) => x) e

Bridge theorem: if exponential search succeeds, the integral satisfies the lower bound.

theorem LeanCert.Validity.Integration.integral_search_upper_of_check (e : Core.Expr) (I : Core.IntervalRat) (startN maxN : ℕ) (hstart : 0 < startN) (c : ℚ) (hcheck : checkIntegralSearchUpperBound e I startN maxN c = true) (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 ≤ ↑c

Bridge theorem: if exponential search succeeds, the integral satisfies the upper bound.