OAI/Computability/MaxCut/Estimates/Divides.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.OptimalMaxCut.CounterMachine.Expr.indicator_and line 12
  2. def OAI.OptimalMaxCut.CounterMachine.Expr.divides line 16
  3. theorem OAI.OptimalMaxCut.CounterMachine.Expr.divides_eval line 17
  4. def OAI.OptimalMaxCut.CounterMachine.Expr.prime line 21
  5. theorem OAI.OptimalMaxCut.CounterMachine.Expr.prime_eval line 24
  6. def OAI.OptimalMaxCut.CounterMachine.Expr.powTwo line 47
  7. theorem OAI.OptimalMaxCut.CounterMachine.Expr.powTwo_eval line 52
  8. def OAI.OptimalMaxCut.CounterMachine.Expr.size line 87

    Source documentation

    Cardinality of powers of two not exceeding an integer, hence its bit length.

    def size (n : Expr) : Expr := .sum (.add n (.const 1)) (powTwo (.arg 0))

    Mentions: OAI.OptimalMaxCut.CounterMachine.Expr, OAI.OptimalMaxCut.CounterMachine.Expr.powTwo

  9. theorem OAI.OptimalMaxCut.CounterMachine.Expr.count_powers line 89
  10. theorem OAI.OptimalMaxCut.CounterMachine.Expr.size_eval line 102
  11. def OAI.OptimalMaxCut.CounterMachine.Expr.digitPower line 109

    Source documentation

    Locate the unique power of two having the requested binary digit index. Search is bounded by n+1; no exponentially large unary number is ever built.

    def digitPower (n i : Expr) : Expr := .sum (.add n (.const 1))
…

    Mentions: OAI.OptimalMaxCut.CounterMachine.Expr

  12. theorem OAI.OptimalMaxCut.CounterMachine.Expr.digitPower_eval line 113
  13. def OAI.OptimalMaxCut.CounterMachine.Expr.digit line 131
  14. theorem OAI.OptimalMaxCut.CounterMachine.Expr.digit_eval line 133