Skip to content

How to represent externally certified enclosures with trv decoration? #763

Description

@ChangheYang1999

Hi, I have a question about decorations in IntervalArithmetic.jl.

In my project, some intervals are not obtained directly from decorated interval evaluation. Instead, they are certified by an external error estimate.

For example, suppose I have an approximate value x_approx and a rigorous error bound E, with an external proof that

abs(x_true - x_approx) <= E

Then I know that the true value is contained in

[x_approx - E, x_approx + E]

In code this is roughly:

lo = x_approx - E
hi = x_approx + E
Y = hull(lo, hi)

The result may have decoration trv. I understand that this can happen because hull is a set operation, not a continuous function evaluation, so it should not automatically preserve com.

My question is: how should such externally certified enclosures be represented?

More specifically:

  1. Does trv mean only that the decoration-based function-evaluation information is lost, or does it also mean the interval should not be trusted as an enclosure?
  2. Is it reasonable to keep the trv decoration while relying on the external proof abs(x_true - x_approx) <= E?
  3. Is there a recommended pattern for this, such as wrapping the interval in a separate CertifiedEnclosure type?

I do not want to manually reconstruct the interval as com, since that would misrepresent the decoration semantics. I only want a clean way to express: the interval is not certified by decorations, but its bounds are certified by an external theorem or error bound.

Thanks!

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions