OAI/LinearAlgebra/MatrixFields/Histories/HistoryRecoveryBudget.lean

GitHub source file

104 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.wordPairLeftPositions line 25
  2. def OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.wordPairRightPositions line 29
  3. def OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.wordPairCount line 33
  4. theorem OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.wordPairCount_smul line 40
  5. theorem OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.average_wordPairCount_shift line 52
  6. def OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.wordPairMaskBad line 64
  7. theorem OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.wordPair_orbit_fraction_eq line 69
  8. theorem OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.wordPair_orbit_rejection_le line 83
  9. theorem OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.wordPair_orbit_rejection_of_windows_le line 97
  10. def OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.selectedWordPairCount line 116
  11. theorem OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.selectedWordPairCount_smul line 123
  12. theorem OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.average_selectedWordPairCount_shift line 136
  13. def OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.selectedWordPairMaskBad line 150
  14. theorem OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.selectedWordPair_orbit_fraction_eq line 157
  15. theorem OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.selectedWordPair_orbit_rejection_le line 172
  16. theorem OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.selectedWordPair_orbit_rejection_of_windows_le line 189
  17. theorem OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.selectedWordPair_orbit_rejection_of_completeWindows_le line 210
  18. theorem OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.finite_selectedWordPair_sum_orbit_fraction_le line 246
  19. theorem OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.finite_selectedWordPair_orbit_rejection_of_windows_le line 295
  20. theorem OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.finite_selectedWordPair_orbit_inverse_linear_of_windows line 330
  21. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryMasks.Classes line 381
  22. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryMasks.Positions line 383
  23. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryMasks.Letters line 386
  24. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryMasks.Words line 388
  25. instance OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryMasks.permutationsFintype line 391
  26. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryMasks.SymbolChoice line 405
  27. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryMasks.MaskIndex line 407
  28. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryMasks.testedClasses line 409
  29. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryMasks.pairWidth line 412
  30. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryMasks.childWidth line 414
  31. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryMasks.pairWidth_pos line 416
  32. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryMasks.childWidth_pos line 421
  33. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryMasks.classStatistic line 424
  34. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryMasks.leftSymbol line 426
  35. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryMasks.rightSymbol line 428
  36. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryMasks.leftProbability line 430
  37. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryMasks.rightProbability line 433
  38. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryMasks.center line 436
  39. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryMasks.passes line 440
  40. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryMasks.childWindows line 446
  41. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryMasks.lossConstant line 454
  42. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryMasks.lossConstant_nonneg line 459
  43. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryMaskLaws.parentCenter line 485
  44. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryMaskLaws.center_eq_parentCenter line 492
  45. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryMaskLaws.stageBActive line 522
  46. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryMaskLaws.stageB_leftLaw_branch line 526
  47. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryMaskLaws.stageB_rightLaw_branch line 537
  48. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryMaskLaws.stageB_sum_laws line 550
  49. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryMaskLaws.parentCenter_stageB line 566
  50. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryMaskLaws.center_stageB line 604
  51. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryRawMasks.rawPairCount line 629
  52. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryRawMasks.rawPass line 635
  53. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryRawMasks.sum_positiveClasses line 642
  54. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryRawMasks.selectedWordPairCount_pairEquiv line 675
  55. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryRawMasks.testedClasses_populationSize line 697
  56. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryRawMasks.raw_population_pos line 705
  57. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryRawMasks.passes_pairEquiv_iff_rawPass line 710
  58. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryRawMasks.passes_pairEquiv_target_independent line 721
  59. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryIncomingMasks.empiricalLaw_congr_decidable line 751
  60. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryIncomingMasks.typeWindow_mono_decidable line 757
  61. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryIncomingMasks.weight_append line 765
  62. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryIncomingMasks.strand_append line 769
  63. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryIncomingMasks.shapeTensor_append line 776
  64. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryIncomingMasks.shapeTensor_joinHalves line 785
  65. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryIncomingMasks.defaultStatistic line 793
  66. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryIncomingMasks.choiceAt line 798
  67. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryIncomingMasks.choiceAt_self line 801
  68. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryIncomingMasks.rawPairCount_eq_wordPopulation line 804
  69. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryIncomingMasks.fourStatistic_append line 812
  70. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryIncomingMasks.append_singletons line 816
  71. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryIncomingMasks.rawPass_stageB_typeWindow line 823
  72. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryIncomingMasks.incoming_stageA line 863
  73. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryIncomingMasks.incoming_stageB line 871
  74. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryIncomingMasks.incoming_stageC line 892
  75. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryIncomingMasks.stageCWeights line 932
  76. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryIncomingMasks.received_of_rawPass line 943
  77. def OAI.MatrixAllFields.MatrixMultiplication.EquivOrbitTransport.action line 970
  78. theorem OAI.MatrixAllFields.MatrixMultiplication.EquivOrbitTransport.equiv_smul line 979
  79. theorem OAI.MatrixAllFields.MatrixMultiplication.EquivOrbitTransport.orbitSet_map line 988
  80. theorem OAI.MatrixAllFields.MatrixMultiplication.EquivOrbitTransport.orbitSet_card line 997
  81. theorem OAI.MatrixAllFields.MatrixMultiplication.EquivOrbitTransport.rejected_card line 1004
  82. theorem OAI.MatrixAllFields.MatrixMultiplication.EquivOrbitTransport.rejected_fraction line 1015
  83. theorem OAI.MatrixAllFields.MatrixMultiplication.EquivOrbitTransport.coefficients_preserved line 1026
  84. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryRecovery.halfLength_le_eight line 1068
  85. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryRecovery.Raw line 1072
  86. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryRecovery.Targets line 1075
  87. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryRecovery.Symmetries line 1078
  88. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryRecovery.childStatistic line 1082
  89. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryRecovery.leftPrescription line 1085
  90. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryRecovery.rightPrescription line 1088
  91. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryRecovery.outputWidth line 1091
  92. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryRecovery.parents line 1094
  93. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryRecovery.rawSource line 1098
  94. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryRecovery.ideal line 1104
  95. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryRecovery.coordinates line 1113
  96. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryRecovery.canonical line 1118
  97. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryRecovery.rawAction line 1127
  98. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryRecovery.completeKeep line 1132
  99. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryRecovery.sideVariable line 1139
  100. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryRecovery.idealSide line 1141
  101. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryRecovery.minimumDilation line 1164
  102. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryRecovery.minimumDilation_spec line 1167
  103. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryRecovery.shiftCount line 1181
  104. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryRecovery.replication_subexponential line 1185