OAI/Computability/DirectedFeedback/Machines/MachineProductFinish.lean

GitHub source file

83 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.DFVSGames.Explicit.MachineProductFinish.base_ready line 19
  2. def OAI.DFVSGames.Explicit.MachineProductFinish.afterRows line 28
  3. theorem OAI.DFVSGames.Explicit.MachineProductFinish.afterRows_output line 33
  4. theorem OAI.DFVSGames.Explicit.MachineProductFinish.allRows_eq line 39
  5. theorem OAI.DFVSGames.Explicit.MachineProductFinish.afterRows_accumulator line 45
  6. def OAI.DFVSGames.Explicit.MachineProductFinish.finishInTime line 56
  7. theorem OAI.DFVSGames.Explicit.MachineProductFinish.finishCost_le_uniform line 77
  8. theorem OAI.DFVSGames.Explicit.MachineProductFinish.finish_afterRows line 88
  9. def OAI.DFVSGames.Explicit.MachineProductRuntime.loopPolynomial line 127
  10. theorem OAI.DFVSGames.Explicit.MachineProductRuntime.loop_budget line 131
  11. def OAI.DFVSGames.Explicit.MachineProductRuntime.prefixPolynomial line 140
  12. def OAI.DFVSGames.Explicit.MachineProductRuntime.prefixInTime line 143
  13. def OAI.DFVSGames.Explicit.MachineProductRuntime.timePolynomial line 165
  14. def OAI.DFVSGames.Explicit.MachineProductRuntime.outputInTime line 169
  15. abbrev OAI.DFVSGames.Explicit.MachineProductRuntime.Input line 196
  16. def OAI.DFVSGames.Explicit.MachineProductRuntime.construct line 198
  17. def OAI.DFVSGames.Explicit.MachineProductRuntime.computation line 201
  18. theorem OAI.DFVSGames.Explicit.MachineProductRuntime.finiteAlphabet line 214
  19. def OAI.DFVSGames.Explicit.MachineProductRuntime.certify line 220
  20. def OAI.DFVSGames.Explicit.MachineProductRuntime.compose line 230
  21. theorem OAI.DFVSGames.Explicit.MachineProductRuntime.compose_finiteAlphabet line 237
  22. def OAI.DFVSGames.Repetition.Analytic.quadraticMass line 257
  23. def OAI.DFVSGames.Repetition.Analytic.gatedCorrelation line 260
  24. def OAI.DFVSGames.Repetition.Analytic.gatedMinimum line 263
  25. def OAI.DFVSGames.Repetition.Analytic.gatedMaximum line 266
  26. theorem OAI.DFVSGames.Repetition.Analytic.quadraticMass_nonnegative line 269
  27. theorem OAI.DFVSGames.Repetition.Analytic.gatedCorrelation_nonnegative line 276
  28. theorem OAI.DFVSGames.Repetition.Analytic.gatedCorrelation_le_mass line 285
  29. theorem OAI.DFVSGames.Repetition.Analytic.gatedMinimum_nonnegative line 296
  30. theorem OAI.DFVSGames.Repetition.Analytic.gatedMinimum_le_mass line 304
  31. theorem OAI.DFVSGames.Repetition.Analytic.gatedMinimum_add_maximum_le line 317
  32. theorem OAI.DFVSGames.Repetition.Analytic.gatedCorrelation_sq_le_min_mul_max line 333
  33. theorem OAI.DFVSGames.Repetition.Analytic.gatedCorrelation_sq_le_min_quadratic line 356
  34. theorem OAI.DFVSGames.Repetition.Analytic.gatedMinimum_cheeger line 366
  35. theorem OAI.DFVSGames.Repetition.Analytic.gatedMinimum_near_one line 378
  36. theorem OAI.DFVSGames.Repetition.Analytic.gatedMinimum_unit_mass line 398
  37. def OAI.DFVSGames.Repetition.rowSquareMass line 425
  38. def OAI.DFVSGames.Repetition.paddedAmplitude line 427
  39. def OAI.DFVSGames.Repetition.paddedLabel line 431
  40. theorem OAI.DFVSGames.Repetition.paddedAmplitude_nonnegative line 436
  41. theorem OAI.DFVSGames.Repetition.paddedAmplitude_row line 447
  42. def OAI.DFVSGames.Repetition.pairEnergy line 458
  43. def OAI.DFVSGames.Repetition.pairOverlap line 464
  44. theorem OAI.DFVSGames.Repetition.pairEnergy_nonnegative line 471
  45. theorem OAI.DFVSGames.Repetition.pairEnergy_le_padded line 483
  46. theorem OAI.DFVSGames.Repetition.pairQuadraticMass_eq_one line 523
  47. theorem OAI.DFVSGames.Repetition.pairGatedCorrelation_eq_energy line 545
  48. theorem OAI.DFVSGames.Repetition.pairGatedMinimum_eq_overlap line 555
  49. theorem OAI.DFVSGames.Repetition.pairEnergy_le_one_of_unit_rows line 565
  50. theorem OAI.DFVSGames.Repetition.pairOverlap_ge_energy line 577
  51. def OAI.DFVSGames.Foundations.CorrelatedSampling.firstAccepted line 596
  52. theorem OAI.DFVSGames.Foundations.CorrelatedSampling.first_union_common line 601
  53. def OAI.DFVSGames.Foundations.CorrelatedSampling.thresholdSample line 624
  54. theorem OAI.DFVSGames.Foundations.CorrelatedSampling.thresholdSample_agreement line 628
  55. def OAI.DFVSGames.Foundations.CorrelatedSampling.totalVariation line 647
  56. def OAI.DFVSGames.Foundations.CorrelatedSampling.overlapMass line 649
  57. def OAI.DFVSGames.Foundations.CorrelatedSampling.unionMass line 651
  58. theorem OAI.DFVSGames.Foundations.CorrelatedSampling.totalVariation_nonneg line 653
  59. theorem OAI.DFVSGames.Foundations.CorrelatedSampling.overlapMass_nonneg line 657
  60. theorem OAI.DFVSGames.Foundations.CorrelatedSampling.min_abs_identity_inline_Basic line 661
  61. theorem OAI.DFVSGames.Foundations.CorrelatedSampling.max_abs_identity_inline_Basic line 668
  62. theorem OAI.DFVSGames.Foundations.CorrelatedSampling.overlapMass_eq line 675
  63. theorem OAI.DFVSGames.Foundations.CorrelatedSampling.unionMass_eq line 683
  64. theorem OAI.DFVSGames.Foundations.CorrelatedSampling.totalVariation_le_one line 691
  65. theorem OAI.DFVSGames.Foundations.CorrelatedSampling.overlap_union_ratio line 698
  66. theorem OAI.DFVSGames.Foundations.CorrelatedSampling.overlap_union_ratio_lower_bound line 704
  67. theorem OAI.DFVSGames.Foundations.CorrelatedSampling.first_union_disagreement_upper_bound line 713
  68. def OAI.DFVSGames.Foundations.CorrelatedSampling.eventMass line 725
  69. theorem OAI.DFVSGames.Foundations.CorrelatedSampling.eventMass_nonneg line 728
  70. theorem OAI.DFVSGames.Foundations.CorrelatedSampling.eventMass_complement line 734
  71. def OAI.DFVSGames.Foundations.CorrelatedSampling.geometricMass line 746
  72. theorem OAI.DFVSGames.Foundations.CorrelatedSampling.geometricMass_nonneg line 750
  73. theorem OAI.DFVSGames.Foundations.CorrelatedSampling.geometricMass_identity line 756
  74. def OAI.DFVSGames.Foundations.CorrelatedSampling.firstHitWeight line 767
  75. theorem OAI.DFVSGames.Foundations.CorrelatedSampling.firstHitWeight_nonneg line 775
  76. theorem OAI.DFVSGames.Foundations.CorrelatedSampling.firstHitWeight_none line 789
  77. theorem OAI.DFVSGames.Foundations.CorrelatedSampling.firstHitWeight_some line 795
  78. theorem OAI.DFVSGames.Foundations.CorrelatedSampling.firstHitWeight_normalized line 805
  79. def OAI.DFVSGames.Foundations.CorrelatedSampling.goodFirstMass line 818
  80. theorem OAI.DFVSGames.Foundations.CorrelatedSampling.goodFirstMass_eq line 821
  81. theorem OAI.DFVSGames.Foundations.CorrelatedSampling.goodFirstMass_exact line 832
  82. theorem OAI.DFVSGames.Foundations.CorrelatedSampling.commonMass_le_acceptMass line 848
  83. theorem OAI.DFVSGames.Foundations.CorrelatedSampling.goodFirstMass_lower_bound line 855