Taylor Model Integration

This module connects Taylor-model pointwise enclosures to certified interval enclosures for definite integrals.

The first bridge is deliberately conservative: it integrates the global Taylor-model range bound over the domain. This is enough to certify interval kernel banks and constant-factory observers today. Tighter polynomial-exact Taylor integration can be layered on top without changing this API.

The second bridge is the polynomial-exact enclosure shape used by certified quadrature: if the integral of the Taylor polynomial is known exactly, the only interval over-approximation comes from integrating the remainder interval.

noncomputable def LeanCert.Engine.TaylorModel.integrateShiftedPoly (p : Polynomial ℚ) (a b c : ℚ) : ℚ

Exact rational formula for integrating a shifted polynomial over [a,b].

This is the computational primitive for polynomial-exact Taylor quadrature:

∫ x in a..b, p(x-c) dx = Σ_i p_i ((b-c)^(i+1) - (a-c)^(i+1))/(i+1).

Equations

• LeanCert.Engine.TaylorModel.integrateShiftedPoly p a b c = ∑ i ∈ Finset.range (p.natDegree + 1), p.coeff i * (((b - c) ^ (i + 1) - (a - c) ^ (i + 1)) / (↑i + 1))

noncomputable def LeanCert.Engine.TaylorModel.integralBoundPolyExact (tm : TaylorModel) : Core.IntervalRat

Polynomial-exact integral enclosure for a Taylor model over its own domain.

The polynomial part is integrated exactly by integrateShiftedPoly; the remainder interval is scaled by the domain width.

Equations

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

noncomputable def LeanCert.Engine.TaylorModel.integralBoundCoarse (tm : TaylorModel) : Core.IntervalRat

Coarse integral enclosure for a Taylor model over its own domain.

If tm.bound = [lo, hi] contains all values of f on tm.domain, this interval is [width * lo, width * hi], expressed through the standard interval product.

Equations

• tm.integralBoundCoarse = (LeanCert.Core.IntervalRat.singleton tm.domain.width).mul tm.bound

theorem LeanCert.Engine.TaylorModel.integral_mem_bound_coarse (tm : TaylorModel) (f : ℝ → ℝ) (hf : ∀ x ∈ tm.domain, f x ∈ tm.evalSet x) (hInt : IntervalIntegrable f MeasureTheory.volume ↑tm.domain.lo ↑tm.domain.hi) : ∫ (x : ℝ) in ↑tm.domain.lo..↑tm.domain.hi, f x ∈ tm.integralBoundCoarse

Soundness of the coarse Taylor-model integral bound.

This theorem is intentionally phrased in terms of the Taylor-model semantic predicate evalSet, so any Taylor-model construction that proves ∀ x ∈ tm.domain, f x ∈ tm.evalSet x can immediately produce an integral certificate.

theorem LeanCert.Engine.TaylorModel.integral_mem_bound_polyExact_of_poly_integral (tm : TaylorModel) (f : ℝ → ℝ) (hf : ∀ x ∈ tm.domain, f x ∈ tm.evalSet x) (hInt : IntervalIntegrable f MeasureTheory.volume ↑tm.domain.lo ↑tm.domain.hi) (hPolyInt : IntervalIntegrable tm.evalPoly MeasureTheory.volume ↑tm.domain.lo ↑tm.domain.hi) (hPolyIntegral : ∫ (x : ℝ) in ↑tm.domain.lo..↑tm.domain.hi, tm.evalPoly x = ↑(integrateShiftedPoly tm.poly tm.domain.lo tm.domain.hi tm.center)) : ∫ (x : ℝ) in ↑tm.domain.lo..↑tm.domain.hi, f x ∈ tm.integralBoundPolyExact

Soundness of the polynomial-exact Taylor-model integral bound, assuming the Taylor polynomial integral has been identified with integrateShiftedPoly.

The assumption hPolyIntegral is intentionally explicit: the reusable numeric soundness theorem here is the interval/remainder part of Taylor quadrature, while callers may discharge the polynomial antiderivative equality using the best local polynomial API available for their representation.