OAI/Combinatorics/EditApproximation/Binary/BinaryInitialKernel.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Literal initial-cone arithmetic on gathered integer seed entries. The local grid list is supplied by its bounded enumerator; all values, ceilings, spatial charges and the fallback minimum are computed on binary storage.

  1. theorem OAI.EditApproximation.BinaryFraction.ofNaturalWord_value line 18
  2. theorem OAI.EditApproximation.BinaryFraction.ofNaturalWord_width line 24
  3. theorem OAI.EditApproximation.BinaryFraction.scaledSeedWithWork_value line 29
  4. theorem OAI.EditApproximation.BinaryFraction.initialConeWithWork_value line 36
  5. def OAI.EditApproximation.BinaryFraction.initialMinimumWithWork line 47

    Source documentation

    The local initial-cone arithmetic after the center list has been constructed and the corresponding seed values gathered.

    def initialMinimumWithWork {n : ℕ} (sourceLength : ℕ) (U : TargetInterval n → ℕ)
    (N F : ℕ) (a : BinaryFraction) (query : TargetInterval n) (centers : List (TargetInterval n)) :
    BinaryFraction × ℕ :=
…

    Mentions: OAI.EditApproximation.TargetInterval, OAI.EditApproximation.BinaryFraction

  6. theorem OAI.EditApproximation.BinaryFraction.initialMinimumWithWork_value line 60