OAI/Computability/DirectedFeedback/Analysis/Deletion.lean

GitHub source file

94 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DFVSGames.Fourier.Deletion.trueCount line 11
  2. theorem OAI.DFVSGames.Fourier.Deletion.trueCount_mono line 15
  3. theorem OAI.DFVSGames.Fourier.Deletion.trueCount_eq_zero line 27
  4. structure OAI.DFVSGames.Fourier.Deletion.RestrictionSystem line 36
  5. def OAI.DFVSGames.Fourier.Deletion.Dense line 46
  6. def OAI.DFVSGames.Fourier.Deletion.BadRow line 50
  7. def OAI.DFVSGames.Fourier.Deletion.DeletedSet line 54
  8. def OAI.DFVSGames.Fourier.Deletion.remainder line 58
  9. def OAI.DFVSGames.Fourier.Deletion.removed line 63
  10. theorem OAI.DFVSGames.Fourier.Deletion.remainder_le_original line 68
  11. theorem OAI.DFVSGames.Fourier.Deletion.dense_deletes_whole_row line 77
  12. theorem OAI.DFVSGames.Fourier.Deletion.dense_restriction_remainder_zero line 87
  13. def OAI.DFVSGames.Fourier.Deletion.RestrictionGlobal line 95
  14. theorem OAI.DFVSGames.Fourier.Deletion.remainder_restrictionGlobal line 99
  15. theorem OAI.DFVSGames.Fourier.Deletion.boolean_partition line 114
  16. theorem OAI.DFVSGames.Fourier.Deletion.trueCount_partition line 121
  17. abbrev OAI.DFVSGames.Fourier.MatrixRestrictions.Ambient line 145
  18. abbrev OAI.DFVSGames.Fourier.MatrixRestrictions.Parameter line 149
  19. def OAI.DFVSGames.Fourier.MatrixRestrictions.embed line 152
  20. theorem OAI.DFVSGames.Fourier.MatrixRestrictions.embed_apply line 156
  21. theorem OAI.DFVSGames.Fourier.MatrixRestrictions.embed_injective line 160
  22. theorem OAI.DFVSGames.Fourier.MatrixRestrictions.embed_vanishes line 169
  23. theorem OAI.DFVSGames.Fourier.MatrixRestrictions.embed_range line 177
  24. theorem OAI.DFVSGames.Fourier.MatrixRestrictions.exists_embed_iff line 183
  25. theorem OAI.DFVSGames.Fourier.MatrixRestrictions.quotient_embed_zero line 202
  26. def OAI.DFVSGames.Fourier.MatrixRestrictions.translate line 210
  27. theorem OAI.DFVSGames.Fourier.MatrixRestrictions.translate_injective line 214
  28. theorem OAI.DFVSGames.Fourier.MatrixRestrictions.quotient_translate line 220
  29. def OAI.DFVSGames.Fourier.MatrixRestrictions.embedding line 233
  30. def OAI.DFVSGames.Fourier.MatrixRestrictions.order line 245
  31. def OAI.DFVSGames.Fourier.MatrixRestrictions.restrict line 248
  32. instance OAI.DFVSGames.Fourier.MatrixRestrictions.parameterFintype line 252
  33. theorem OAI.DFVSGames.Fourier.MatrixRestrictions.parameter_card_pos line 260
  34. structure OAI.DFVSGames.Fourier.MatrixRestrictions.Row line 264
  35. structure OAI.DFVSGames.Fourier.MatrixRestrictions.Witness line 269
  36. def OAI.DFVSGames.Fourier.MatrixRestrictions.samples line 275
  37. theorem OAI.DFVSGames.Fourier.MatrixRestrictions.samples_length line 280
  38. theorem OAI.DFVSGames.Fourier.MatrixRestrictions.samples_nonempty line 284
  39. theorem OAI.DFVSGames.Fourier.MatrixRestrictions.mem_samples_iff line 291
  40. theorem OAI.DFVSGames.Fourier.MatrixRestrictions.samples_nodup line 298
  41. def OAI.DFVSGames.Fourier.MatrixRestrictions.system line 304
  42. theorem OAI.DFVSGames.Fourier.MatrixRestrictions.remainder_restriction_count line 315
  43. theorem OAI.DFVSGames.Fourier.MatrixRestrictions.trueCount_eq_countP_inline_MatrixRestrictions line 323
  44. theorem OAI.DFVSGames.Fourier.MatrixRestrictions.samples_trueCount line 330
  45. def OAI.DFVSGames.Fourier.MatrixRestrictions.density line 343
  46. theorem OAI.DFVSGames.Fourier.MatrixRestrictions.density_eq_count_div line 348
  47. theorem OAI.DFVSGames.Fourier.MatrixRestrictions.dense_iff_lt_density line 356
  48. theorem OAI.DFVSGames.Fourier.MatrixRestrictions.remainder_restriction_density line 370
  49. theorem OAI.DFVSGames.Fourier.MatrixRestrictions.remainder_restriction_sq_expect line 385
  50. def OAI.DFVSGames.Fourier.MatrixRestrictions.quotientKernelEquiv line 403
  51. theorem OAI.DFVSGames.Fourier.MatrixRestrictions.quotientKernel_card line 422
  52. theorem OAI.DFVSGames.Fourier.MatrixRestrictions.quotientKernel_filter_card line 430
  53. theorem OAI.DFVSGames.Fourier.MatrixRestrictions.deletedSet_iff_exists_target line 438
  54. theorem OAI.DFVSGames.Fourier.MatrixRestrictions.badRow_codim_le line 451
  55. theorem OAI.DFVSGames.Fourier.MatrixRestrictions.deletedSet_iff_exists_admissible_target line 462
  56. abbrev OAI.DFVSGames.Decoder.AdviceFibers.RowFiber line 488
  57. def OAI.DFVSGames.Decoder.AdviceFibers.kernelDifference line 491
  58. theorem OAI.DFVSGames.Decoder.AdviceFibers.kernelDifference_apply line 504
  59. def OAI.DFVSGames.Decoder.AdviceFibers.assemble line 508
  60. theorem OAI.DFVSGames.Decoder.AdviceFibers.assemble_apply line 512
  61. theorem OAI.DFVSGames.Decoder.AdviceFibers.observed_assemble line 516
  62. def OAI.DFVSGames.Decoder.AdviceFibers.rowFiberEquiv line 522
  63. theorem OAI.DFVSGames.Decoder.AdviceFibers.rowFiberEquiv_coe line 539
  64. theorem OAI.DFVSGames.Decoder.AdviceFibers.rowFiberEquiv_symm line 543
  65. theorem OAI.DFVSGames.Decoder.AdviceFibers.assemble_affine_target line 547
  66. theorem OAI.DFVSGames.Decoder.AdviceFibers.rowFiber_card line 559
  67. theorem OAI.DFVSGames.Decoder.AdviceFibers.rowFiber_expect line 565
  68. abbrev OAI.DFVSGames.Decoder.AdviceFibers.ObservedRow line 574
  69. def OAI.DFVSGames.Decoder.AdviceFibers.observe line 577
  70. def OAI.DFVSGames.Decoder.AdviceFibers.observedBase line 580
  71. theorem OAI.DFVSGames.Decoder.AdviceFibers.observedBase_property line 583
  72. def OAI.DFVSGames.Decoder.AdviceFibers.hiddenCoordinate line 586
  73. theorem OAI.DFVSGames.Decoder.AdviceFibers.observe_assemble_base line 591
  74. def OAI.DFVSGames.Decoder.AdviceFibers.observationEquiv line 596
  75. theorem OAI.DFVSGames.Decoder.AdviceFibers.observationEquiv_apply line 616
  76. theorem OAI.DFVSGames.Decoder.AdviceFibers.observation_expect line 623
  77. theorem OAI.DFVSGames.Decoder.AdviceFibers.observed_hidden_independent line 631
  78. abbrev OAI.DFVSGames.Reduction.ActualOrbit.Ambient line 652
  79. def OAI.DFVSGames.Reduction.ActualOrbit.body line 654
  80. def OAI.DFVSGames.Reduction.ActualOrbit.offset line 657
  81. def OAI.DFVSGames.Reduction.ActualOrbit.Vertex line 659
  82. def OAI.DFVSGames.Reduction.ActualOrbit.vertex line 661
  83. theorem OAI.DFVSGames.Reduction.ActualOrbit.vertex_surjective line 664
  84. instance OAI.DFVSGames.Reduction.ActualOrbit.vertexFintype line 669
  85. instance OAI.DFVSGames.Reduction.ActualOrbit.vertexNonempty line 674
  86. theorem OAI.DFVSGames.Reduction.ActualOrbit.vertex_eq_iff line 677
  87. abbrev OAI.DFVSGames.Reduction.ActualOrbit.TwoSidedVertex line 684
  88. def OAI.DFVSGames.Reduction.ActualOrbit.vertexEquiv line 686
  89. def OAI.DFVSGames.Reduction.ActualOrbit.explicitVertexEquiv line 690
  90. def OAI.DFVSGames.Reduction.ActualOrbit.unfold line 702
  91. theorem OAI.DFVSGames.Reduction.ActualOrbit.add_self_vector line 705
  92. theorem OAI.DFVSGames.Reduction.ActualOrbit.add_cancel_vector line 709
  93. theorem OAI.DFVSGames.Reduction.ActualOrbit.constraint_iff_unfolded line 712
  94. theorem OAI.DFVSGames.Reduction.ActualOrbit.unfold_eq_of_canonical_eq line 724