API REFERENCE/omnibias-core

omnibias.core.verified.euler_maclaurin

0.5.0rc1Release candidatePython >=3.10Apache-2.0

Coefficient recurrences, activation contracts, jet algebra, and verified arithmetic shared by the numerical backends.

import omnibias.core.verified.euler_maclaurin

Module contract & mathematical conventions

Certified Euler-Maclaurin summation and the special functions it yields.

Euler-Maclaurin is *exactly* the composition this repo already owns: the exact Bernoulli numbers (omnibias.core.verified.coeffs.bernoulli_number_exact, read off the closed-form tanh tower) weighting high-order derivative enclosures, closed with a **rigorous** remainder. For p correction terms,

\sum_{k=a}^{b} f(k) = \int_a^b f + \tfrac12\,(f(a) + f(b)) + \sum_{j=1}^{p} \frac{B_{2j}}{(2j)!}\,\bigl(f^{(2j-1)}(b) - f^{(2j-1)}(a)\bigr) + R_p,

with the standard bound (max_{[0,1]} |\tilde B_{2p}| = |B_{2p}|)

|R_p| \le \frac{|B_{2p}|}{(2p)!}\int_a^b |f^{(2p)}(x)|\,dx \le \frac{|B_{2p}|}{(2p)!}\,(b-a)\,\max_{[a,b]}|f^{(2p)}|.

euler_maclaurin_sum takes a caller-supplied derivative-enclosure oracle f^{(k)} (any function enclosable over an interval -- not just the activation dictionary) plus a certified enclosure of \int_a^b f and returns a guaranteed enclosure of the finite sum. log_gamma_iv and digamma_iv are the special functions this unlocks: Stirling / asymptotic series with a remainder enclosed by the classical *first-omitted-term* bound (valid on the positive real axis), tightened by shifting the argument up via the Gamma / psi recurrences. Everything is **closed-form + numerical** honest: the coefficients are exact, the enclosures outward-rounded, the remainder rigorously bounded.

Shared formulas do not imply universal floating-point identity. Verify dtype, shape, derivative-order support, and the stated numerical assumptions for the path you use.

Module source ↗Source revision 9a2d73df0573Running reference examples →

CONSTANT

DerivativeOracle

omnibias.core.verified.euler_maclaurin.DerivativeOracleSource ↗

DerivativeOracle = Callable[[int, Interval], Interval]

A derivative-enclosure oracle: deriv(k, x) encloses f^{(k)} over x.

Read the implementation

DerivativeOracle = Callable[[int, Interval], Interval]

FUNCTION

digamma_iv

omnibias.core.verified.digamma_ivSource ↗

digamma_iv(x: Interval, *, terms: int=6, shift_to: float=8.0) -> Interval

Guaranteed enclosure of the digamma psi(x) for a strictly positive x.

Shifted up via psi(x) = psi(x + n) - sum_{k=0}^{n-1} 1/(x + k) before the asymptotic series, mirroring log_gamma_iv.

Parameters

Name	Type & default	Contract
xpositional-or-keyword	IntervalRequired	See the operation contract and implementation below.
termskeyword-only	intDefault: 6	See the operation contract and implementation below.
shift_tokeyword-only	floatDefault: 8.0	See the operation contract and implementation below.

ReturnsInterval

Explicit validation & failure cases

• When x.lo <= 0.0, raises ValueError('digamma_iv requires a strictly positive interval').
• When terms < 1, raises ValueError(f'terms must be >= 1, got {terms}').

These are explicit source guards. Backend operations may also raise for invalid shapes, dtypes, or unsupported devices.

Executed regression · digamma encloses mpmath grid and random

Recorded coverage confirms this test executed the API body. This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.

Full file, imports & fixtures ↗

def test_digamma_encloses_mpmath_grid_and_random() -> None:
    mp = pytest.importorskip("mpmath")
    for seed in _SEEDS:
        for x in _grid_and_random(0.4, 6.0, seed):
            enc = digamma_iv(Interval.point(x))
            with mp.workdps(40):
                true = float(mp.digamma(x))
            assert enc.lo <= true <= enc.hi, (x, enc, true)
            assert enc.width < 1e-8

python -m pytest "packages/omnibias-core/tests/verified/test_euler_maclaurin.py::test_digamma_encloses_mpmath_grid_and_random" -q

Regression example · log gamma known values

This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.

Full file, imports & fixtures ↗

def test_log_gamma_known_values() -> None:
    for x, val in ((1.0, 0.0), (2.0, 0.0), (5.0, math.log(24.0))):
        enc = log_gamma_iv(Interval.point(x))
        assert enc.lo <= val <= enc.hi

python -m pytest packages/omnibias-core/tests/verified/test_euler_maclaurin.py -k test_log_gamma_known_values -q

Read the implementation

def digamma_iv(x: Interval, *, terms: int = 6, shift_to: float = 8.0) -> Interval:
    r"""Guaranteed enclosure of the digamma ``psi(x)`` for a strictly positive ``x``.

    Shifted up via ``psi(x) = psi(x + n) - sum_{k=0}^{n-1} 1/(x + k)`` before the
    asymptotic series, mirroring :func:`log_gamma_iv`.
    """
    if x.lo <= 0.0:
        raise ValueError("digamma_iv requires a strictly positive interval")
    if terms < 1:
        raise ValueError(f"terms must be >= 1, got {terms}")
    n = _shift_count(x.lo, shift_to)
    shift = Interval.point(0.0)
    for k in range(n):
        shift = shift + (x + Interval.from_rational(k)).reciprocal()
    w = x + Interval.from_rational(n)
    return _stirling_digamma(w, terms) - shift

Other public import paths

• omnibias.core.verified.digamma_iv
• omnibias.core.verified.euler_maclaurin.digamma_iv

FUNCTION

euler_maclaurin_sum

omnibias.core.verified.euler_maclaurin_sumSource ↗

euler_maclaurin_sum(deriv: DerivativeOracle, integral: Interval, a: int, b: int, *, terms: int) -> Interval

Guaranteed enclosure of sum_{k=a}^{b} f(k) via Euler-Maclaurin.

Parameters

deriv: Oracle returning a guaranteed enclosure of f^{(k)} over an interval; deriv(0, x) is f itself. It must accept a *box* argument (used to bound f^{(2*terms)} over [a, b] for the remainder). integral: A guaranteed enclosure of \int_a^b f(x) dx (the caller supplies it in closed form, e.g. for a p-series or a log term). a, b: Integer summation limits, inclusive, with a <= b. terms: The number p >= 1 of Bernoulli correction pairs; the remainder uses f^{(2p)}.

Parameters

Name	Type & default	Contract
derivpositional-or-keyword	DerivativeOracleRequired	Oracle returning a guaranteed enclosure of f^{(k)} over an interval; deriv(0, x) is f itself. It must accept a *box* argument (used to bound f^{(2*terms)} over [a, b] for the remainder).
integralpositional-or-keyword	IntervalRequired	A guaranteed enclosure of \int_a^b f(x) dx (the caller supplies it in closed form, e.g. for a p-series or a log term).
apositional-or-keyword	intRequired	Integer summation limits, inclusive, with a <= b.
bpositional-or-keyword	intRequired	See the operation contract and implementation below.
termskeyword-only	intRequired	The number p >= 1 of Bernoulli correction pairs; the remainder uses f^{(2p)}.

ReturnsInterval

Explicit validation & failure cases

• When b < a, raises ValueError(f'require a <= b, got a={a}, b={b}').
• When terms < 1, raises ValueError(f'terms (p) must be >= 1, got {terms}').

These are explicit source guards. Backend operations may also raise for invalid shapes, dtypes, or unsupported devices.

Executed regression · euler maclaurin sum validates arguments

Recorded coverage confirms this test executed the API body. This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.

Full file, imports & fixtures ↗

def test_euler_maclaurin_sum_validates_arguments() -> None:
    def deriv(k: int, x: Interval) -> Interval:
        return x

    with pytest.raises(ValueError, match="a <= b"):
        euler_maclaurin_sum(deriv, Interval.point(0.0), 5, 1, terms=2)
    with pytest.raises(ValueError, match="terms"):
        euler_maclaurin_sum(deriv, Interval.point(0.0), 1, 5, terms=0)

python -m pytest "packages/omnibias-core/tests/verified/test_euler_maclaurin.py::test_euler_maclaurin_sum_validates_arguments" -q

Regression example · euler maclaurin sum encloses exact p series

This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.

Full file, imports & fixtures ↗

def test_euler_maclaurin_sum_encloses_exact_p_series() -> None:
    # f(x) = x^-2, so f^(k)(x) = (-1)^k (k+1)! x^-(k+2); integral_a^b = 1/a - 1/b.
    def deriv(k: int, x: Interval) -> Interval:
        coeff = Interval.from_rational(Fraction((-1) ** k * math.factorial(k + 1)))
        return coeff * x.pow_int(k + 2).reciprocal()

    a, b = 4, 30
    integral = Interval.from_rational(Fraction(1, a) - Fraction(1, b))
    enc = euler_maclaurin_sum(deriv, integral, a, b, terms=4)
    exact = float(sum(Fraction(1, k * k) for k in range(a, b + 1)))
    assert enc.lo <= exact <= enc.hi
    assert enc.width < 1e-4  # tight: Euler-Maclaurin, not a huge remainder

python -m pytest packages/omnibias-core/tests/verified/test_euler_maclaurin.py -k test_euler_maclaurin_sum_encloses_exact_p_series -q

Read the implementation

def euler_maclaurin_sum(
    deriv: DerivativeOracle,
    integral: Interval,
    a: int,
    b: int,
    *,
    terms: int,
) -> Interval:
    r"""Guaranteed enclosure of ``sum_{k=a}^{b} f(k)`` via Euler-Maclaurin.

    Parameters
    ----------
    deriv:
        Oracle returning a guaranteed enclosure of ``f^{(k)}`` over an interval;
        ``deriv(0, x)`` is ``f`` itself. It must accept a *box* argument (used to
        bound ``f^{(2*terms)}`` over ``[a, b]`` for the remainder).
    integral:
        A guaranteed enclosure of ``\int_a^b f(x) dx`` (the caller supplies it in
        closed form, e.g. for a ``p``-series or a log term).
    a, b:
        Integer summation limits, inclusive, with ``a <= b``.
    terms:
        The number ``p >= 1`` of Bernoulli correction pairs; the remainder uses
        ``f^{(2p)}``.
    """
    if b < a:
        raise ValueError(f"require a <= b, got a={a}, b={b}")
    if terms < 1:
        raise ValueError(f"terms (p) must be >= 1, got {terms}")

    a_iv = Interval.from_rational(a)
    b_iv = Interval.from_rational(b)
    total = integral + (deriv(0, a_iv) + deriv(0, b_iv)) * _HALF

    for j in range(1, terms + 1):
        coeff = Interval.from_rational(bernoulli_number_exact(2 * j) / factorial(2 * j))
        total = total + coeff * (deriv(2 * j - 1, b_iv) - deriv(2 * j - 1, a_iv))

    # Remainder: |R_p| <= |B_{2p}|/(2p)! * (b - a) * max_[a,b] |f^{(2p)}|.
    box = Interval(float(a), float(b))
    f2p = deriv(2 * terms, box)
    bound_iv = (
        Interval.from_rational(abs(bernoulli_number_exact(2 * terms)) / factorial(2 * terms))
        * Interval.from_rational(b - a)
        * Interval.point(f2p.mag)
    )
    bound = bound_iv.hi
    return total + Interval(-bound, bound)

Related APIsomnibias.core.verified.bernoulli_number_exact↗omnibias.core.verified.Interval↗

Other public import paths

• omnibias.core.verified.euler_maclaurin_sum
• omnibias.core.verified.euler_maclaurin.euler_maclaurin_sum

FUNCTION

log_gamma_iv

omnibias.core.verified.log_gamma_ivSource ↗

log_gamma_iv(x: Interval, *, terms: int=6, shift_to: float=8.0) -> Interval

Guaranteed enclosure of ln Gamma(x) for a strictly positive interval x.

The argument is shifted up to >= shift_to via ln Gamma(x) = ln Gamma(x + n) - sum_{k=0}^{n-1} ln(x + k) so the Stirling series is tight, then _stirling_log_gamma closes it with a rigorous remainder. Increase terms / shift_to to tighten.

Parameters

Name	Type & default	Contract
xpositional-or-keyword	IntervalRequired	See the operation contract and implementation below.
termskeyword-only	intDefault: 6	See the operation contract and implementation below.
shift_tokeyword-only	floatDefault: 8.0	See the operation contract and implementation below.

ReturnsInterval

Explicit validation & failure cases

• When x.lo <= 0.0, raises ValueError('log_gamma_iv requires a strictly positive interval').
• When terms < 1, raises ValueError(f'terms must be >= 1, got {terms}').

These are explicit source guards. Backend operations may also raise for invalid shapes, dtypes, or unsupported devices.

Executed regression · log gamma rejects nonpositive

Recorded coverage confirms this test executed the API body. This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.

Full file, imports & fixtures ↗

def test_log_gamma_rejects_nonpositive() -> None:
    with pytest.raises(ValueError, match="strictly positive"):
        log_gamma_iv(Interval(-1.0, 1.0))

python -m pytest "packages/omnibias-core/tests/verified/test_euler_maclaurin.py::test_log_gamma_rejects_nonpositive" -q

Regression example · log gamma known values

This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.

Full file, imports & fixtures ↗

def test_log_gamma_known_values() -> None:
    for x, val in ((1.0, 0.0), (2.0, 0.0), (5.0, math.log(24.0))):
        enc = log_gamma_iv(Interval.point(x))
        assert enc.lo <= val <= enc.hi

python -m pytest packages/omnibias-core/tests/verified/test_euler_maclaurin.py -k test_log_gamma_known_values -q

Read the implementation

def log_gamma_iv(x: Interval, *, terms: int = 6, shift_to: float = 8.0) -> Interval:
    r"""Guaranteed enclosure of ``ln Gamma(x)`` for a strictly positive interval ``x``.

    The argument is shifted up to ``>= shift_to`` via
    ``ln Gamma(x) = ln Gamma(x + n) - sum_{k=0}^{n-1} ln(x + k)`` so the Stirling
    series is tight, then :func:`_stirling_log_gamma` closes it with a rigorous
    remainder. Increase ``terms`` / ``shift_to`` to tighten.
    """
    if x.lo <= 0.0:
        raise ValueError("log_gamma_iv requires a strictly positive interval")
    if terms < 1:
        raise ValueError(f"terms must be >= 1, got {terms}")
    n = _shift_count(x.lo, shift_to)
    shift = Interval.point(0.0)
    for k in range(n):
        shift = shift + ln_iv(x + Interval.from_rational(k))
    w = x + Interval.from_rational(n)
    return _stirling_log_gamma(w, terms) - shift

Related APIsomnibias.core.verified.ln_iv↗

Other public import paths

• omnibias.core.verified.log_gamma_iv
• omnibias.core.verified.euler_maclaurin.log_gamma_iv

← Package overviewRunnable learning examples →