OAI/Combinatorics/MatchingCount/Algorithm/OutputLengthBound.lean

GitHub source file

113 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MatchingFPRAS.Perfect.vertices_le_twice_edges line 12
  2. lemma OAI.MatchingFPRAS.positive_count_vertices line 27
  3. lemma OAI.MatchingFPRAS.sparse_reject_zero line 32
  4. lemma OAI.MatchingFPRAS.encodeNat_length_pos line 36
  5. lemma OAI.MatchingFPRAS.flatMap_length_ge line 37
  6. lemma OAI.MatchingFPRAS.edges_le_input_length line 45
  7. lemma OAI.MatchingFPRAS.nonzero_vertices_le_input_twice line 60
  8. lemma OAI.MatchingFPRAS.Counting.sigma_inv_polynomial line 66
  9. lemma OAI.MatchingFPRAS.Trial.Parameters.N_polynomial line 84
  10. lemma OAI.MatchingFPRAS.Trial.Parameters.D_polynomial line 91
  11. lemma OAI.MatchingFPRAS.Trial.Parameters.S_polynomial line 94
  12. lemma OAI.MatchingFPRAS.BitArithmetic.size_add_le line 110
  13. lemma OAI.MatchingFPRAS.BitArithmetic.complete_count_size line 118
  14. lemma OAI.MatchingFPRAS.Amplification.median_mem line 129
  15. def OAI.MatchingFPRAS.FiniteTrial.outputLengthBound line 141
  16. lemma OAI.MatchingFPRAS.FiniteTrial.output_encode_length line 143
  17. lemma OAI.MatchingFPRAS.FiniteTrial.amplifiedOutput_encode_length line 158
  18. lemma OAI.MatchingFPRAS.Transport.clog_two_le_self line 170
  19. lemma OAI.MatchingFPRAS.Transport.bitPrecision_le line 172
  20. lemma OAI.MatchingFPRAS.Transport.sym2_card_le_square line 174
  21. lemma OAI.MatchingFPRAS.Transport.bagEdge_card_le line 176
  22. def OAI.MatchingFPRAS.Transport.tierPolynomial line 185
  23. def OAI.MatchingFPRAS.Transport.lambdaPolynomial line 186
  24. def OAI.MatchingFPRAS.Transport.stepsPolynomial line 187
  25. def OAI.MatchingFPRAS.Transport.edgePolynomial line 190
  26. def OAI.MatchingFPRAS.Transport.scanErrorPolynomial line 191
  27. def OAI.MatchingFPRAS.Transport.totalBitsPolynomial line 194
  28. lemma OAI.MatchingFPRAS.Transport.endpoint_le_polynomial line 198
  29. lemma OAI.MatchingFPRAS.Transport.lambda_le_polynomial line 204
  30. lemma OAI.MatchingFPRAS.Transport.discreteSteps_le_polynomial line 208
  31. lemma OAI.MatchingFPRAS.RationalSource.edge_card_polynomial line 222
  32. lemma OAI.MatchingFPRAS.RationalSource.scan_error_polynomial line 227
  33. def OAI.MatchingFPRAS.RationalSource.samplerBitCount line 239
  34. lemma OAI.MatchingFPRAS.RationalSource.samplerBitCount_le line 245
  35. lemma OAI.MatchingFPRAS.Variation.imageLaw_ignore_right line 269
  36. def OAI.MatchingFPRAS.Variation.paddedBits line 273
  37. def OAI.MatchingFPRAS.Variation.padSampler line 276
  38. lemma OAI.MatchingFPRAS.Variation.padSampler_law line 279
  39. def OAI.MatchingFPRAS.Variation.markedBitsEquiv line 282
  40. def OAI.MatchingFPRAS.RationalSource.bitSampler line 308
  41. lemma OAI.MatchingFPRAS.RationalSource.bitSampler_law line 315
  42. def OAI.MatchingFPRAS.RationalSource.fixedSampler line 323
  43. lemma OAI.MatchingFPRAS.RationalSource.fixedSampler_law line 330
  44. lemma OAI.MatchingFPRAS.Variation.imageLaw_sigma_pair line 345
  45. def OAI.MatchingFPRAS.FiniteTrial.oneBits line 379
  46. lemma OAI.MatchingFPRAS.FiniteTrial.oneBits_eq line 382
  47. def OAI.MatchingFPRAS.FiniteTrial.ScaleState.drawOne line 387
  48. lemma OAI.MatchingFPRAS.FiniteTrial.ScaleState.drawOne_law line 393
  49. def OAI.MatchingFPRAS.FiniteTrial.stageBits line 396
  50. def OAI.MatchingFPRAS.FiniteTrial.ScaleState.drawStage line 397
  51. lemma OAI.MatchingFPRAS.FiniteTrial.ScaleState.drawStage_law line 400
  52. def OAI.MatchingFPRAS.FiniteTrial.Layer.drawAppend line 418
  53. lemma OAI.MatchingFPRAS.FiniteTrial.Layer.drawAppend_law line 425
  54. def OAI.MatchingFPRAS.FiniteTrial.successorBitsEquiv line 437
  55. def OAI.MatchingFPRAS.FiniteTrial.drawLayer line 439
  56. lemma OAI.MatchingFPRAS.FiniteTrial.drawLayer_law line 443
  57. def OAI.MatchingFPRAS.FiniteTrial.bitOutput line 455
  58. lemma OAI.MatchingFPRAS.FiniteTrial.bitOutput_nonneg line 457
  59. lemma OAI.MatchingFPRAS.Variation.event_push line 466
  60. lemma OAI.MatchingFPRAS.Variation.event_imageLaw line 476
  61. lemma OAI.MatchingFPRAS.Variation.event_complement line 484
  62. def OAI.MatchingFPRAS.FiniteTrial.amplifiedBits line 498
  63. def OAI.MatchingFPRAS.FiniteTrial.drawTrials line 500
  64. lemma OAI.MatchingFPRAS.FiniteTrial.drawTrials_law line 503
  65. def OAI.MatchingFPRAS.FiniteTrial.amplifiedBitOutput line 509
  66. lemma OAI.MatchingFPRAS.FiniteTrial.amplifiedBitOutput_nonneg line 511
  67. def OAI.MatchingFPRAS.FiniteTrial.accurateBits line 514
  68. theorem OAI.MatchingFPRAS.FiniteTrial.amplifiedBitOutput_success line 516
  69. def OAI.MatchingFPRAS.BitComplexity.PolynomiallyBounded line 538
  70. lemma OAI.MatchingFPRAS.BitComplexity.PolynomiallyBounded.const line 539
  71. lemma OAI.MatchingFPRAS.BitComplexity.PolynomiallyBounded.id line 541
  72. lemma OAI.MatchingFPRAS.BitComplexity.PolynomiallyBounded.add line 543
  73. lemma OAI.MatchingFPRAS.BitComplexity.PolynomiallyBounded.mul line 554
  74. lemma OAI.MatchingFPRAS.BitComplexity.PolynomiallyBounded.pow line 562
  75. def OAI.MatchingFPRAS.BitComplexity.boundK line 569
  76. def OAI.MatchingFPRAS.BitComplexity.boundN line 570
  77. def OAI.MatchingFPRAS.BitComplexity.boundD line 571
  78. def OAI.MatchingFPRAS.BitComplexity.boundS line 572
  79. def OAI.MatchingFPRAS.BitComplexity.boundBits line 573
  80. lemma OAI.MatchingFPRAS.BitComplexity.c line 575
  81. lemma OAI.MatchingFPRAS.BitComplexity.X line 576
  82. lemma OAI.MatchingFPRAS.BitComplexity.boundK_polynomial line 577
  83. lemma OAI.MatchingFPRAS.BitComplexity.boundN_polynomial line 579
  84. lemma OAI.MatchingFPRAS.BitComplexity.boundD_polynomial line 581
  85. lemma OAI.MatchingFPRAS.BitComplexity.boundS_polynomial line 583
  86. lemma OAI.MatchingFPRAS.BitComplexity.ladderL_polynomial line 587
  87. lemma OAI.MatchingFPRAS.BitComplexity.ladderQ_polynomial line 590
  88. lemma OAI.MatchingFPRAS.BitComplexity.ladderM_polynomial line 593
  89. lemma OAI.MatchingFPRAS.BitComplexity.tier_polynomial line 596
  90. lemma OAI.MatchingFPRAS.BitComplexity.edge_polynomial line 599
  91. lemma OAI.MatchingFPRAS.BitComplexity.lambda_polynomial line 602
  92. lemma OAI.MatchingFPRAS.BitComplexity.steps_polynomial line 607
  93. lemma OAI.MatchingFPRAS.BitComplexity.scan_polynomial line 613
  94. lemma OAI.MatchingFPRAS.BitComplexity.total_polynomial line 620
  95. lemma OAI.MatchingFPRAS.BitComplexity.boundBits_polynomial line 628
  96. lemma OAI.MatchingFPRAS.Transport.totalBitsPolynomial_mono line 635
  97. lemma OAI.MatchingFPRAS.BitComplexity.parameters_K_le line 646
  98. lemma OAI.MatchingFPRAS.BitComplexity.parameters_N_le line 652
  99. lemma OAI.MatchingFPRAS.BitComplexity.parameters_D_le line 657
  100. lemma OAI.MatchingFPRAS.BitComplexity.parameters_S_le line 662
  101. lemma OAI.MatchingFPRAS.BitComplexity.amplifiedBits_le_bound line 668
  102. def OAI.MatchingFPRAS.BitComplexity.inputSize line 679
  103. lemma OAI.MatchingFPRAS.BitComplexity.inputSize_pos line 681
  104. lemma OAI.MatchingFPRAS.BitComplexity.scheduledBits_le line 682
  105. theorem OAI.MatchingFPRAS.BitComplexity.polynomial_fair_bits line 691
  106. lemma OAI.MatchingFPRAS.UnitRefresh.pairingCount_pos_even line 700
  107. lemma OAI.MatchingFPRAS.count_le_complete line 713
  108. lemma OAI.MatchingFPRAS.positive_count_even line 722
  109. lemma OAI.MatchingFPRAS.positive_nonempty_two line 726
  110. lemma OAI.MatchingFPRAS.empty_count_one line 729
  111. lemma OAI.MatchingFPRAS.Variation.padSampler_success line 756
  112. lemma OAI.MatchingFPRAS.FiniteTrial.padded_amplified_success line 771
  113. theorem OAI.MatchingFPRAS.FiniteTrial.scheduled_fair_tapes line 779