API REFERENCE/omnibias-core

omnibias.core.verified.sequence_space

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

Module contract & mathematical conventions

Weighted \ell^1_\nu sequence spaces with rigorous tail bounds.

Modern computer-assisted proofs work in a Banach space of Fourier / Chebyshev / Taylor coefficients with a *geometric* weight nu > 1 (analytic data) or nu in (0, 1] (formal series):

\|a\|_\nu = \sum_{k} |a_k|\,\nu^{|k|}.

This norm makes coefficient convolution **submultiplicative** (||a * b||_nu <= ||a||_nu ||b||_nu), i.e. the sequence space is a Banach *algebra* -- the property the Newton-Kantorovich / radii-polynomial machinery in omnibias.core.verified.kantorovich relies on.

This module provides the rigorous (outward-rounded Interval) norm, geometric tail bounds, and a ValidatedSeries -- a finite vector of interval coefficients plus a non-negative *tail* radius bounding the weighted norm of everything truncated away -- closed under +, * (Banach-algebra convolution) and scalar operations.

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 →

CLASS

ValidatedSeries

omnibias.core.verified.ValidatedSeriesSource ↗

class ValidatedSeries

Dataclass constructor fields; inherited fields, if any, are declared by the base class. A field(...) expression describes a default factory or field options, not a literal argument default.

A rigorous element of \ell^1_\nu: finite coefficients + tail radius.

coeffs[k] encloses the k-th coefficient for k = 0..N; tail is a non-negative bound on sum_{k>N} |a_k| nu^k (the weighted norm of the truncated remainder). All operations keep coeffs exact for k <= N and fold every overflow / cross term rigorously into tail.

Parameters

Name	Type & default	Contract
coeffsdataclass field	list[Interval]Required	See the operation contract and implementation below.
taildataclass field	IntervalRequired	See the operation contract and implementation below.
nudataclass field	floatRequired	See the operation contract and implementation below.
chebyshevdataclass field	boolDefault: False	See the operation contract and implementation below.

Executed regression · chebyshev validated series rejects nu below one

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_chebyshev_validated_series_rejects_nu_below_one() -> None:
    with pytest.raises(ValueError, match="nu >= 1"):
        ValidatedSeries.from_coeffs([1.0], 0.9, chebyshev=True)

python -m pytest "packages/omnibias-core/tests/verified/test_sequence_space.py::test_chebyshev_validated_series_rejects_nu_below_one" -q

Regression example · banach algebra submultiplicative

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_banach_algebra_submultiplicative() -> None:
    rng = random.Random(1)
    nu = 1.5
    for _ in range(100):
        a = ValidatedSeries.from_coeffs(
            [Interval.point(rng.uniform(-2, 2)) for _ in range(4)], nu, tail=abs(rng.uniform(0, 0.3))
        )
        b = ValidatedSeries.from_coeffs(
            [Interval.point(rng.uniform(-2, 2)) for _ in range(4)], nu, tail=abs(rng.uniform(0, 0.3))
        )
        prod = a * b
        # ||a*b|| <= ||a|| ||b||  (submultiplicativity of the weighted norm).
        assert prod.norm().hi <= a.banach_algebra_bound(b).hi * (1 + 1e-12)

python -m pytest packages/omnibias-core/tests/verified/test_sequence_space.py -k test_banach_algebra_submultiplicative -q

Fields & methods

coeffsfield

coeffs: list[Interval]

Declared list[Interval] field on ValidatedSeries. A value must be provided when constructing the configuration, unless an inherited constructor supplies it.

View source ↗

tailfield

tail: Interval

Declared Interval field on ValidatedSeries. A value must be provided when constructing the configuration, unless an inherited constructor supplies it.

View source ↗

nufield

nu: float

Declared float field on ValidatedSeries. A value must be provided when constructing the configuration, unless an inherited constructor supplies it.

View source ↗

chebyshevfield

chebyshev: bool = False

Declared bool field on ValidatedSeries. Default expression: False.

View source ↗

__post_init__method

__post_init__(self) -> None

See the class contract above and the exact method implementation below.

Returns: None

Validation & failure cases

• When self.tail.lo < 0.0, raises ValueError('tail radius must be non-negative').
• When self.chebyshev and self.nu < 1.0, raises ValueError('Chebyshev ValidatedSeries requires nu >= 1').

Executed regression · chebyshev validated series rejects nu below one

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_chebyshev_validated_series_rejects_nu_below_one() -> None:
    with pytest.raises(ValueError, match="nu >= 1"):
        ValidatedSeries.from_coeffs([1.0], 0.9, chebyshev=True)

python -m pytest "packages/omnibias-core/tests/verified/test_sequence_space.py::test_chebyshev_validated_series_rejects_nu_below_one" -q

Method implementation

    def __post_init__(self) -> None:
        if self.tail.lo < 0.0:
            raise ValueError("tail radius must be non-negative")
        if self.chebyshev and self.nu < 1.0:
            raise ValueError("Chebyshev ValidatedSeries requires nu >= 1")

View source ↗

orderproperty

order(self) -> int

See the class contract above and the exact method implementation below.

Returns: int

Executed regression · manufactured solution is an exact zero

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_manufactured_solution_is_an_exact_zero() -> None:
    problem, a_star = _scalar_problem()
    residual = evaluate_residual(problem, a_star)
    assert residual.norm().hi < 1e-12

python -m pytest "packages/omnibias-core/tests/verified/test_radii_series.py::test_manufactured_solution_is_an_exact_zero" -q

Method implementation

    def order(self) -> int:
        return len(self.coeffs) - 1

View source ↗

from_coeffsmethod

from_coeffs(cls, coeffs: Sequence[IntervalLike], nu: float, *, tail: IntervalLike=0.0, chebyshev: bool=False) -> ValidatedSeries

See the class contract above and the exact method implementation below.

Parameters

Name	Type & default	Contract
coeffspositional-or-keyword	Sequence[IntervalLike]Required	See the operation contract and implementation below.
nupositional-or-keyword	floatRequired	See the operation contract and implementation below.
tailkeyword-only	IntervalLikeDefault: 0.0	See the operation contract and implementation below.
chebyshevkeyword-only	boolDefault: False	See the operation contract and implementation below.

Returns: ValidatedSeries

Executed regression · chebyshev validated series rejects nu below one

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_chebyshev_validated_series_rejects_nu_below_one() -> None:
    with pytest.raises(ValueError, match="nu >= 1"):
        ValidatedSeries.from_coeffs([1.0], 0.9, chebyshev=True)

python -m pytest "packages/omnibias-core/tests/verified/test_sequence_space.py::test_chebyshev_validated_series_rejects_nu_below_one" -q

Method implementation

    def from_coeffs(
        cls,
        coeffs: Sequence[IntervalLike],
        nu: float,
        *,
        tail: IntervalLike = 0.0,
        chebyshev: bool = False,
    ) -> ValidatedSeries:
        return cls(
            [Interval.from_value(c) for c in coeffs],
            Interval.from_value(tail),
            float(nu),
            chebyshev,
        )

View source ↗

low_normmethod

low_norm(self) -> Interval

Weighted norm of the finite (kept) part only.

Returns: Interval

Executed regression · manufactured solution is an exact zero

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_manufactured_solution_is_an_exact_zero() -> None:
    problem, a_star = _scalar_problem()
    residual = evaluate_residual(problem, a_star)
    assert residual.norm().hi < 1e-12

python -m pytest "packages/omnibias-core/tests/verified/test_radii_series.py::test_manufactured_solution_is_an_exact_zero" -q

Method implementation

    def low_norm(self) -> Interval:
        """Weighted norm of the finite (kept) part only."""
        return ell1_nu_norm(self.coeffs, self.nu, chebyshev=self.chebyshev)

View source ↗

normmethod

norm(self) -> Interval

Rigorous total weighted norm ||a||_nu (finite part + tail).

Returns: Interval

Executed regression · manufactured solution is an exact zero

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_manufactured_solution_is_an_exact_zero() -> None:
    problem, a_star = _scalar_problem()
    residual = evaluate_residual(problem, a_star)
    assert residual.norm().hi < 1e-12

python -m pytest "packages/omnibias-core/tests/verified/test_radii_series.py::test_manufactured_solution_is_an_exact_zero" -q

Method implementation

    def norm(self) -> Interval:
        """Rigorous total weighted norm ``||a||_nu`` (finite part + tail)."""
        return self.low_norm() + self.tail

View source ↗

__add__method

__add__(self, other: ValidatedSeries) -> ValidatedSeries

See the class contract above and the exact method implementation below.

Parameters

Name	Type & default	Contract
otherpositional-or-keyword	ValidatedSeriesRequired	See the operation contract and implementation below.

Returns: ValidatedSeries

Executed regression · manufactured solution is an exact zero

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_manufactured_solution_is_an_exact_zero() -> None:
    problem, a_star = _scalar_problem()
    residual = evaluate_residual(problem, a_star)
    assert residual.norm().hi < 1e-12

python -m pytest "packages/omnibias-core/tests/verified/test_radii_series.py::test_manufactured_solution_is_an_exact_zero" -q

Method implementation

    def __add__(self, other: ValidatedSeries) -> ValidatedSeries:
        self._check_compatible(other)
        n = max(len(self.coeffs), len(other.coeffs))
        coeffs: list[Interval] = []
        for k in range(n):
            a = self.coeffs[k] if k < len(self.coeffs) else Interval.point(0.0)
            b = other.coeffs[k] if k < len(other.coeffs) else Interval.point(0.0)
            coeffs.append(a + b)
        return ValidatedSeries(coeffs, _nonneg(self.tail + other.tail), self.nu, self.chebyshev)

View source ↗

__mul__method

__mul__(self, other: ValidatedSeries) -> ValidatedSeries

See the class contract above and the exact method implementation below.

Parameters

Name	Type & default	Contract
otherpositional-or-keyword	ValidatedSeriesRequired	See the operation contract and implementation below.

Returns: ValidatedSeries

Executed regression · manufactured solution is an exact zero

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_manufactured_solution_is_an_exact_zero() -> None:
    problem, a_star = _scalar_problem()
    residual = evaluate_residual(problem, a_star)
    assert residual.norm().hi < 1e-12

python -m pytest "packages/omnibias-core/tests/verified/test_radii_series.py::test_manufactured_solution_is_an_exact_zero" -q

Method implementation

    def __mul__(self, other: ValidatedSeries) -> ValidatedSeries:
        self._check_compatible(other)
        n = min(self.order, other.order)  # keep coefficients up to this order
        conv = (
            _chebyshev_product(self.coeffs, other.coeffs)
            if self.chebyshev
            else convolve(self.coeffs, other.coeffs)
        )
        kept = conv[: n + 1]
        overflow = conv[n + 1 :]
        # Weighted norm of the overflow coefficients (their true index starts at n+1).
        nu_iv = Interval.point(self.nu)
        overflow_norm = Interval.point(0.0)
        power = _nu_power(nu_iv, n + 1)
        for k, c in enumerate(overflow):
            w = Interval.point(2.0) if self.chebyshev and (n + 1 + k) >= 1 else Interval.point(1.0)
            overflow_norm = overflow_norm + Interval.point(c.mag) * power * w
            power = power * nu_iv
        cross = (
            self.low_norm() * other.tail
            + self.tail * other.low_norm()
            + self.tail * other.tail
        )
        if self.chebyshev and cross.hi > 0.0:
            # A Chebyshev tail can fold back to every low mode through
            # T_i*T_j = (T_{i+j}+T_|i-j|)/2. Enclose that possible contribution
            # in each retained coefficient; the same norm bound covers the
            # unknown high modes held in ``tail``.
            cross_bound = Interval.point(cross.hi)
            for k, coefficient in enumerate(kept):
                weight = Interval.point(1.0 if k == 0 else 2.0)
                mode_bound = cross_bound / (weight * _nu_power(nu_iv, k))
                radius = mode_bound.hi
                kept[k] = coefficient + Interval(-radius, radius)
        return ValidatedSeries(kept, _nonneg(overflow_norm + cross), self.nu, self.chebyshev)

View source ↗

scalemethod

scale(self, factor: IntervalLike) -> ValidatedSeries

Multiply by a scalar (constant) rigorously.

Parameters

Name	Type & default	Contract
factorpositional-or-keyword	IntervalLikeRequired	See the operation contract and implementation below.

Returns: ValidatedSeries

Executed regression · manufactured solution is an exact zero

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_manufactured_solution_is_an_exact_zero() -> None:
    problem, a_star = _scalar_problem()
    residual = evaluate_residual(problem, a_star)
    assert residual.norm().hi < 1e-12

python -m pytest "packages/omnibias-core/tests/verified/test_radii_series.py::test_manufactured_solution_is_an_exact_zero" -q

Method implementation

    def scale(self, factor: IntervalLike) -> ValidatedSeries:
        """Multiply by a scalar (constant) rigorously."""
        f = Interval.from_value(factor)
        coeffs = [c * f for c in self.coeffs]
        return ValidatedSeries(
            coeffs, _nonneg(self.tail * Interval.point(f.mag)), self.nu, self.chebyshev
        )

View source ↗

banach_algebra_boundmethod

banach_algebra_bound(self, other: ValidatedSeries) -> Interval

The submultiplicative bound ||a||_nu * ||b||_nu on the product norm.

Parameters

Name	Type & default	Contract
otherpositional-or-keyword	ValidatedSeriesRequired	See the operation contract and implementation below.

Returns: Interval

Executed regression · banach algebra submultiplicative

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_banach_algebra_submultiplicative() -> None:
    rng = random.Random(1)
    nu = 1.5
    for _ in range(100):
        a = ValidatedSeries.from_coeffs(
            [Interval.point(rng.uniform(-2, 2)) for _ in range(4)], nu, tail=abs(rng.uniform(0, 0.3))
        )
        b = ValidatedSeries.from_coeffs(
            [Interval.point(rng.uniform(-2, 2)) for _ in range(4)], nu, tail=abs(rng.uniform(0, 0.3))
        )
        prod = a * b
        # ||a*b|| <= ||a|| ||b||  (submultiplicativity of the weighted norm).
        assert prod.norm().hi <= a.banach_algebra_bound(b).hi * (1 + 1e-12)

python -m pytest "packages/omnibias-core/tests/verified/test_sequence_space.py::test_banach_algebra_submultiplicative" -q

Method implementation

    def banach_algebra_bound(self, other: ValidatedSeries) -> Interval:
        """The submultiplicative bound ``||a||_nu * ||b||_nu`` on the product norm."""
        self._check_compatible(other)
        return self.norm() * other.norm()

View source ↗

Read the implementation

class ValidatedSeries:
    r"""A rigorous element of :math:`\ell^1_\nu`: finite coefficients + tail radius.

    ``coeffs[k]`` encloses the ``k``-th coefficient for ``k = 0..N``; ``tail`` is a
    non-negative bound on ``sum_{k>N} |a_k| nu^k`` (the weighted norm of the
    truncated remainder).  All operations keep ``coeffs`` exact for ``k <= N`` and
    fold every overflow / cross term rigorously into ``tail``.
    """

    coeffs: list[Interval]
    tail: Interval
    nu: float
    chebyshev: bool = False

    def __post_init__(self) -> None:
        if self.tail.lo < 0.0:
            raise ValueError("tail radius must be non-negative")
        if self.chebyshev and self.nu < 1.0:
            raise ValueError("Chebyshev ValidatedSeries requires nu >= 1")

    @property
    def order(self) -> int:
        return len(self.coeffs) - 1

    @classmethod
    def from_coeffs(
        cls,
        coeffs: Sequence[IntervalLike],
        nu: float,
        *,
        tail: IntervalLike = 0.0,
        chebyshev: bool = False,
    ) -> ValidatedSeries:
        return cls(
            [Interval.from_value(c) for c in coeffs],
            Interval.from_value(tail),
            float(nu),
            chebyshev,
        )

    def low_norm(self) -> Interval:
        """Weighted norm of the finite (kept) part only."""
        return ell1_nu_norm(self.coeffs, self.nu, chebyshev=self.chebyshev)

    def norm(self) -> Interval:
        """Rigorous total weighted norm ``||a||_nu`` (finite part + tail)."""
        return self.low_norm() + self.tail

    def _check_compatible(self, other: ValidatedSeries) -> None:
        if self.nu != other.nu or self.chebyshev != other.chebyshev:
            raise ValueError("ValidatedSeries operands must share nu and basis")

    def __add__(self, other: ValidatedSeries) -> ValidatedSeries:
        self._check_compatible(other)
        n = max(len(self.coeffs), len(other.coeffs))
        coeffs: list[Interval] = []
        for k in range(n):
            a = self.coeffs[k] if k < len(self.coeffs) else Interval.point(0.0)
            b = other.coeffs[k] if k < len(other.coeffs) else Interval.point(0.0)
            coeffs.append(a + b)
        return ValidatedSeries(coeffs, _nonneg(self.tail + other.tail), self.nu, self.chebyshev)

    def __mul__(self, other: ValidatedSeries) -> ValidatedSeries:
        self._check_compatible(other)
        n = min(self.order, other.order)  # keep coefficients up to this order
        conv = (
            _chebyshev_product(self.coeffs, other.coeffs)
            if self.chebyshev
            else convolve(self.coeffs, other.coeffs)
        )
        kept = conv[: n + 1]
        overflow = conv[n + 1 :]
        # Weighted norm of the overflow coefficients (their true index starts at n+1).
        nu_iv = Interval.point(self.nu)
        overflow_norm = Interval.point(0.0)
        power = _nu_power(nu_iv, n + 1)
        for k, c in enumerate(overflow):
            w = Interval.point(2.0) if self.chebyshev and (n + 1 + k) >= 1 else Interval.point(1.0)
            overflow_norm = overflow_norm + Interval.point(c.mag) * power * w
            power = power * nu_iv
        cross = (
            self.low_norm() * other.tail
            + self.tail * other.low_norm()
            + self.tail * other.tail
        )
        if self.chebyshev and cross.hi > 0.0:
            # A Chebyshev tail can fold back to every low mode through
            # T_i*T_j = (T_{i+j}+T_|i-j|)/2. Enclose that possible contribution
            # in each retained coefficient; the same norm bound covers the
            # unknown high modes held in ``tail``.
            cross_bound = Interval.point(cross.hi)
            for k, coefficient in enumerate(kept):
                weight = Interval.point(1.0 if k == 0 else 2.0)
                mode_bound = cross_bound / (weight * _nu_power(nu_iv, k))
                radius = mode_bound.hi
                kept[k] = coefficient + Interval(-radius, radius)
        return ValidatedSeries(kept, _nonneg(overflow_norm + cross), self.nu, self.chebyshev)

    def scale(self, factor: IntervalLike) -> ValidatedSeries:
        """Multiply by a scalar (constant) rigorously."""
        f = Interval.from_value(factor)
        coeffs = [c * f for c in self.coeffs]
        return ValidatedSeries(
            coeffs, _nonneg(self.tail * Interval.point(f.mag)), self.nu, self.chebyshev
        )

    def banach_algebra_bound(self, other: ValidatedSeries) -> Interval:
        """The submultiplicative bound ``||a||_nu * ||b||_nu`` on the product norm."""
        self._check_compatible(other)
        return self.norm() * other.norm()

Related APIsomnibias.core.verified.Interval↗omnibias.core.verified.convolve↗omnibias.core.verified.ell1_nu_norm↗

Other public import paths

• omnibias.core.verified.ValidatedSeries
• omnibias.core.verified.sequence_space.ValidatedSeries

FUNCTION

convolve

omnibias.core.verified.convolveSource ↗

convolve(a: Sequence[Interval], b: Sequence[Interval]) -> list[Interval]

Rigorous discrete convolution (a * b)_k = sum_{i+j=k} a_i b_j.

Parameters

Name	Type & default	Contract
apositional-or-keyword	Sequence[Interval]Required	See the operation contract and implementation below.
bpositional-or-keyword	Sequence[Interval]Required	See the operation contract and implementation below.

Returnslist[Interval]

Executed regression · manufactured solution is an exact zero

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_manufactured_solution_is_an_exact_zero() -> None:
    problem, a_star = _scalar_problem()
    residual = evaluate_residual(problem, a_star)
    assert residual.norm().hi < 1e-12

python -m pytest "packages/omnibias-core/tests/verified/test_radii_series.py::test_manufactured_solution_is_an_exact_zero" -q

Regression example · convolution matches polynomial product

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_convolution_matches_polynomial_product() -> None:
    a = [Interval.point(1.0), Interval.point(2.0)]  # 1 + 2x
    b = [Interval.point(3.0), Interval.point(4.0)]  # 3 + 4x
    c = convolve(a, b)  # 3 + 10x + 8x^2
    vals = [iv.mid for iv in c]
    assert vals == [3.0, 10.0, 8.0]

python -m pytest packages/omnibias-core/tests/verified/test_sequence_space.py -k test_convolution_matches_polynomial_product -q

Read the implementation

def convolve(a: Sequence[Interval], b: Sequence[Interval]) -> list[Interval]:
    """Rigorous discrete convolution ``(a * b)_k = sum_{i+j=k} a_i b_j``."""
    if not a or not b:
        return []
    out = [Interval.point(0.0) for _ in range(len(a) + len(b) - 1)]
    for i, ai in enumerate(a):
        for j, bj in enumerate(b):
            out[i + j] = out[i + j] + ai * bj
    return out

Other public import paths

• omnibias.core.verified.convolve
• omnibias.core.verified.sequence_space.convolve

FUNCTION

ell1_nu_norm

omnibias.core.verified.ell1_nu_normSource ↗

ell1_nu_norm(coeffs: Sequence[IntervalLike], nu: float, *, chebyshev: bool=False) -> Interval

Rigorous one-sided weighted norm sum_{k>=0} w_k |a_k| nu^k.

With chebyshev=True the Chebyshev convention w_0 = 1, w_k = 2 (k >= 1) is used; otherwise w_k = 1 (Taylor / power series).

Parameters

Name	Type & default	Contract
coeffspositional-or-keyword	Sequence[IntervalLike]Required	See the operation contract and implementation below.
nupositional-or-keyword	floatRequired	See the operation contract and implementation below.
chebyshevkeyword-only	boolDefault: False	See the operation contract and implementation below.

ReturnsInterval

Executed regression · manufactured solution is an exact zero

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_manufactured_solution_is_an_exact_zero() -> None:
    problem, a_star = _scalar_problem()
    residual = evaluate_residual(problem, a_star)
    assert residual.norm().hi < 1e-12

python -m pytest "packages/omnibias-core/tests/verified/test_radii_series.py::test_manufactured_solution_is_an_exact_zero" -q

Regression example · chebyshev weighting

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_chebyshev_weighting() -> None:
    coeffs = [Interval.point(1.0), Interval.point(1.0)]
    # |c0| + 2|c1| nu at nu=1 -> 1 + 2 = 3.
    norm = ell1_nu_norm(coeffs, 1.0, chebyshev=True)
    assert norm.lo <= 3.0 <= norm.hi

python -m pytest packages/omnibias-core/tests/verified/test_sequence_space.py -k test_chebyshev_weighting -q

Read the implementation

def ell1_nu_norm(
    coeffs: Sequence[IntervalLike],
    nu: float,
    *,
    chebyshev: bool = False,
) -> Interval:
    r"""Rigorous one-sided weighted norm ``sum_{k>=0} w_k |a_k| nu^k``.

    With ``chebyshev=True`` the Chebyshev convention ``w_0 = 1``, ``w_k = 2``
    (``k >= 1``) is used; otherwise ``w_k = 1`` (Taylor / power series).
    """
    nu_iv = Interval.point(float(nu))
    acc = Interval.point(0.0)
    power = Interval.point(1.0)
    for k, c in enumerate(coeffs):
        mag = Interval.from_value(c).mag
        term = Interval.point(mag) * power
        if chebyshev and k >= 1:
            term = term * 2
        acc = acc + term
        power = power * nu_iv
    return acc

Other public import paths

• omnibias.core.verified.ell1_nu_norm
• omnibias.core.verified.sequence_space.ell1_nu_norm

FUNCTION

fourier_nu_norm

omnibias.core.verified.fourier_nu_normSource ↗

fourier_nu_norm(coeffs: Mapping[int, IntervalLike], nu: float) -> Interval

Rigorous two-sided weighted norm sum_{k in Z} |a_k| nu^{|k|}.

Parameters

Name	Type & default	Contract
coeffspositional-or-keyword	Mapping[int, IntervalLike]Required	See the operation contract and implementation below.
nupositional-or-keyword	floatRequired	See the operation contract and implementation below.

ReturnsInterval

Executed regression · fourier two sided norm

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_fourier_two_sided_norm() -> None:
    coeffs = {-1: Interval.point(2.0), 0: Interval.point(1.0), 1: Interval.point(2.0)}
    # 1 + 2 nu + 2 nu at nu=3 -> 1 + 12 = 13.
    norm = fourier_nu_norm(coeffs, 3.0)
    assert norm.lo <= 13.0 <= norm.hi

python -m pytest "packages/omnibias-core/tests/verified/test_sequence_space.py::test_fourier_two_sided_norm" -q

Regression example · chebyshev weighting

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_chebyshev_weighting() -> None:
    coeffs = [Interval.point(1.0), Interval.point(1.0)]
    # |c0| + 2|c1| nu at nu=1 -> 1 + 2 = 3.
    norm = ell1_nu_norm(coeffs, 1.0, chebyshev=True)
    assert norm.lo <= 3.0 <= norm.hi

python -m pytest packages/omnibias-core/tests/verified/test_sequence_space.py -k test_chebyshev_weighting -q

Read the implementation

def fourier_nu_norm(coeffs: Mapping[int, IntervalLike], nu: float) -> Interval:
    r"""Rigorous two-sided weighted norm ``sum_{k in Z} |a_k| nu^{|k|}``."""
    nu_iv = Interval.point(float(nu))
    acc = Interval.point(0.0)
    for k, c in coeffs.items():
        mag = Interval.from_value(c).mag
        acc = acc + Interval.point(mag) * _nu_power(nu_iv, abs(int(k)))
    return acc

Other public import paths

• omnibias.core.verified.fourier_nu_norm
• omnibias.core.verified.sequence_space.fourier_nu_norm

FUNCTION

geometric_tail_bound

omnibias.core.verified.geometric_tail_boundSource ↗

geometric_tail_bound(coeff_bound: float, ratio: float, nu: float, n_trunc: int) -> Interval

Bound sum_{k>n_trunc} |a_k| nu^k given |a_k| <= coeff_bound*ratio^k.

Requires the *weighted* ratio r = nu*ratio < 1; the geometric tail is then coeff_bound * r^{n_trunc+1} / (1 - r) (outward rounded).

Parameters

Name	Type & default	Contract
coeff_boundpositional-or-keyword	floatRequired	See the operation contract and implementation below.
ratiopositional-or-keyword	floatRequired	See the operation contract and implementation below.
nupositional-or-keyword	floatRequired	See the operation contract and implementation below.
n_truncpositional-or-keyword	intRequired	See the operation contract and implementation below.

ReturnsInterval

Explicit validation & failure cases

• When coeff_bound < 0.0, raises ValueError('coeff_bound must be non-negative').
• When r.hi >= 1.0, raises ValueError(f'weighted ratio nu*ratio={r.hi!r} must be < 1 for a finite tail').
• When one_minus.lo <= 0.0, raises ValueError('1 - nu*ratio must be strictly positive').

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

Executed regression · geometric tail requires convergent weight

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_geometric_tail_requires_convergent_weight() -> None:
    with pytest.raises(ValueError):
        geometric_tail_bound(1.0, 2.0, 1.0, 0)  # nu*ratio = 2 >= 1

python -m pytest "packages/omnibias-core/tests/verified/test_sequence_space.py::test_geometric_tail_requires_convergent_weight" -q

Regression example · geometric tail encloses exact 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_geometric_tail_encloses_exact_series() -> None:
    # sum_{k>2} M q^k nu^k with M=1, q=0.5, nu=1, exact = r^3/(1-r), r=0.5 -> 0.25.
    bound = geometric_tail_bound(1.0, 0.5, 1.0, 2)
    assert bound.lo <= 0.125 / (1 - 0.5) <= bound.hi
    assert bound.hi < 0.26

python -m pytest packages/omnibias-core/tests/verified/test_sequence_space.py -k test_geometric_tail_encloses_exact_series -q

Read the implementation

def geometric_tail_bound(
    coeff_bound: float,
    ratio: float,
    nu: float,
    n_trunc: int,
) -> Interval:
    r"""Bound ``sum_{k>n_trunc} |a_k| nu^k`` given ``|a_k| <= coeff_bound*ratio^k``.

    Requires the *weighted* ratio ``r = nu*ratio < 1``; the geometric tail is then
    ``coeff_bound * r^{n_trunc+1} / (1 - r)`` (outward rounded).
    """
    if coeff_bound < 0.0:
        raise ValueError("coeff_bound must be non-negative")
    r = Interval.point(float(nu)) * Interval.point(float(ratio))
    if r.hi >= 1.0:
        raise ValueError(f"weighted ratio nu*ratio={r.hi!r} must be < 1 for a finite tail")
    one_minus = Interval.point(1.0) - r
    if one_minus.lo <= 0.0:
        raise ValueError("1 - nu*ratio must be strictly positive")
    return Interval.point(coeff_bound) * r.pow_int(n_trunc + 1) / one_minus

Other public import paths

• omnibias.core.verified.geometric_tail_bound
• omnibias.core.verified.sequence_space.geometric_tail_bound

← Package overviewRunnable learning examples →