OAI/Combinatorics/EditApproximation/Binary/BinaryGroupSetup.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The literal scale list and sample counts, including scales below one. Dyadic input exponents are carried by the computed parameter construction; no real logarithm is evaluated by these routines.

  1. theorem OAI.EditApproximation.BinaryFraction.signedPowerTwoWithWork_value line 16
  2. theorem OAI.EditApproximation.BinaryFraction.signedPowerTwoWithWork_width line 26
  3. theorem OAI.EditApproximation.BinaryFraction.groupScalesWithWork_value line 41
  4. theorem OAI.EditApproximation.BinaryFraction.groupScalesWithWork_length line 58
  5. theorem OAI.EditApproximation.BinaryFraction.groupSampleCountWithWork_value line 66

    Source documentation

    Exact versus sampled is decided from the actual binary sample count.

    @[simp] theorem groupSampleCountWithWork_value (M Q b : ℕ) (h : BinaryFraction) :
    bitWordValue (groupSampleCountWithWork M Q b h).1 = groupSampleCount M Q b h.value := by
…

    Mentions: OAI.EditApproximation.BinaryFraction, OAI.EditApproximation.bitWordValue, OAI.EditApproximation.BinaryFraction.groupSampleCountWithWork, OAI.EditApproximation.groupSampleCount