OAI/Computability/DirectedFeedback/Games/FinishReduction.lean

GitHub source file

98 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.DFVSGames.Explicit.BipartiteGame.product_soundness_rate line 19
  2. theorem OAI.DFVSGames.Explicit.BipartiteGame.product_soundness line 26
  3. theorem OAI.DFVSGames.Explicit.BipartiteGame.product_explicit_soundness line 32
  4. theorem OAI.DFVSGames.Explicit.BipartiteGame.binaryProduct_soundness_rate line 47
  5. theorem OAI.DFVSGames.Explicit.BipartiteGame.binaryProduct_soundness line 55
  6. theorem OAI.DFVSGames.Explicit.BipartiteGame.binaryProduct_explicit_soundness line 62
  7. theorem OAI.DFVSGames.Explicit.ProductPaddedOutput.output_soundness_rate line 84
  8. theorem OAI.DFVSGames.Explicit.ProductPaddedOutput.output_soundness line 95
  9. def OAI.DFVSGames.FinishReduction.of_matrix_reduction line 116
  10. def OAI.DFVSGames.Decoder.SparseLaw.uniformWeights line 234
  11. theorem OAI.DFVSGames.Decoder.SparseLaw.uniformWeights_pos line 237
  12. theorem OAI.DFVSGames.Decoder.SparseLaw.uniformWeights_isProbability line 240
  13. def OAI.DFVSGames.Decoder.SparseLaw.uniformChiSquare line 246
  14. theorem OAI.DFVSGames.Decoder.SparseLaw.uniformChiSquare_eq_pearson line 249
  15. theorem OAI.DFVSGames.Decoder.SparseLaw.uniformChiSquare_eq_secondMoment line 259
  16. theorem OAI.DFVSGames.Decoder.SparseLaw.uniformChiSquare_nonneg line 275
  17. def OAI.DFVSGames.Decoder.SparseLaw.mixture line 279
  18. theorem OAI.DFVSGames.Decoder.SparseLaw.mixture_isProbability line 282
  19. theorem OAI.DFVSGames.Decoder.SparseLaw.uniformChiSquare_mixture line 292
  20. theorem OAI.DFVSGames.Decoder.SparseLaw.totalVariation_le_half_sqrt line 302
  21. def OAI.DFVSGames.Decoder.SparseLaw.independentWeights line 311
  22. theorem OAI.DFVSGames.Decoder.SparseLaw.independentWeights_isProbability line 314
  23. theorem OAI.DFVSGames.Decoder.SparseLaw.uniformChiSquare_independent line 322
  24. theorem OAI.DFVSGames.Decoder.SparseLaw.pow_mul_one_sub_le_one line 336
  25. theorem OAI.DFVSGames.Decoder.SparseLaw.pow_sub_one_le_fraction line 347
  26. theorem OAI.DFVSGames.Decoder.SparseLaw.pow_sub_one_le_twice line 354
  27. def OAI.DFVSGames.Decoder.SparseLaw.lineCount line 367
  28. def OAI.DFVSGames.Decoder.SparseLaw.singletonPairWeights line 371
  29. def OAI.DFVSGames.Decoder.SparseLaw.singletonSamplerWeights line 373
  30. theorem OAI.DFVSGames.Decoder.SparseLaw.singletonSamplerWeights_eq line 378
  31. theorem OAI.DFVSGames.Decoder.SparseLaw.lineCount_sum line 405
  32. theorem OAI.DFVSGames.Decoder.SparseLaw.lineCount_sq line 419
  33. theorem OAI.DFVSGames.Decoder.SparseLaw.lineCount_sq_sum line 424
  34. theorem OAI.DFVSGames.Decoder.SparseLaw.singletonPairWeights_isProbability line 435
  35. theorem OAI.DFVSGames.Decoder.SparseLaw.singletonPairWeights_secondMoment line 444
  36. theorem OAI.DFVSGames.Decoder.SparseLaw.singletonPairWeights_chiSquare line 450
  37. theorem OAI.DFVSGames.Decoder.SparseLaw.paddedSlope_chiSquare line 459
  38. theorem OAI.DFVSGames.Decoder.SparseLaw.paddedSlope_totalVariation line 467
  39. theorem OAI.DFVSGames.Decoder.SparseLaw.paddedSlope_totalVariation_small line 474
  40. theorem OAI.DFVSGames.Decoder.SparseLaw.cubeSlope_totalVariation line 487
  41. theorem OAI.DFVSGames.Decoder.SparseLaw.exists_cubeSlope_totalVariation_le line 518
  42. theorem OAI.DFVSGames.Decoder.SparseLaw.cube_expected_singletons line 545
  43. theorem OAI.DFVSGames.Decoder.SparseLaw.translated_uniform_intercept line 558
  44. theorem OAI.DFVSGames.Decoder.SparseLaw.uniform_intercept_pushforward line 561
  45. theorem OAI.DFVSGames.Decoder.SparseLaw.joint_intercept_pushforward line 568
  46. theorem OAI.DFVSGames.Decoder.SparseLaw.totalVariation_append_uniform_intercept line 581
  47. inductive OAI.DFVSGames.Soundness.PartnerProjection.Slot line 594
  48. structure OAI.DFVSGames.Soundness.PartnerProjection.Triple line 598
  49. def OAI.DFVSGames.Soundness.PartnerProjection.zeroTriple line 604
  50. def OAI.DFVSGames.Soundness.PartnerProjection.parity line 606
  51. def OAI.DFVSGames.Soundness.PartnerProjection.addTriple line 608
  52. theorem OAI.DFVSGames.Soundness.PartnerProjection.parity_add line 611
  53. theorem OAI.DFVSGames.Soundness.PartnerProjection.and_xor line 617
  54. def OAI.DFVSGames.Soundness.PartnerProjection.retained line 621
  55. def OAI.DFVSGames.Soundness.PartnerProjection.freeBit line 627
  56. theorem OAI.DFVSGames.Soundness.PartnerProjection.retained_add line 633
  57. theorem OAI.DFVSGames.Soundness.PartnerProjection.freeBit_add line 637
  58. def OAI.DFVSGames.Soundness.PartnerProjection.complete line 641
  59. theorem OAI.DFVSGames.Soundness.PartnerProjection.parity_complete line 647
  60. theorem OAI.DFVSGames.Soundness.PartnerProjection.retained_complete line 651
  61. theorem OAI.DFVSGames.Soundness.PartnerProjection.freeBit_complete line 655
  62. theorem OAI.DFVSGames.Soundness.PartnerProjection.complete_coordinates line 659
  63. theorem OAI.DFVSGames.Soundness.PartnerProjection.retained_zero line 664
  64. theorem OAI.DFVSGames.Soundness.PartnerProjection.freeBit_zero line 667
  65. theorem OAI.DFVSGames.Soundness.PartnerProjection.complete_zero line 670
  66. theorem OAI.DFVSGames.Soundness.PartnerProjection.complete_kernel_add line 673
  67. structure OAI.DFVSGames.Soundness.PartnerProjection.SourcePoint line 680
  68. structure OAI.DFVSGames.Soundness.PartnerProjection.PartnerPoint line 685
  69. theorem OAI.DFVSGames.Soundness.PartnerProjection.source_ext line 693
  70. theorem OAI.DFVSGames.Soundness.PartnerProjection.partner_ext line 701
  71. def OAI.DFVSGames.Soundness.PartnerProjection.project line 711
  72. def OAI.DFVSGames.Soundness.PartnerProjection.lift line 719
  73. theorem OAI.DFVSGames.Soundness.PartnerProjection.project_lift line 730
  74. theorem OAI.DFVSGames.Soundness.PartnerProjection.project_surjective line 743
  75. theorem OAI.DFVSGames.Soundness.PartnerProjection.homogeneous_preserved line 748
  76. def OAI.DFVSGames.Soundness.PartnerProjection.zeroSource line 751
  77. def OAI.DFVSGames.Soundness.PartnerProjection.zeroPartner line 756
  78. def OAI.DFVSGames.Soundness.PartnerProjection.addSource line 764
  79. def OAI.DFVSGames.Soundness.PartnerProjection.addPartner line 771
  80. theorem OAI.DFVSGames.Soundness.PartnerProjection.project_add line 787
  81. theorem OAI.DFVSGames.Soundness.PartnerProjection.project_zero line 797
  82. def OAI.DFVSGames.Soundness.PartnerProjection.InKernel line 806
  83. theorem OAI.DFVSGames.Soundness.PartnerProjection.kernel_characterization line 809
  84. structure OAI.DFVSGames.Soundness.PartnerProjection.ActiveBits line 835
  85. theorem OAI.DFVSGames.Soundness.PartnerProjection.activeBits_ext line 839
  86. def OAI.DFVSGames.Soundness.PartnerProjection.addActiveBits line 846
  87. def OAI.DFVSGames.Soundness.PartnerProjection.kernelPoint line 853
  88. theorem OAI.DFVSGames.Soundness.PartnerProjection.kernelPoint_add line 858
  89. theorem OAI.DFVSGames.Soundness.PartnerProjection.kernelPoint_mem line 866
  90. def OAI.DFVSGames.Soundness.PartnerProjection.kernelCoefficients line 875
  91. theorem OAI.DFVSGames.Soundness.PartnerProjection.kernelPoint_coefficients line 883
  92. theorem OAI.DFVSGames.Soundness.PartnerProjection.coefficients_kernelPoint line 899
  93. theorem OAI.DFVSGames.Soundness.PartnerProjection.kernelPoint_injective line 906
  94. theorem OAI.DFVSGames.Soundness.PartnerProjection.kernel_unique_coefficients line 917
  95. def OAI.DFVSGames.Soundness.PartnerProjection.extendActive line 926
  96. theorem OAI.DFVSGames.Soundness.PartnerProjection.kernel_realizes_active line 930
  97. theorem OAI.DFVSGames.Soundness.PartnerProjection.kernel_determined_by_active line 939
  98. theorem OAI.DFVSGames.Soundness.PartnerProjection.disjoint_kernels_intersection_zero line 956