OAI/Computability/DirectedFeedback/Games/RowErasureSlices.lean

GitHub source file

84 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.DFVSGames.Inverse.RowErasure.SliceFamily line 14
  2. def OAI.DFVSGames.Inverse.RowErasure.SliceFamily.agreement line 22
  3. def OAI.DFVSGames.Inverse.RowErasure.SliceFamily.GoodAdvice line 25
  4. def OAI.DFVSGames.Inverse.RowErasure.SliceFamily.goodAt line 30
  5. def OAI.DFVSGames.Inverse.RowErasure.SliceFamily.erasedUnion line 34
  6. def OAI.DFVSGames.Inverse.RowErasure.SliceFamily.randomizedAgreement line 38
  7. theorem OAI.DFVSGames.Inverse.RowErasure.SliceFamily.mem_erasedUnion_of_good_row line 42
  8. theorem OAI.DFVSGames.Inverse.RowErasure.SliceFamily.original_agreement_lt_of_not_good line 51
  9. theorem OAI.DFVSGames.Inverse.RowErasure.SliceFamily.modified_agreement_le_original_add_randomized line 59
  10. theorem OAI.DFVSGames.Inverse.RowErasure.SliceFamily.modified_agreement_eq_randomized_of_good line 81
  11. theorem OAI.DFVSGames.Inverse.RowErasure.SliceFamily.modified_agreement_lt line 94
  12. theorem OAI.DFVSGames.Inverse.RowErasure.SliceFamily.union_mass_ge_of_inverse_and_erasure line 112
  13. theorem OAI.DFVSGames.Inverse.RowErasure.uniformMass_exists_le_sum line 147
  14. theorem OAI.DFVSGames.Inverse.RowErasure.exists_avoiding_of_sum_bad_lt_one line 164
  15. theorem OAI.DFVSGames.Inverse.RowErasure.exists_avoiding_of_card_mul_bound_lt_one line 180
  16. theorem OAI.DFVSGames.Inverse.RowErasure.SliceFamily.exists_erasure_of_probability_bound line 192
  17. theorem OAI.DFVSGames.Inverse.RowErasure.advice_average_ge line 207
  18. theorem OAI.DFVSGames.Inverse.RowErasure.advice_average_ge_ten_eta_sq_div_card line 228
  19. abbrev OAI.DFVSGames.Inverse.Shortcode.F2 line 247
  20. abbrev OAI.DFVSGames.Inverse.Shortcode.Vector line 248
  21. abbrev OAI.DFVSGames.Inverse.Shortcode.Mat line 249
  22. def OAI.DFVSGames.Inverse.Shortcode.rankOne line 251
  23. def OAI.DFVSGames.Inverse.Shortcode.evaluate line 254
  24. theorem OAI.DFVSGames.Inverse.Shortcode.evaluate_zero line 257
  25. theorem OAI.DFVSGames.Inverse.Shortcode.rankOne_zero_left line 261
  26. theorem OAI.DFVSGames.Inverse.Shortcode.rankOne_zero_right line 266
  27. def OAI.DFVSGames.Inverse.Shortcode.equalityAcceptance line 271
  28. structure OAI.DFVSGames.Inverse.Shortcode.Slice line 274
  29. def OAI.DFVSGames.Inverse.Shortcode.Slice.Contains line 282
  30. def OAI.DFVSGames.Inverse.Shortcode.Slice.points line 286
  31. def OAI.DFVSGames.Inverse.Shortcode.Slice.affineAgreement line 289
  32. def OAI.DFVSGames.Inverse.Shortcode.Slice.constantAgreement line 293
  33. theorem OAI.DFVSGames.Inverse.Shortcode.Slice.constantAgreement_eq_affine line 297
  34. def OAI.DFVSGames.Inverse.Shortcode.HasAffineSlice line 302
  35. theorem OAI.DFVSGames.Inverse.Shortcode.hasAffineSlice_of_constant line 306
  36. def OAI.DFVSGames.Inverse.Shortcode.InversePrinciple line 313
  37. abbrev OAI.DFVSGames.Inverse.RowErasureDescriptions.RowMap line 331
  38. abbrev OAI.DFVSGames.Inverse.RowErasureDescriptions.Description line 333
  39. theorem OAI.DFVSGames.Inverse.RowErasureDescriptions.card_vector line 337
  40. theorem OAI.DFVSGames.Inverse.RowErasureDescriptions.card_rowMap line 340
  41. theorem OAI.DFVSGames.Inverse.RowErasureDescriptions.card_description line 343
  42. def OAI.DFVSGames.Inverse.RowErasureDescriptions.Description.toSlice line 350
  43. def OAI.DFVSGames.Inverse.RowErasureDescriptions.Description.coefficient line 358
  44. def OAI.DFVSGames.Inverse.RowErasureDescriptions.Description.intercept line 361
  45. def OAI.DFVSGames.Inverse.RowErasureDescriptions.padZero line 364
  46. def OAI.DFVSGames.Inverse.RowErasureDescriptions.padSlice line 367
  47. theorem OAI.DFVSGames.Inverse.RowErasureDescriptions.padSlice_contains_iff line 375
  48. theorem OAI.DFVSGames.Inverse.RowErasureDescriptions.padSlice_points line 399
  49. theorem OAI.DFVSGames.Inverse.RowErasureDescriptions.padSlice_affineAgreement line 406
  50. def OAI.DFVSGames.Inverse.RowErasureDescriptions.describe line 412
  51. theorem OAI.DFVSGames.Inverse.RowErasureDescriptions.describe_toSlice line 417
  52. theorem OAI.DFVSGames.Inverse.RowErasureDescriptions.describe_coefficient line 421
  53. theorem OAI.DFVSGames.Inverse.RowErasureDescriptions.describe_intercept line 424
  54. theorem OAI.DFVSGames.Inverse.RowErasureDescriptions.exists_description line 427
  55. def OAI.DFVSGames.Inverse.RowErasureMatrix.rowAdvice line 447
  56. def OAI.DFVSGames.Inverse.RowErasureMatrix.family line 450
  57. theorem OAI.DFVSGames.Inverse.RowErasureMatrix.family_agreement line 464
  58. abbrev OAI.DFVSGames.Inverse.RowErasureMatrix.Samples line 476
  59. def OAI.DFVSGames.Inverse.RowErasureMatrix.left line 478
  60. def OAI.DFVSGames.Inverse.RowErasureMatrix.right line 480
  61. theorem OAI.DFVSGames.Inverse.RowErasureMatrix.expect_prod line 483
  62. theorem OAI.DFVSGames.Inverse.RowErasureMatrix.left_uniform line 492
  63. def OAI.DFVSGames.Inverse.RowErasureMatrix.stepEquiv line 498
  64. theorem OAI.DFVSGames.Inverse.RowErasureMatrix.right_uniform line 510
  65. theorem OAI.DFVSGames.Inverse.RowErasureMatrix.acceptance_eq line 517
  66. theorem OAI.DFVSGames.Inverse.RowErasureMatrix.described_inverse line 534
  67. theorem OAI.DFVSGames.Inverse.RowErasureMatrix.advice_mass_ge_of_inverse_and_erasure line 551
  68. abbrev OAI.DFVSGames.Inverse.AffineWitness.F2 line 573
  69. theorem OAI.DFVSGames.Inverse.AffineWitness.add_self_binary line 580
  70. def OAI.DFVSGames.Inverse.AffineWitness.InSlice line 587
  71. theorem OAI.DFVSGames.Inverse.AffineWitness.translate_target line 591
  72. theorem OAI.DFVSGames.Inverse.AffineWitness.no_affine_representative line 601
  73. def OAI.DFVSGames.Inverse.AffineWitness.shift line 615
  74. theorem OAI.DFVSGames.Inverse.AffineWitness.shift_apply line 618
  75. theorem OAI.DFVSGames.Inverse.AffineWitness.shift_zero line 621
  76. theorem OAI.DFVSGames.Inverse.AffineWitness.shift_add line 626
  77. theorem OAI.DFVSGames.Inverse.AffineWitness.shift_preserves_slice line 632
  78. theorem OAI.DFVSGames.Inverse.AffineWitness.shift_preserves_target line 646
  79. theorem OAI.DFVSGames.Inverse.AffineWitness.normalize line 651
  80. theorem OAI.DFVSGames.Inverse.AffineWitness.columns_iff_span line 668
  81. theorem OAI.DFVSGames.Inverse.AffineWitness.explicit_slice_iff line 681
  82. theorem OAI.DFVSGames.Inverse.AffineWitness.translate_explicit_target line 689
  83. theorem OAI.DFVSGames.Inverse.folded_action_injective line 704
  84. theorem OAI.DFVSGames.Inverse.folded_action_card_mul_agreement_le line 736