OAI/Computability/DirectedFeedback/Encoding/ActualGoodRows.lean

GitHub source file

53 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.DFVSGames.Inverse.RowErasureMatrix.exists_replacement_of_budget line 15
  2. theorem OAI.DFVSGames.Inverse.RowErasureMatrix.advice_mass_ge_of_inverse_and_budget line 41
  3. theorem OAI.DFVSGames.Inverse.RowErasure.eventually_log_unionBound_neg line 63
  4. theorem OAI.DFVSGames.Inverse.RowErasure.eventually_unionBound_lt_one line 116
  5. theorem OAI.DFVSGames.Inverse.RowErasure.exists_unionBound_threshold line 133
  6. theorem OAI.DFVSGames.Inverse.RowErasureMatrix.exists_erasure_threshold line 152
  7. theorem OAI.DFVSGames.Inverse.RowErasureMatrix.exists_fixed_context_advice_threshold line 165
  8. theorem OAI.DFVSGames.Inverse.RowErasureMatrix.exists_contextual_advice_threshold line 180
  9. def OAI.DFVSGames.Decoder.ActualGoodRows.table line 223
  10. theorem OAI.DFVSGames.Decoder.ActualGoodRows.table_acceptance line 230
  11. def OAI.DFVSGames.Decoder.ActualGoodRows.adviceMass line 248
  12. def OAI.DFVSGames.Decoder.ActualGoodRows.goodRowMass line 255
  13. theorem OAI.DFVSGames.Decoder.ActualGoodRows.goodRowMass_pos line 258
  14. theorem OAI.DFVSGames.Decoder.ActualGoodRows.exists_actual_advice_threshold line 263
  15. def OAI.DFVSGames.Decoder.ConstantSelection.visibleMass line 307
  16. def OAI.DFVSGames.Decoder.ConstantSelection.conditionalMass line 310
  17. def OAI.DFVSGames.Decoder.ConstantSelection.decodingMass line 313
  18. def OAI.DFVSGames.Decoder.ConstantSelection.variationBudget line 316
  19. theorem OAI.DFVSGames.Decoder.ConstantSelection.visibleMass_pos line 319
  20. theorem OAI.DFVSGames.Decoder.ConstantSelection.conditionalMass_pos line 324
  21. theorem OAI.DFVSGames.Decoder.ConstantSelection.decodingMass_pos line 329
  22. theorem OAI.DFVSGames.Decoder.ConstantSelection.variationBudget_pos line 333
  23. theorem OAI.DFVSGames.Decoder.ConstantSelection.variationBudget_suffices line 337
  24. theorem OAI.DFVSGames.Decoder.ConstantSelection.cube_exponential_antitone line 349
  25. theorem OAI.DFVSGames.Decoder.ConstantSelection.exists_simultaneous_cube line 357
  26. theorem OAI.DFVSGames.Decoder.ConstantSelection.exists_matrix_cube line 376
  27. structure OAI.DFVSGames.Decoder.MatrixGapChoice.InverseParameters line 398
  28. theorem OAI.DFVSGames.Decoder.MatrixGapChoice.eta_lt_one line 420
  29. theorem OAI.DFVSGames.Decoder.MatrixGapChoice.exists_inverse_parameters line 428
  30. theorem OAI.DFVSGames.Decoder.MatrixGapChoice.exists_cube line 465
  31. def OAI.DFVSGames.Inverse.RowErasure.SliceFamily.chosenDescription line 493
  32. theorem OAI.DFVSGames.Inverse.RowErasure.SliceFamily.chosenDescription_spec line 498
  33. theorem OAI.DFVSGames.Inverse.RowErasure.SliceFamily.chosenDescription_congr line 507
  34. def OAI.DFVSGames.Inverse.RowErasure.SliceFamily.selectedDescription line 517
  35. theorem OAI.DFVSGames.Inverse.RowErasure.SliceFamily.selectedDescription_of_good line 523
  36. theorem OAI.DFVSGames.Inverse.RowErasure.SliceFamily.good_of_selectedDescription line 529
  37. theorem OAI.DFVSGames.Inverse.RowErasure.SliceFamily.selectedDescription_spec line 538
  38. theorem OAI.DFVSGames.Inverse.RowErasure.SliceFamily.selectedDescription_congr line 549
  39. def OAI.DFVSGames.Inverse.RowErasure.SliceFamily.selectedEvent line 557
  40. def OAI.DFVSGames.Inverse.RowErasure.SliceFamily.selectedMatch line 561
  41. theorem OAI.DFVSGames.Inverse.RowErasure.SliceFamily.selectedEvent_iff_of_advice line 566
  42. theorem OAI.DFVSGames.Inverse.RowErasure.SliceFamily.selectedMatch_iff_of_advice line 579
  43. theorem OAI.DFVSGames.Inverse.RowErasure.SliceFamily.selectedEvent_good line 594
  44. theorem OAI.DFVSGames.Inverse.RowErasure.SliceFamily.selectedMatch_event line 600
  45. def OAI.DFVSGames.Inverse.RowErasure.SelectionPartition.fiber line 617
  46. def OAI.DFVSGames.Inverse.RowErasure.SelectionPartition.event line 620
  47. def OAI.DFVSGames.Inverse.RowErasure.SelectionPartition.matchEvent line 624
  48. theorem OAI.DFVSGames.Inverse.RowErasure.SelectionPartition.expect_le_expect_of_fiber_sum_le line 628
  49. theorem OAI.DFVSGames.Inverse.RowErasure.SelectionPartition.sum_event_mul_fiber line 639
  50. theorem OAI.DFVSGames.Inverse.RowErasure.SelectionPartition.sum_event_fiber line 664
  51. theorem OAI.DFVSGames.Inverse.RowErasure.SelectionPartition.sum_match_fiber line 673
  52. theorem OAI.DFVSGames.Inverse.RowErasure.SelectionPartition.mass_event_ge line 691
  53. theorem OAI.DFVSGames.Inverse.RowErasure.SelectionPartition.mass_match_ge line 728