Sharing enclosures between rounding comparisons #
A rounding search compares one mathematical value with many boundaries. Its enclosures depend on the requested accuracy, not on the boundary, so recomputing the same Taylor polynomial at every bisection step is unnecessary.
cacheIntervals delays a finite prefix with Lean's pure Thunk type. A requested entry is
computed once and shared by subsequent comparisons. Entries beyond the prefix are computed
normally; the cache size never limits the mathematical search. The cache is explicit data:
returning a curried function here would let eta expansion move allocation into each lookup.
A shared finite prefix, followed by an unrestricted interval generator.
- values : Array (Thunk RationalInterval)
Lazily evaluated intervals at the most frequently requested degrees.
- fallback : ℕ → RationalInterval
The original generator remains available beyond the cached prefix.
Instances For
Retrieve an interval, computing and sharing its cached entry when present.
Instances For
Lazily cache the first count intervals without changing the sequence.
Instances For
Caching changes evaluation cost but leaves every rational endpoint unchanged.
A comparison prepared once for many boundaries.
The data constructor keeps the shared interval array outside the boundary function. Direct comparisons cover exact rational values and algorithms whose enclosures depend on the boundary.
- direct
(run : ℚ → Ordering)
: Prepared
A comparison that does not share a target's interval sequence.
- enclosed
(cache : IntervalCache)
(terminates : ∀ (boundary : ℚ), ∃ (n : ℕ), Separates (cache.get n) boundary)
: Prepared
A total adaptive comparison with a shared target enclosure sequence.
Instances For
Compare a prepared target with one rational boundary.