omnibias.core.verified.series

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.series

Module contract & mathematical conventions

Certified series summation -- the verified Sigma operator.

omnibias's closed-form derivative tower, the Wilson-plaquette character / cluster expansion, and Neumann series are all *series*; turning a truncated float sum into a theorem-grade enclosure needs a rigorous bound on the omitted tail. This module supplies that bound for the geometric-majorant case -- exactly the situation of a convergent expansion with a proven consecutive-ratio bound |a_{n+1} / a_n| <= q < 1 valid past the truncation index.

Given such a rigorous q (an Interval with q.hi < 1) the omitted tail of a series truncated after a_N obeys

\Bigl| \sum_{k \ge 1} a_{N+k} \Bigr| \le |a_N| \sum_{k \ge 1} q^{k} = \frac{|a_N|\, q}{1 - q},

an outward-rounded Interval. The full sum is the interval sum of the retained terms plus that symmetric tail enclosure. Nothing here assumes a sign pattern: the bound is on the *absolute* tail, so it is valid for sign-indefinite series too. geometric_series_closed_form gives the analytic limit a / (1 - r) of a pure geometric series, the ground truth a certified partial sum must enclose.

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 →

FUNCTION

certified_geometric_series_sum

omnibias.core.verified.certified_geometric_series_sumSource ↗

certified_geometric_series_sum(terms: Sequence[IntervalLike], ratio: IntervalLike) -> Interval

Enclosure of sum_{n>=0} a_n from retained terms a_0..a_N and a tail.

terms are enclosures of the retained terms a_0, ..., a_N; ratio is a rigorous magnitude bound q (0 <= q < 1) on every *omitted* consecutive ratio. The result is sum(terms) + geometric_tail_enclosure(terms[-1], q).

The caller is responsible for q being an a-priori rigorous bound (e.g. the convergence ratio of a character expansion); this routine does not infer it from the retained terms.

Parameters

Name	Type & default	Contract
`terms`positional-or-keyword	`Sequence[IntervalLike]`Required	See the operation contract and implementation below.
`ratio`positional-or-keyword	`IntervalLike`Required	See the operation contract and implementation below.

ReturnsInterval

Explicit validation & failure cases

When not ivs, raises ValueError('certified_geometric_series_sum needs >= 1 retained term').

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

Executed regression · certified sum encloses sign indefinite series

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_certified_sum_encloses_sign_indefinite_series() -> None:
    # a_n = (-0.3)^n ; |a_{n+1}/a_n| = 0.3
    terms = [Interval.point((-0.3) ** n) for n in range(7)]
    enc = certified_geometric_series_sum(terms, 0.3)
    assert enc.lo <= 1.0 / 1.3 <= enc.hi

python -m pytest "packages/omnibias-core/tests/verified/test_series.py::test_certified_sum_encloses_sign_indefinite_series" -q

Regression example · certified sum encloses positive 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_certified_sum_encloses_positive_series() -> None:
    terms = [Interval.point(0.5**n) for n in range(10)]
    enc = certified_geometric_series_sum(terms, 0.5)
    assert enc.lo <= 2.0 <= enc.hi
    # retained 10 terms + tail; still a genuine (finite-width) bracket
    assert enc.width < 1e-2

python -m pytest packages/omnibias-core/tests/verified/test_series.py -k test_certified_sum_encloses_positive_series -q

Read the implementation

def certified_geometric_series_sum(
    terms: Sequence[IntervalLike], ratio: IntervalLike
) -> Interval:
    r"""Enclosure of ``sum_{n>=0} a_n`` from retained terms ``a_0..a_N`` and a tail.

    ``terms`` are enclosures of the retained terms ``a_0, ..., a_N``; ``ratio`` is
    a rigorous magnitude bound ``q`` (``0 <= q < 1``) on every *omitted*
    consecutive ratio.  The result is
    ``sum(terms) + geometric_tail_enclosure(terms[-1], q)``.

    The caller is responsible for ``q`` being an a-priori rigorous bound (e.g. the
    convergence ratio of a character expansion); this routine does not infer it
    from the retained terms.
    """
    ivs = [Interval.from_value(t) for t in terms]
    if not ivs:
        raise ValueError("certified_geometric_series_sum needs >= 1 retained term")
    partial = sum_intervals(ivs)
    tail = geometric_tail_enclosure(ivs[-1], ratio)
    return partial + tail

Other public import paths

omnibias.core.verified.certified_geometric_series_sum
omnibias.core.verified.series.certified_geometric_series_sum

FUNCTION

certified_ratio_series_sum

omnibias.core.verified.certified_ratio_series_sumSource ↗

certified_ratio_series_sum(term: Callable[[int], IntervalLike], ratio: IntervalLike, *, num_terms: int) -> Interval

Enclosure of sum_{n>=0} a_n for terms a_n = term(n) under a ratio bound.

A thin driver over certified_geometric_series_sum: it evaluates the num_terms retained terms a_0, ..., a_{num_terms-1} from the term callable and applies the geometric tail majorant, where ratio is a rigorous magnitude bound q (0 <= q < 1) on every *omitted* consecutive ratio |a_{n+1} / a_n| past the last retained term. Shared by the basic hypergeometric (omnibias-qcalculus) and polylogarithm (core.verified.polylog) enclosures, whose a_n are mpmath-free products of exact rationals and certified transcendental base points.

Parameters

Name	Type & default	Contract
`term`positional-or-keyword	`Callable[[int], IntervalLike]`Required	See the operation contract and implementation below.
`ratio`positional-or-keyword	`IntervalLike`Required	See the operation contract and implementation below.
`num_terms`keyword-only	`int`Required	See the operation contract and implementation below.

ReturnsInterval

Explicit validation & failure cases

When num_terms < 1, raises ValueError(f'num_terms must be >= 1, got {num_terms}').

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

Executed regression · num terms guard

Full file, imports & fixtures ↗

    def test_num_terms_guard(self) -> None:
        with pytest.raises(ValueError):
            certified_ratio_series_sum(lambda k: Interval.point(0.0), Fraction(1, 3), num_terms=0)

python -m pytest "packages/omnibias-core/tests/verified/test_bernoulli_polynomials.py::TestCertifiedRatioSeries::test_num_terms_guard" -q

Regression example · alternating sum is enclosed

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_alternating_sum_is_enclosed(self) -> None:
        # a_n = (-1/2)^n -> sum = 1/(1+1/2) = 2/3; |ratio| = 1/2.
        enc = certified_ratio_series_sum(
            lambda k: Interval.from_rational(Fraction(-1, 2)) ** k,
            Fraction(1, 2),
            num_terms=40,
        )
        assert enc.contains(2.0 / 3.0)

python -m pytest packages/omnibias-core/tests/verified/test_bernoulli_polynomials.py -k test_alternating_sum_is_enclosed -q

Read the implementation

def certified_ratio_series_sum(
    term: Callable[[int], IntervalLike], ratio: IntervalLike, *, num_terms: int
) -> Interval:
    r"""Enclosure of ``sum_{n>=0} a_n`` for terms ``a_n = term(n)`` under a ratio bound.

    A thin driver over :func:`certified_geometric_series_sum`: it evaluates the
    ``num_terms`` retained terms ``a_0, ..., a_{num_terms-1}`` from the ``term``
    callable and applies the geometric tail majorant, where ``ratio`` is a rigorous
    magnitude bound ``q`` (``0 <= q < 1``) on every *omitted* consecutive ratio
    ``|a_{n+1} / a_n|`` past the last retained term. Shared by the basic
    hypergeometric (``omnibias-qcalculus``) and polylogarithm
    (``core.verified.polylog``) enclosures, whose ``a_n`` are ``mpmath``-free
    products of exact rationals and certified transcendental base points.
    """
    if num_terms < 1:
        raise ValueError(f"num_terms must be >= 1, got {num_terms}")
    terms = [Interval.from_value(term(k)) for k in range(num_terms)]
    return certified_geometric_series_sum(terms, ratio)

Other public import paths

omnibias.core.verified.certified_ratio_series_sum
omnibias.core.verified.series.certified_ratio_series_sum

FUNCTION

geometric_series_closed_form

omnibias.core.verified.geometric_series_closed_formSource ↗

geometric_series_closed_form(first: IntervalLike, ratio: IntervalLike) -> Interval

Exact enclosure of sum_{n>=0} first * ratio^n = first / (1 - ratio).

Requires |ratio| < 1 (checked as -1 < ratio.lo and ratio.hi < 1). Unlike certified_geometric_series_sum this is the analytic limit of a *pure* geometric series; it is the ground truth a truncated certified sum must contain.

Parameters

Name	Type & default	Contract
`first`positional-or-keyword	`IntervalLike`Required	See the operation contract and implementation below.
`ratio`positional-or-keyword	`IntervalLike`Required	See the operation contract and implementation below.

ReturnsInterval

Explicit validation & failure cases

When r.hi >= 1.0 or r.lo <= -1.0, raises ValueError(f'geometric closed form requires |ratio| < 1, got {r!r}').

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

Executed regression · geometric closed form encloses limit

Full file, imports & fixtures ↗

def test_geometric_closed_form_encloses_limit() -> None:
    # sum 0.5^n = 2
    enc = geometric_series_closed_form(1.0, 0.5)
    assert enc.lo <= 2.0 <= enc.hi
    assert enc.width < 1e-12
    # sum (-0.3)^n = 1/1.3
    enc2 = geometric_series_closed_form(1.0, -0.3)
    assert enc2.lo <= 1.0 / 1.3 <= enc2.hi

python -m pytest "packages/omnibias-core/tests/verified/test_series.py::test_geometric_closed_form_encloses_limit" -q

Regression example · certified sum brackets closed form

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_certified_sum_brackets_closed_form() -> None:
    terms = [Interval.point(0.25 * 0.4**n) for n in range(6)]
    truncated = certified_geometric_series_sum(terms, 0.4)
    exact = geometric_series_closed_form(0.25, 0.4)
    # the truncated certified bracket must contain the analytic value
    assert truncated.lo <= exact.mid <= truncated.hi

python -m pytest packages/omnibias-core/tests/verified/test_series.py -k test_certified_sum_brackets_closed_form -q

Read the implementation

def geometric_series_closed_form(first: IntervalLike, ratio: IntervalLike) -> Interval:
    r"""Exact enclosure of ``sum_{n>=0} first * ratio^n = first / (1 - ratio)``.

    Requires ``|ratio| < 1`` (checked as ``-1 < ratio.lo`` and ``ratio.hi < 1``).
    Unlike :func:`certified_geometric_series_sum` this is the analytic limit of a
    *pure* geometric series; it is the ground truth a truncated certified sum must
    contain.
    """
    a = Interval.from_value(first)
    r = Interval.from_value(ratio)
    if r.hi >= 1.0 or r.lo <= -1.0:
        raise ValueError(f"geometric closed form requires |ratio| < 1, got {r!r}")
    return a * (Interval.point(1.0) - r).reciprocal()

Other public import paths

omnibias.core.verified.geometric_series_closed_form
omnibias.core.verified.series.geometric_series_closed_form

FUNCTION

geometric_tail_enclosure

omnibias.core.verified.geometric_tail_enclosureSource ↗

geometric_tail_enclosure(last_term: IntervalLike, ratio: IntervalLike) -> Interval

Symmetric enclosure of sum_{k>=1} a_{N+k} from the last retained term.

last_term encloses the final *retained* term a_N; ratio is a rigorous magnitude bound q (0 <= q < 1) on every subsequent consecutive ratio |a_{n+1} / a_n|. Returns [-B, B] with B = (|a_N| * q / (1 - q)).hi (outward rounded) -- a guaranteed enclosure of the omitted tail, regardless of the sign pattern of the terms.

Parameters

Name	Type & default	Contract
`last_term`positional-or-keyword	`IntervalLike`Required	See the operation contract and implementation below.
`ratio`positional-or-keyword	`IntervalLike`Required	See the operation contract and implementation below.

ReturnsInterval

Executed regression · zero last term gives zero tail

Full file, imports & fixtures ↗

def test_zero_last_term_gives_zero_tail() -> None:
    tail = geometric_tail_enclosure(Interval.point(0.0), 0.7)
    assert tail.lo <= 0.0 <= tail.hi
    assert tail.hi < 1e-300  # a zero last term leaves an essentially-zero tail

python -m pytest "packages/omnibias-core/tests/verified/test_series.py::test_zero_last_term_gives_zero_tail" -q

Regression example · tail shrinks with more retained terms

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_tail_shrinks_with_more_retained_terms() -> None:
    t5 = geometric_tail_enclosure(Interval.point(0.5**5), 0.5).hi
    t10 = geometric_tail_enclosure(Interval.point(0.5**10), 0.5).hi
    t20 = geometric_tail_enclosure(Interval.point(0.5**20), 0.5).hi
    assert t5 > t10 > t20 > 0.0

python -m pytest packages/omnibias-core/tests/verified/test_series.py -k test_tail_shrinks_with_more_retained_terms -q

Read the implementation

def geometric_tail_enclosure(last_term: IntervalLike, ratio: IntervalLike) -> Interval:
    r"""Symmetric enclosure of ``sum_{k>=1} a_{N+k}`` from the last retained term.

    ``last_term`` encloses the final *retained* term ``a_N``; ``ratio`` is a
    rigorous magnitude bound ``q`` (``0 <= q < 1``) on every subsequent
    consecutive ratio ``|a_{n+1} / a_n|``.  Returns ``[-B, B]`` with
    ``B = (|a_N| * q / (1 - q)).hi`` (outward rounded) -- a guaranteed enclosure
    of the omitted tail, regardless of the sign pattern of the terms.
    """
    term = Interval.from_value(last_term)
    q = Interval.from_value(ratio)
    _check_ratio(q)
    one_minus = Interval.point(1.0) - q
    bound = term.abs() * q * one_minus.reciprocal()
    b = bound.hi
    return Interval(-b, b)

Other public import paths

omnibias.core.verified.geometric_tail_enclosure
omnibias.core.verified.series.geometric_tail_enclosure

← Package overview Runnable learning examples →

omnibias.core.verified.series

certified_geometric_series_sum​

Parameters

certified_ratio_series_sum​

Parameters

geometric_series_closed_form​

Parameters

geometric_tail_enclosure​

Parameters

certified_geometric_series_sum

certified_ratio_series_sum

geometric_series_closed_form

geometric_tail_enclosure