OAI/Computability/DirectedFeedback/Machines/MachineSingleOrbitBridge.lean

GitHub source file

80 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.DFVSGames.Explicit.MachineSingleOrbitBridge.SingleAddress.vertexCount line 15
  2. abbrev OAI.DFVSGames.Explicit.MachineSingleOrbitBridge.SingleAddress.queryAddress line 16
  3. abbrev OAI.DFVSGames.Explicit.MachineSingleOrbitBridge.SingleAddress.addressEdge line 17
  4. abbrev OAI.DFVSGames.Explicit.MachineSingleOrbitBridge.SingleAddress.outputInstance line 18
  5. abbrev OAI.DFVSGames.Explicit.MachineSingleOrbitBridge.SingleAddress.tableOutput line 19
  6. theorem OAI.DFVSGames.Explicit.MachineSingleOrbitBridge.old_addressEdge_eq_double line 23
  7. theorem OAI.DFVSGames.Explicit.MachineSingleOrbitBridge.old_outputInstance_eq_double line 32
  8. theorem OAI.DFVSGames.Explicit.MachineSingleOrbitBridge.old_tableOutput_eq_double line 41
  9. def OAI.DFVSGames.Explicit.MachineSingleOrbitBridge.output line 46
  10. theorem OAI.DFVSGames.Explicit.MachineSingleOrbitBridge.old_output_eq_double line 50
  11. def OAI.DFVSGames.Explicit.MachineSingleOrbitBridge.doubledComputableInPolyTime line 57
  12. def OAI.DFVSGames.Explicit.MachineSingleOrbitBridge.computableInPolyTime line 72
  13. theorem OAI.DFVSGames.Explicit.MachineSingleOrbitBridge.workAlphabetFinite line 84
  14. def OAI.DFVSGames.FromMatrixGap.reduction line 109
  15. theorem OAI.DFVSGames.Inverse.binary_kernel_finrank_lower line 154
  16. theorem OAI.DFVSGames.Inverse.binary_kernel_card_lower line 169
  17. theorem OAI.DFVSGames.Decoder.DimensionSelection.exists_logical_dimension line 181
  18. theorem OAI.DFVSGames.Decoder.DimensionSelection.kernel_fraction_le line 204
  19. theorem OAI.DFVSGames.Decoder.DimensionSelection.kernel_fraction_lt line 213
  20. def OAI.DFVSGames.Decoder.NoiseSampler.samplerLaw line 233
  21. theorem OAI.DFVSGames.Decoder.NoiseSampler.samplerLaw_nonneg line 238
  22. theorem OAI.DFVSGames.Decoder.NoiseSampler.samplerLaw_eq_count line 248
  23. theorem OAI.DFVSGames.Decoder.NoiseSampler.samplerLaw_sum line 256
  24. theorem OAI.DFVSGames.Decoder.NoiseSampler.sample_expect_eq line 266
  25. theorem OAI.DFVSGames.Decoder.NoiseSampler.samplerLaw_normalized line 270
  26. theorem OAI.DFVSGames.Decoder.NoiseSampler.rat_expect_cast line 275
  27. theorem OAI.DFVSGames.Decoder.NoiseSampler.samplerLaw_eq_rat_count line 280
  28. theorem OAI.DFVSGames.Decoder.NoiseSampler.sample_kernel_eq_eigenvalue line 293
  29. theorem OAI.DFVSGames.Decoder.NoiseSampler.detection_add_eigenvalue line 299
  30. theorem OAI.DFVSGames.Decoder.NoiseSampler.detection_eigenvalue_le line 312
  31. theorem OAI.DFVSGames.Decoder.NoiseSampler.detection_eigenvalue_le_complement line 319
  32. theorem OAI.DFVSGames.Decoder.NoiseSampler.rational_detection_eigenvalue_le line 326
  33. theorem OAI.DFVSGames.Appendix.RankAdditivity.ker_add_of_disjoint line 346
  34. theorem OAI.DFVSGames.Appendix.RankAdditivity.finrank_add_eq_iff line 369
  35. theorem OAI.DFVSGames.Appendix.RankAdditivity.range_left_le_range_add line 398
  36. theorem OAI.DFVSGames.Appendix.RankAdditivity.ker_add_le_ker_left line 416
  37. def OAI.DFVSGames.Appendix.RankAdditivity.RankBelow line 423
  38. theorem OAI.DFVSGames.Appendix.RankAdditivity.add_remainder line 428
  39. theorem OAI.DFVSGames.Appendix.RankAdditivity.rankBelow_iff line 432
  40. theorem OAI.DFVSGames.Appendix.RankAdditivity.range_le_of_rankBelow line 441
  41. theorem OAI.DFVSGames.Appendix.RankAdditivity.ker_le_of_rankBelow line 450
  42. theorem OAI.DFVSGames.Appendix.RankAdditivity.range_remainder_eq_range_on_kernel line 459
  43. theorem OAI.DFVSGames.Appendix.RankAdditivity.mem_ker_of_apply_mem_range_remainder line 483
  44. def OAI.DFVSGames.Appendix.CompressionCount.base line 510
  45. theorem OAI.DFVSGames.Appendix.CompressionCount.base_apply line 513
  46. def OAI.DFVSGames.Appendix.CompressionCount.compress line 517
  47. theorem OAI.DFVSGames.Appendix.CompressionCount.compress_apply line 520
  48. def OAI.DFVSGames.Appendix.CompressionCount.Fiber line 523
  49. abbrev OAI.DFVSGames.Appendix.CompressionCount.Parameters line 528
  50. def OAI.DFVSGames.Appendix.CompressionCount.graph line 531
  51. def OAI.DFVSGames.Appendix.CompressionCount.inclusion line 534
  52. def OAI.DFVSGames.Appendix.CompressionCount.lower line 537
  53. def OAI.DFVSGames.Appendix.CompressionCount.lift line 540
  54. theorem OAI.DFVSGames.Appendix.CompressionCount.lift_apply line 544
  55. theorem OAI.DFVSGames.Appendix.CompressionCount.compress_lift line 550
  56. theorem OAI.DFVSGames.Appendix.CompressionCount.graph_injective line 555
  57. theorem OAI.DFVSGames.Appendix.CompressionCount.inclusion_injective line 560
  58. theorem OAI.DFVSGames.Appendix.CompressionCount.lower_surjective line 566
  59. theorem OAI.DFVSGames.Appendix.CompressionCount.range_lift_sub_base line 573
  60. theorem OAI.DFVSGames.Appendix.CompressionCount.range_lift line 579
  61. theorem OAI.DFVSGames.Appendix.CompressionCount.finrank_base line 599
  62. theorem OAI.DFVSGames.Appendix.CompressionCount.lift_rank_order line 605
  63. def OAI.DFVSGames.Appendix.CompressionCount.toFiber line 612
  64. theorem OAI.DFVSGames.Appendix.CompressionCount.lift_injective line 616
  65. theorem OAI.DFVSGames.Appendix.CompressionCount.natCard_linearMap line 630
  66. theorem OAI.DFVSGames.Appendix.CompressionCount.card_parameters line 644
  67. theorem OAI.DFVSGames.Appendix.CompressionCount.fiber_geometry line 652
  68. theorem OAI.DFVSGames.Appendix.CompressionCount.snd_mem_range line 661
  69. def OAI.DFVSGames.Appendix.CompressionCount.linearSection line 678
  70. theorem OAI.DFVSGames.Appendix.CompressionCount.section_spec line 683
  71. def OAI.DFVSGames.Appendix.CompressionCount.extractedF line 688
  72. def OAI.DFVSGames.Appendix.CompressionCount.extractedH line 693
  73. theorem OAI.DFVSGames.Appendix.CompressionCount.extracted_lower line 699
  74. theorem OAI.DFVSGames.Appendix.CompressionCount.difference_ext_snd line 710
  75. theorem OAI.DFVSGames.Appendix.CompressionCount.lift_extracted line 726
  76. theorem OAI.DFVSGames.Appendix.CompressionCount.toFiber_bijective line 751
  77. def OAI.DFVSGames.Appendix.CompressionCount.fiberEquiv line 759
  78. theorem OAI.DFVSGames.Appendix.CompressionCount.fiber_remainder_rank line 763
  79. theorem OAI.DFVSGames.Appendix.CompressionCount.fiber_rank line 770
  80. theorem OAI.DFVSGames.Appendix.CompressionCount.card_fiber line 774