OAI/Computability/DirectedFeedback/Games/RowErasureSliceUniform.lean

GitHub source file

69 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.DFVSGames.Inverse.RowErasureColumnMass.card_affineSlice line 19
  2. theorem OAI.DFVSGames.Inverse.RowErasureColumnMass.card_rowFiber line 27
  3. theorem OAI.DFVSGames.Inverse.RowErasureColumnMass.card_rowFiber_eq_mul line 34
  4. theorem OAI.DFVSGames.Inverse.RowErasureColumnMass.card_rowFiber_le_mul line 41
  5. theorem OAI.DFVSGames.Inverse.RowErasureColumnMass.column_fraction_eq line 52
  6. theorem OAI.DFVSGames.Inverse.RowErasureColumnMass.column_fraction_ge line 64
  7. theorem OAI.DFVSGames.Inverse.Shortcode.Slice.difference_row_zero line 87
  8. theorem OAI.DFVSGames.Inverse.Shortcode.Slice.difference_range_le line 100
  9. theorem OAI.DFVSGames.Inverse.Shortcode.Slice.difference_vanishes_columns line 107
  10. theorem OAI.DFVSGames.Inverse.Shortcode.Slice.directionEmbedding_surjective line 119
  11. def OAI.DFVSGames.Inverse.Shortcode.Slice.directionEquiv line 139
  12. theorem OAI.DFVSGames.Inverse.Shortcode.Slice.directionEquiv_val line 144
  13. instance OAI.DFVSGames.Inverse.Shortcode.Slice.directionsFintype line 148
  14. theorem OAI.DFVSGames.Inverse.Shortcode.Slice.card_points_eq_directions line 156
  15. theorem OAI.DFVSGames.Inverse.Shortcode.Slice.points_expect_eq_directions line 160
  16. theorem OAI.DFVSGames.Inverse.Shortcode.Slice.directionMatrix_evaluate line 168
  17. theorem OAI.DFVSGames.Inverse.Shortcode.Slice.direction_affine_target line 174
  18. theorem OAI.DFVSGames.Inverse.Shortcode.Slice.affineAgreement_eq_directions line 185
  19. def OAI.DFVSGames.Inverse.RowErasureDescriptionColumnMass.rowFiber line 207
  20. theorem OAI.DFVSGames.Inverse.RowErasureDescriptionColumnMass.mem_rowFiber line 211
  21. def OAI.DFVSGames.Inverse.RowErasureDescriptionColumnMass.rowOnly line 215
  22. theorem OAI.DFVSGames.Inverse.RowErasureDescriptionColumnMass.rowOnly_contains_iff line 223
  23. theorem OAI.DFVSGames.Inverse.RowErasureDescriptionColumnMass.rowOnly_points line 236
  24. theorem OAI.DFVSGames.Inverse.RowErasureDescriptionColumnMass.contains_rowOnly line 242
  25. theorem OAI.DFVSGames.Inverse.RowErasureDescriptionColumnMass.rowOnly_columnSpan line 246
  26. theorem OAI.DFVSGames.Inverse.RowErasureDescriptionColumnMass.rowOnly_quotient_finrank line 252
  27. theorem OAI.DFVSGames.Inverse.RowErasureDescriptionColumnMass.rowFiber_card line 262
  28. theorem OAI.DFVSGames.Inverse.RowErasureDescriptionColumnMass.rowFiber_nonempty line 271
  29. theorem OAI.DFVSGames.Inverse.RowErasureDescriptionColumnMass.column_fraction_ge line 279
  30. def OAI.DFVSGames.Inverse.RowErasure.SliceFamily.selectedPoints line 313
  31. def OAI.DFVSGames.Inverse.RowErasure.SliceFamily.selectedHit line 319
  32. theorem OAI.DFVSGames.Inverse.RowErasure.SliceFamily.selectedPoints_of_good line 323
  33. theorem OAI.DFVSGames.Inverse.RowErasure.SliceFamily.selectedHit_of_good line 330
  34. theorem OAI.DFVSGames.Inverse.RowErasure.SliceFamily.selectedPoints_support line 343
  35. theorem OAI.DFVSGames.Inverse.RowErasure.SliceFamily.selectedEvent_iff_points line 357
  36. theorem OAI.DFVSGames.Inverse.RowErasure.SliceFamily.selectedMatch_iff_points line 373
  37. theorem OAI.DFVSGames.Inverse.RowErasure.SliceFamily.selectedPoints_match_sum line 391
  38. theorem OAI.DFVSGames.Inverse.RowErasureMatrix.selectedPoints_column_mass line 420
  39. theorem OAI.DFVSGames.Inverse.RowErasureMatrix.selected_event_mass_ge line 437
  40. theorem OAI.DFVSGames.Inverse.RowErasureMatrix.selected_match_mass_ge line 464
  41. def OAI.DFVSGames.Inverse.RowErasureMatrix.selectedEventMass line 488
  42. def OAI.DFVSGames.Inverse.RowErasureMatrix.selectedMatchMass line 491
  43. theorem OAI.DFVSGames.Inverse.RowErasureMatrix.selectedEventMass_ge line 494
  44. theorem OAI.DFVSGames.Inverse.RowErasureMatrix.selectedMatchMass_ge line 507
  45. theorem OAI.DFVSGames.Inverse.RowErasureMatrix.selectedEventMass_weighted_ge line 514
  46. theorem OAI.DFVSGames.Inverse.RowErasureMatrix.selectedMatchMass_weighted_ge line 532
  47. theorem OAI.DFVSGames.Inverse.RowErasureMatrix.selectedMatchMass_conditional_ge line 546
  48. theorem OAI.DFVSGames.Inverse.RowErasureMatrix.selectedEventMass_contextual_ge line 553
  49. theorem OAI.DFVSGames.Inverse.RowErasureMatrix.selectedMatchMass_contextual_ge line 562
  50. abbrev OAI.DFVSGames.Decoder.ActualEvents.Context line 588
  51. abbrev OAI.DFVSGames.Decoder.ActualEvents.Sample line 591
  52. abbrev OAI.DFVSGames.Decoder.ActualEvents.FullTableSample line 594
  53. def OAI.DFVSGames.Decoder.ActualEvents.fullTableEquiv line 597
  54. def OAI.DFVSGames.Decoder.ActualEvents.unrestricted line 632
  55. def OAI.DFVSGames.Decoder.ActualEvents.sliceEvent line 635
  56. def OAI.DFVSGames.Decoder.ActualEvents.targetHit line 641
  57. theorem OAI.DFVSGames.Decoder.ActualEvents.targetHit_implies_slice line 647
  58. theorem OAI.DFVSGames.Decoder.ActualEvents.uniform_probability_expect line 655
  59. theorem OAI.DFVSGames.Decoder.ActualEvents.unrestricted_slice_mass line 662
  60. theorem OAI.DFVSGames.Decoder.ActualEvents.unrestricted_match_mass line 676
  61. theorem OAI.DFVSGames.Decoder.ActualEvents.slice_probability_lower line 698
  62. theorem OAI.DFVSGames.Decoder.ActualEvents.target_probability_lower line 709
  63. def OAI.DFVSGames.Inverse.RowErasureDescriptions.Description.withTarget line 725
  64. theorem OAI.DFVSGames.Inverse.RowErasureDescriptions.Description.withTarget_toSlice line 729
  65. theorem OAI.DFVSGames.Inverse.RowErasureDescriptions.Description.withTarget_coefficient line 733
  66. theorem OAI.DFVSGames.Inverse.RowErasureDescriptions.Description.withTarget_intercept line 737
  67. theorem OAI.DFVSGames.Inverse.RowErasureMatrix.exists_normalizedChosenDescription line 753
  68. def OAI.DFVSGames.Inverse.RowErasureMatrix.normalizedChosenDescription line 792
  69. theorem OAI.DFVSGames.Inverse.RowErasureMatrix.normalizedChosenDescription_spec line 802