OAI/Combinatorics/ParityLifts/RealEval.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ParityWL.Complexity.RBEval line 7
  2. lemma OAI.ParityWL.Complexity.BEval.real line 10
  3. lemma OAI.ParityWL.Complexity.RBEval.mono line 13
  4. lemma OAI.ParityWL.Complexity.RBEval.nonneg line 18
  5. lemma OAI.ParityWL.Complexity.RBEval.seq line 22
  6. lemma OAI.ParityWL.Complexity.RBEval.ceil line 28
  7. lemma OAI.ParityWL.Complexity.RBEval.any line 33
  8. lemma OAI.ParityWL.Complexity.RBEval.simulation line 49
  9. lemma OAI.ParityWL.Complexity.RBEval.decision line 57