OAI/Computability/DirectedFeedback/Games/AffineWitnessNormalization.lean

GitHub source file

68 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.DFVSGames.Inverse.AffineWitness.Slice line 13
  2. def OAI.DFVSGames.Inverse.AffineWitness.sliceShift line 16
  3. theorem OAI.DFVSGames.Inverse.AffineWitness.sliceShift_zero line 22
  4. theorem OAI.DFVSGames.Inverse.AffineWitness.sliceShift_add line 29
  5. theorem OAI.DFVSGames.Inverse.AffineWitness.agreement_count_le line 37
  6. theorem OAI.DFVSGames.Inverse.AffineWitness.normalize_of_good_count line 61
  7. def OAI.DFVSGames.Inverse.Shortcode.Slice.rowMap line 85
  8. def OAI.DFVSGames.Inverse.Shortcode.Slice.columnSpan line 88
  9. abbrev OAI.DFVSGames.Inverse.Shortcode.Slice.Directions line 91
  10. def OAI.DFVSGames.Inverse.Shortcode.Slice.directionMap line 94
  11. def OAI.DFVSGames.Inverse.Shortcode.Slice.directionMatrix line 98
  12. theorem OAI.DFVSGames.Inverse.Shortcode.Slice.directionMatrix_injective line 101
  13. theorem OAI.DFVSGames.Inverse.Shortcode.Slice.directionMatrix_row line 112
  14. theorem OAI.DFVSGames.Inverse.Shortcode.Slice.directionMatrix_column line 121
  15. theorem OAI.DFVSGames.Inverse.Shortcode.Slice.contains_add_direction line 131
  16. def OAI.DFVSGames.Inverse.Shortcode.Slice.directionEmbedding line 148
  17. theorem OAI.DFVSGames.Inverse.Shortcode.Slice.columnSpan_finrank_le line 158
  18. theorem OAI.DFVSGames.Inverse.Shortcode.Slice.quotient_finrank_ge line 166
  19. theorem OAI.DFVSGames.Inverse.Shortcode.Slice.rowKernel_finrank_ge line 174
  20. theorem OAI.DFVSGames.Inverse.Shortcode.Slice.card_directions line 183
  21. theorem OAI.DFVSGames.Inverse.Shortcode.Slice.card_directions_le line 190
  22. theorem OAI.DFVSGames.Inverse.Shortcode.Slice.pow_dimension_le_card line 199
  23. theorem OAI.DFVSGames.Inverse.Shortcode.Slice.evaluate_eq_toLin line 226
  24. theorem OAI.DFVSGames.Inverse.Shortcode.Slice.row_equations_iff line 229
  25. theorem OAI.DFVSGames.Inverse.Shortcode.Slice.contains_iff_inSlice line 250
  26. def OAI.DFVSGames.Inverse.Shortcode.Slice.linearSliceEquiv line 268
  27. theorem OAI.DFVSGames.Inverse.Shortcode.Slice.affineAgreement_eq_of_target_eq line 285
  28. theorem OAI.DFVSGames.Inverse.Shortcode.Slice.affineAgreement_eq_of_linear_target_eq line 296
  29. theorem OAI.DFVSGames.Inverse.Shortcode.Slice.affineAgreement_translate line 306
  30. theorem OAI.DFVSGames.Inverse.AffineWitness.normalize_of_density line 328
  31. theorem OAI.DFVSGames.Inverse.AffineWitness.first_bit_witness line 362
  32. theorem OAI.DFVSGames.Inverse.card_finset_subtype_eq_filter_card line 394
  33. theorem OAI.DFVSGames.Inverse.finset_expect_indicator_eq_card_ratio line 408
  34. theorem OAI.DFVSGames.Inverse.nat_card_subtype_equiv line 415
  35. theorem OAI.DFVSGames.Inverse.finset_expect_indicator_eq_card_ratio_of_equiv line 420
  36. def OAI.DFVSGames.Inverse.Shortcode.functionalRow line 437
  37. theorem OAI.DFVSGames.Inverse.Shortcode.toMatrix_shift line 440
  38. theorem OAI.DFVSGames.Inverse.Shortcode.Slice.affineAgreement_eq_linear_ratio line 452
  39. theorem OAI.DFVSGames.Inverse.Shortcode.Slice.first_bit_normalization line 469
  40. def OAI.DFVSGames.Decoder.MatrixCoordinates.domainCoordinates line 514
  41. def OAI.DFVSGames.Decoder.MatrixCoordinates.changeDomain line 519
  42. def OAI.DFVSGames.Decoder.MatrixCoordinates.mapEquiv line 529
  43. theorem OAI.DFVSGames.Decoder.MatrixCoordinates.mapEquiv_apply line 534
  44. theorem OAI.DFVSGames.Decoder.MatrixCoordinates.mapEquiv_symm_apply line 539
  45. def OAI.DFVSGames.Decoder.MatrixCoordinates.functionalEquiv line 544
  46. theorem OAI.DFVSGames.Decoder.MatrixCoordinates.functionalEquiv_apply line 548
  47. theorem OAI.DFVSGames.Decoder.MatrixCoordinates.mapEquiv_rankOne line 553
  48. theorem OAI.DFVSGames.Decoder.MatrixCoordinates.mapEquiv_symm_add_rankOne line 559
  49. def OAI.DFVSGames.Decoder.MatrixCoordinates.coordinateTau line 567
  50. theorem OAI.DFVSGames.Decoder.MatrixCoordinates.functionalEquiv_tau line 570
  51. theorem OAI.DFVSGames.Decoder.MatrixCoordinates.mapEquiv_symm_firstBit_shift line 577
  52. theorem OAI.DFVSGames.Decoder.MatrixCoordinates.affine_evaluation line 585
  53. theorem OAI.DFVSGames.Decoder.MatrixCoordinates.mapEquiv_rowAdvice line 595
  54. theorem OAI.DFVSGames.Decoder.MatrixCoordinates.indicator_congr_inline_MatrixCoordinates line 604
  55. theorem OAI.DFVSGames.Decoder.MatrixCoordinates.shortcodeAcceptance_eq line 610
  56. theorem OAI.DFVSGames.Inverse.RowErasure.table_expect_prod line 634
  57. theorem OAI.DFVSGames.Inverse.RowErasure.exp_half_le_seven_quarters_inline_RowErasureConcentration line 643
  58. theorem OAI.DFVSGames.Inverse.RowErasure.exp_half_indicator_inline_RowErasureConcentration line 649
  59. theorem OAI.DFVSGames.Inverse.RowErasure.table_coordinate_exp_le line 654
  60. def OAI.DFVSGames.Inverse.RowErasure.randomizedMatches line 693
  61. theorem OAI.DFVSGames.Inverse.RowErasure.randomizedMatches_eq_masked_sum_inline_RowErasureTail line 697
  62. theorem OAI.DFVSGames.Inverse.RowErasure.randomizedMatches_exp_product_inline_RowErasureTail line 716
  63. theorem OAI.DFVSGames.Inverse.RowErasure.table_randomizedMatches_mgf_eq_inline_RowErasureTail line 724
  64. theorem OAI.DFVSGames.Inverse.RowErasure.table_randomizedMatches_product_le_inline_RowErasureTail line 741
  65. theorem OAI.DFVSGames.Inverse.RowErasure.table_randomizedMatches_mgf_le line 771
  66. theorem OAI.DFVSGames.Inverse.RowErasure.uniformMass_mono line 780
  67. theorem OAI.DFVSGames.Inverse.RowErasure.table_randomizedMatches_tail_le line 789
  68. theorem OAI.DFVSGames.Inverse.RowErasure.SliceFamily.randomizedAgreement_probability_le line 842