OAI/Combinatorics/EditApproximation/Coarse/CoarseScalarControlSpace.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.EditApproximation.BinaryFraction.coarseGridNatInvocations line 10

    Source documentation

    Control invocations of the shared-denominator scalar construction.

    def coarseGridNatInvocations (denominator : List Bool)
    (hden : 0 < bitWordValue denominator) (n : ℕ) : ℕ :=
…

    Mentions: OAI.EditApproximation.bitWordValue

  2. theorem OAI.EditApproximation.BinaryFraction.coarseGridNatInvocations_le_work line 16
  3. def OAI.EditApproximation.BinaryFraction.coarseGridAddInvocations line 26
  4. theorem OAI.EditApproximation.BinaryFraction.coarseGridAddInvocations_le_work line 30
  5. def OAI.EditApproximation.BinaryFraction.coarseDivideInvocations line 39
  6. theorem OAI.EditApproximation.BinaryFraction.coarseDivideInvocations_le_work line 43
  7. def OAI.EditApproximation.BinaryFraction.coarseContributionInvocations line 52
  8. theorem OAI.EditApproximation.BinaryFraction.coarseContributionInvocations_le_work line 57
  9. def OAI.EditApproximation.BinaryFraction.coarseChildThresholdInvocations line 67

    Source documentation

    Includes a conservative allowance for the three literal constructors.

    def coarseChildThresholdInvocations (B q : ℕ) (allowance : BinaryFraction) (draw : Fin B) : ℕ :=
…

    Mentions: OAI.EditApproximation.BinaryFraction

  10. theorem OAI.EditApproximation.BinaryFraction.coarseChildThresholdInvocations_le_work line 74
  11. def OAI.EditApproximation.BinaryFraction.coarseChildAllowanceInvocations line 86
  12. theorem OAI.EditApproximation.BinaryFraction.coarseChildAllowanceInvocations_le_work line 89