OAI/Combinatorics/MatchingCount/Tapes/RunBits.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MatchingFPRAS.FiniteChoice.tapeIndex_value line 10
  2. lemma OAI.MatchingFPRAS.FiniteChoice.tapeLaw_eq line 17
  3. def OAI.MatchingFPRAS.BoundedSimulation.runBits line 41
  4. def OAI.MatchingFPRAS.BoundedSimulation.pointMass line 49
  5. def OAI.MatchingFPRAS.BoundedSimulation.uniformLaw line 51
  6. lemma OAI.MatchingFPRAS.BoundedSimulation.uniformLaw_equiv line 58
  7. lemma OAI.MatchingFPRAS.BoundedSimulation.fiber_sum line 65
  8. lemma OAI.MatchingFPRAS.BoundedSimulation.uniformLaw_map line 71
  9. lemma OAI.MatchingFPRAS.BoundedSimulation.uniformLaw_prod line 78
  10. lemma OAI.MatchingFPRAS.BoundedSimulation.uniformLaw_chooseBits line 86
  11. lemma OAI.MatchingFPRAS.BoundedSimulation.uniformLaw_choice_step line 95
  12. lemma OAI.MatchingFPRAS.BoundedSimulation.runBits_law_succ line 105
  13. lemma OAI.MatchingFPRAS.BoundedSimulation.runBits_law line 132
  14. lemma OAI.MatchingFPRAS.BoundedSimulation.pointMass_nonneg line 140
  15. lemma OAI.MatchingFPRAS.BoundedSimulation.pointMass_sum line 143
  16. lemma OAI.MatchingFPRAS.BoundedSimulation.fixed_tape_card line 145
  17. theorem OAI.MatchingFPRAS.BoundedSimulation.fixed_tape_simulation line 151
  18. abbrev OAI.MatchingFPRAS.Counting.alpha line 165
  19. lemma OAI.MatchingFPRAS.Counting.others_nonempty line 167
  20. def OAI.MatchingFPRAS.Counting.rowMaximum line 173
  21. def OAI.MatchingFPRAS.Counting.scaleUpdate line 176
  22. def OAI.MatchingFPRAS.Counting.scalingTrace line 179
  23. structure OAI.MatchingFPRAS.Counting.ScaleInvariant line 189
  24. lemma OAI.MatchingFPRAS.Counting.ScaleInvariant.pos line 194
  25. lemma OAI.MatchingFPRAS.Counting.rowMaximum_le line 197
  26. lemma OAI.MatchingFPRAS.Counting.ratio_le_rowMaximum line 203
  27. lemma OAI.MatchingFPRAS.Counting.rowMaximum_lower line 207
  28. lemma OAI.MatchingFPRAS.Counting.scaleUpdate_le line 219
  29. lemma OAI.MatchingFPRAS.Counting.scaleUpdate_invariant line 225
  30. lemma OAI.MatchingFPRAS.Counting.scaleUpdate_tight line 245
  31. lemma OAI.MatchingFPRAS.Counting.tight_persists line 256
  32. lemma OAI.MatchingFPRAS.Counting.scalingTrace_invariant line 268
  33. theorem OAI.MatchingFPRAS.Counting.one_pass_scaling line 306
  34. def OAI.MatchingFPRAS.Counting.rowPeak line 327
  35. def OAI.MatchingFPRAS.Counting.scaledHoleMatrix line 330
  36. def OAI.MatchingFPRAS.Counting.BalancedRows line 333
  37. theorem OAI.MatchingFPRAS.Counting.one_pass_restores_balance line 339
  38. def OAI.MatchingFPRAS.Counting.sigma line 382
  39. def OAI.MatchingFPRAS.Counting.ratioEstimate line 384
  40. def OAI.MatchingFPRAS.Counting.upperEstimate line 386