OAI/Computability/DirectedFeedback/Games/ActualCanonical.lean

GitHub source file

98 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.DFVSGames.Reduction.ActualCanonical.Record line 16
  2. def OAI.DFVSGames.Reduction.ActualCanonical.recordEquiv line 22
  3. instance OAI.DFVSGames.Reduction.ActualCanonical.(instance at line 34) line 34
  4. abbrev OAI.DFVSGames.Reduction.ActualCanonical.Data line 37
  5. def OAI.DFVSGames.Reduction.ActualCanonical.pivot line 40
  6. def OAI.DFVSGames.Reduction.ActualCanonical.translate line 43
  7. def OAI.DFVSGames.Reduction.ActualCanonical.normalize line 44
  8. def OAI.DFVSGames.Reduction.ActualCanonical.record line 46
  9. def OAI.DFVSGames.Reduction.ActualCanonical.data line 54
  10. def OAI.DFVSGames.Reduction.ActualCanonical.standardTriple line 58
  11. def OAI.DFVSGames.Reduction.ActualCanonical.canonical line 61
  12. def OAI.DFVSGames.Reduction.ActualCanonical.ambientEval line 65
  13. def OAI.DFVSGames.Reduction.ActualCanonical.Represents line 69
  14. theorem OAI.DFVSGames.Reduction.ActualCanonical.add_self line 73
  15. theorem OAI.DFVSGames.Reduction.ActualCanonical.add_both line 79
  16. theorem OAI.DFVSGames.Reduction.ActualCanonical.pivot_translate line 85
  17. theorem OAI.DFVSGames.Reduction.ActualCanonical.normalize_translate line 91
  18. theorem OAI.DFVSGames.Reduction.ActualCanonical.record_translate line 98
  19. theorem OAI.DFVSGames.Reduction.ActualCanonical.data_gauge line 104
  20. theorem OAI.DFVSGames.Reduction.ActualCanonical.data_global_shift line 114
  21. theorem OAI.DFVSGames.Reduction.ActualCanonical.canonical_shift line 122
  22. theorem OAI.DFVSGames.Reduction.ActualCanonical.ambientEval_hBasis line 136
  23. theorem OAI.DFVSGames.Reduction.ActualCanonical.ambientEval_firstBasis line 141
  24. theorem OAI.DFVSGames.Reduction.ActualCanonical.ambientEval_secondBasis line 153
  25. theorem OAI.DFVSGames.Reduction.ActualCanonical.standard_represents line 166
  26. theorem OAI.DFVSGames.Reduction.ActualCanonical.extension_coefficients line 173
  27. theorem OAI.DFVSGames.Reduction.ActualCanonical.canonical_eq_of_extension line 184
  28. theorem OAI.DFVSGames.Reduction.ActualCanonical.extension_independent line 199
  29. def OAI.DFVSGames.Reduction.ActualCanonical.singletonTriple line 207
  30. theorem OAI.DFVSGames.Reduction.ActualCanonical.pivot_singleton line 210
  31. theorem OAI.DFVSGames.Reduction.ActualCanonical.record_singleton line 215
  32. theorem OAI.DFVSGames.Reduction.ActualCanonical.singleton_global_adjustment line 222
  33. theorem OAI.DFVSGames.Reduction.ActualCanonical.singleton_locality line 227
  34. def OAI.DFVSGames.Soundness.ActualCanonicalPullback.selectedFree line 247
  35. def OAI.DFVSGames.Soundness.ActualCanonicalPullback.ambientCoefficients line 254
  36. def OAI.DFVSGames.Soundness.ActualCanonicalPullback.freePullback line 261
  37. theorem OAI.DFVSGames.Soundness.ActualCanonicalPullback.ofBit_and line 267
  38. theorem OAI.DFVSGames.Soundness.ActualCanonicalPullback.inverse_homogeneous line 270
  39. theorem OAI.DFVSGames.Soundness.ActualCanonicalPullback.inverse_first line 274
  40. theorem OAI.DFVSGames.Soundness.ActualCanonicalPullback.inverse_second line 278
  41. theorem OAI.DFVSGames.Soundness.ActualCanonicalPullback.inverse_retained_free line 282
  42. theorem OAI.DFVSGames.Soundness.ActualCanonicalPullback.freePullback_expansion line 296
  43. def OAI.DFVSGames.Soundness.ActualCanonicalPullback.outsideInsideEquiv line 310
  44. theorem OAI.DFVSGames.Soundness.ActualCanonicalPullback.sum_outside_inside line 321
  45. theorem OAI.DFVSGames.Soundness.ActualCanonicalPullback.raw_represents line 332
  46. theorem OAI.DFVSGames.Soundness.ActualCanonicalPullback.canonical_raw_pullback line 360
  47. theorem OAI.DFVSGames.Soundness.ActualCanonicalPullback.ambientCoefficients_single line 370
  48. theorem OAI.DFVSGames.Soundness.ActualCanonicalPullback.ambientCoefficients_full_eq line 379
  49. theorem OAI.DFVSGames.Soundness.ActualCanonicalPullback.raw_data_locality line 385
  50. theorem OAI.DFVSGames.Soundness.ActualCanonicalPullback.canonical_private_input_locality line 413
  51. abbrev OAI.DFVSGames.Soundness.RawPartnerTarget.RawPoint line 440
  52. def OAI.DFVSGames.Soundness.RawPartnerTarget.rawProjection line 444
  53. def OAI.DFVSGames.Soundness.RawPartnerTarget.gammaOfRawMap line 450
  54. theorem OAI.DFVSGames.Soundness.RawPartnerTarget.rawPoint_decomposition line 453
  55. theorem OAI.DFVSGames.Soundness.RawPartnerTarget.rawMap_expansion line 458
  56. theorem OAI.DFVSGames.Soundness.RawPartnerTarget.rawMap_on_partner line 465
  57. theorem OAI.DFVSGames.Soundness.RawPartnerTarget.rawMap_pullback line 471
  58. instance OAI.DFVSGames.Soundness.ConditionalIncidences.zeroBits line 492
  59. def OAI.DFVSGames.Soundness.ConditionalIncidences.membershipBool line 495
  60. def OAI.DFVSGames.Soundness.ConditionalIncidences.fullCoefficient line 498
  61. def OAI.DFVSGames.Soundness.ConditionalIncidences.singleCoefficient line 503
  62. def OAI.DFVSGames.Soundness.ConditionalIncidences.fillHidden line 507
  63. theorem OAI.DFVSGames.Soundness.ConditionalIncidences.singleCoefficient_zero line 511
  64. theorem OAI.DFVSGames.Soundness.ConditionalIncidences.zeroSet_subset line 519
  65. def OAI.DFVSGames.Soundness.ConditionalIncidences.actualFirst line 529
  66. def OAI.DFVSGames.Soundness.ConditionalIncidences.actualSecond line 534
  67. def OAI.DFVSGames.Soundness.ConditionalIncidences.localFirstFromH line 539
  68. def OAI.DFVSGames.Soundness.ConditionalIncidences.localSecondFromH line 550
  69. theorem OAI.DFVSGames.Soundness.ConditionalIncidences.localFirstFromH_question_inside line 562
  70. theorem OAI.DFVSGames.Soundness.ConditionalIncidences.localSecondFromH_question_inside line 572
  71. theorem OAI.DFVSGames.Soundness.ConditionalIncidences.outside_pair_agree line 584
  72. theorem OAI.DFVSGames.Soundness.ConditionalIncidences.fillHidden_occurrences line 590
  73. theorem OAI.DFVSGames.Soundness.ConditionalIncidences.fillHidden_names line 602
  74. theorem OAI.DFVSGames.Soundness.ConditionalIncidences.localFirstFromH_correct line 613
  75. theorem OAI.DFVSGames.Soundness.ConditionalIncidences.localSecondFromH_correct line 634
  76. def OAI.DFVSGames.Soundness.BinaryRowTransport.rowBits line 664
  77. theorem OAI.DFVSGames.Soundness.BinaryRowTransport.rowBits_zero line 666
  78. theorem OAI.DFVSGames.Soundness.BinaryRowTransport.rowBits_add line 671
  79. theorem OAI.DFVSGames.Soundness.BinaryRowTransport.rowBits_smul line 675
  80. theorem OAI.DFVSGames.Soundness.BinaryRowTransport.rowBits_list_sum line 679
  81. theorem OAI.DFVSGames.Soundness.BinaryRowTransport.rowBits_sum line 686
  82. def OAI.DFVSGames.Soundness.BinaryRowTransport.rowBitsEquiv line 691
  83. theorem OAI.DFVSGames.Soundness.BinaryRowTransport.rowBits_eq_zero line 697
  84. def OAI.DFVSGames.Soundness.BinaryRowTransport.rowCoefficients line 706
  85. theorem OAI.DFVSGames.Soundness.BinaryRowTransport.zeroSet_rowCoefficients line 709
  86. theorem OAI.DFVSGames.Soundness.BinaryRowTransport.actual_pullbackRow line 720
  87. theorem OAI.DFVSGames.Soundness.BinaryRowTransport.actual_partnerRow line 752
  88. def OAI.DFVSGames.Soundness.BinaryRowTransport.rawBitsEquiv line 781
  89. def OAI.DFVSGames.Soundness.BinaryRowTransport.bitsMapEquiv line 785
  90. theorem OAI.DFVSGames.Soundness.BinaryRowTransport.uniform_bit_coefficients_maps line 791
  91. def OAI.DFVSGames.Soundness.RawMapLaw.rawMap line 811
  92. theorem OAI.DFVSGames.Soundness.RawMapLaw.coefficients_rawMap line 815
  93. theorem OAI.DFVSGames.Soundness.RawMapLaw.rawMap_coefficients line 826
  94. def OAI.DFVSGames.Soundness.RawMapLaw.rawMapEquiv line 835
  95. instance OAI.DFVSGames.Soundness.RawMapLaw.rawMapsFintype line 841
  96. def OAI.DFVSGames.Soundness.RawMapLaw.bitsRawMapEquiv line 845
  97. theorem OAI.DFVSGames.Soundness.RawMapLaw.bits_coefficients line 849
  98. theorem OAI.DFVSGames.Soundness.RawMapLaw.uniform_bits_rawMaps line 854