TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Numerics.Enclosure.Elementary.LogTable.Runtime

Cached logarithms of j / 32 #

Internal.logTable holds log (j / 32) for j from 24 through 48 on the grid of Internal.logTableBits fractional bits. Each entry is computed with logUnreduced at most once per process, on first use, and a read on a coarser grid rounds the cached entry outward. The certified binary power reads the table to bring a logarithm argument in [3/4, 3/2) within 1/48 of one.

Module initialization only allocates the cells: the table disables closed-term extraction, and every read goes through Internal.forceCache.

source
def FloatLib.Numerics.Enclosure.BinaryGrid.Internal.logTableBits :
ℕ

Fractional bits of the cached logarithms of j / 32.

Instances For
    source
    def FloatLib.Numerics.Enclosure.BinaryGrid.Internal.logTableEntry (index : ℕ) :
    Interval ℤ

    log ((index + 24) / 32) on the grid of Internal.logTableBits fractional bits.

    Instances For
      source
      def FloatLib.Numerics.Enclosure.BinaryGrid.Internal.logTable :
      Array (Thunk (Interval ℤ))

      log (j / 32) for j from 24 through 48, each computed on first use and then shared.

      Instances For
        source
        def FloatLib.Numerics.Enclosure.BinaryGrid.logTableAt? (index precision : ℕ) :
        Option (Interval ℤ)

        log ((index + 24) / 32) on the grid of precision fractional bits, coarsened from its cached entry, or none beyond the table and for grids finer than Internal.logTableBits.

        Instances For