OAI/LinearAlgebra/MatrixFields/Construction/InitialState.lean

GitHub source file

120 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.rectangularAdmissibleExponent_of_rankAtMost line 25
  2. theorem OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.rectangular_rpow_omega_le_of_rankAtMost line 43
  3. theorem OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.rectangular_rpow_omega_le_of_rank_growth line 65
  4. theorem OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.equalRectangular_inequality line 106
  5. theorem OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.power_le_of_forall_pow_le_square_linear_mul_pow line 146
  6. theorem OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.equalRectangular_inequality_of_polynomialApproximation line 158
  7. theorem OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.equalRectangular_log_inequality_of_polynomialApproximation line 177
  8. theorem OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.equalSquare_inequality_of_polynomialApproximation line 194
  9. theorem OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.equalVolume_inequality_of_polynomialApproximation line 217
  10. structure OAI.MatrixAllFields.MatrixMultiplication.AllFieldWitness line 254
  11. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldWitness.volume line 276
  12. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldWitness.volume_pos line 278
  13. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldWitness.finite_inequality line 281
  14. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldWitness.log_inequality line 286
  15. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldSource.Word line 317
  16. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldSource.Index line 319
  17. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldSource.tensor line 321
  18. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldSource.rankBudget line 325
  19. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldSource.rank_bound line 328
  20. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldSource.rankBudget_pos line 338
  21. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldSource.rankBudget_prod line 344
  22. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldSource.matrixTarget line 349
  23. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldSource.restricted_rank_bound line 358
  24. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldSource.restrictedApproximation line 370
  25. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldSource.ofRestriction line 379
  26. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldSource.ofRestriction_polynomial line 401
  27. structure OAI.MatrixAllFields.MatrixMultiplication.AllFieldFiniteFamily.LocalMap line 435
  28. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldFiniteFamily.LocalMap.identity line 451
  29. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldFiniteFamily.LocalMap.delete line 459
  30. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldFiniteFamily.LocalMap.product line 469
  31. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldFiniteFamily.LocalMap.comp line 480
  32. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldFiniteFamily.LocalMap.withSource line 488
  33. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldFiniteFamily.LocalMap.ofExists line 495
  34. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldFiniteFamily.LocalMap.parallelCopies line 501
  35. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldFiniteFamily.LocalMap.directSum line 512
  36. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldFiniteFamily.LocalMap.selectBranches line 524
  37. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldFiniteFamily.LocalMap.unflatten line 535
  38. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldFiniteFamily.LocalMap.flatten line 547
  39. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldFiniteFamily.LocalMap.replicationProduct line 559
  40. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldFiniteFamily.LocalMap.extract line 572
  41. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldFiniteFamily.LocalMap.repairBranches line 581
  42. structure OAI.MatrixAllFields.MatrixMultiplication.AllFieldFiniteFamily.Execution line 592
  43. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldFiniteFamily.Execution.initial line 609
  44. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldFiniteFamily.Execution.restrict line 622
  45. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldFiniteFamily.Execution.replicate line 628
  46. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldFiniteFamily.Execution.step line 636
  47. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldFiniteFamily.Execution.stepOnLeft line 642
  48. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldFiniteFamily.Execution.branchOperation line 652
  49. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldFiniteFamily.Execution.branchOperation_copies line 666
  50. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldFiniteFamily.Execution.step_copies line 678
  51. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldFiniteFamily.Execution.extractAndRepair line 685
  52. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldFiniteFamily.Execution.extractAndRepair_copies line 701
  53. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldFiniteFamily.Execution.extractSelectedAndRepair line 713
  54. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldFiniteFamily.Execution.extractSelectedAndRepair_copies line 734
  55. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldFiniteFamily.run line 760
  56. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldFiniteFamily.run_copies line 764
  57. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldFiniteFamily.cwSource line 782
  58. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldFiniteFamily.startCW line 785
  59. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldFiniteFamily.Execution.toWitness line 789
  60. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldFiniteFamily.Execution.toWitness_rankBound line 796
  61. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialSource.Sites line 823
  62. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialSource.Words line 824
  63. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialSource.sitesEquiv line 826
  64. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialSource.flatten line 829
  65. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialSource.groupedSource line 832
  66. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialSource.groupedSource_eq_lots line 837
  67. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialSource.groupingMap line 843
  68. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialSource.initialExecution line 856
  69. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialSource.initialExecution_copies line 860
  70. abbrev OAI.MatrixAllFields.MatrixMultiplication.JointCanonicalInitial.Word line 888
  71. abbrev OAI.MatrixAllFields.MatrixMultiplication.JointCanonicalInitial.RawWords line 889
  72. abbrev OAI.MatrixAllFields.MatrixMultiplication.JointCanonicalInitial.CanonicalWords line 890
  73. def OAI.MatrixAllFields.MatrixMultiplication.JointCanonicalInitial.wholeEquiv line 892
  74. def OAI.MatrixAllFields.MatrixMultiplication.JointCanonicalInitial.rawSource line 904
  75. def OAI.MatrixAllFields.MatrixMultiplication.JointCanonicalInitial.coarseWord line 907
  76. def OAI.MatrixAllFields.MatrixMultiplication.JointCanonicalInitial.ideal line 910
  77. def OAI.MatrixAllFields.MatrixMultiplication.JointCanonicalInitial.canonical line 916
  78. theorem OAI.MatrixAllFields.MatrixMultiplication.JointCanonicalInitial.canonical_pack line 921
  79. theorem OAI.MatrixAllFields.MatrixMultiplication.JointCanonicalInitial.ideal_eq_canonical line 936
  80. def OAI.MatrixAllFields.MatrixMultiplication.JointCanonicalInitial.coordinateMatrix line 946
  81. theorem OAI.MatrixAllFields.MatrixMultiplication.JointCanonicalInitial.ideal_restrict line 949
  82. theorem OAI.MatrixAllFields.MatrixMultiplication.JointCanonicalInitial.coarse_support line 960
  83. def OAI.MatrixAllFields.MatrixMultiplication.JointCanonicalInitial.sideMask line 974
  84. def OAI.MatrixAllFields.MatrixMultiplication.JointCanonicalInitial.maskedSource line 978
  85. theorem OAI.MatrixAllFields.MatrixMultiplication.JointCanonicalInitial.sideMask_of_target line 983
  86. theorem OAI.MatrixAllFields.MatrixMultiplication.JointCanonicalInitial.maskedSource_support line 991
  87. theorem OAI.MatrixAllFields.MatrixMultiplication.JointCanonicalInitial.ideal_support_masks line 1011
  88. theorem OAI.MatrixAllFields.MatrixMultiplication.JointCanonicalInitial.delete_ideal_eq line 1029
  89. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialStep.toLots line 1061
  90. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialStep.positionMap line 1064
  91. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialStep.initialExecution line 1084
  92. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialStep.initialExecution_copies line 1088
  93. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialStep.maskedInitialExecution line 1091
  94. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialStep.CoarseWord line 1098
  95. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialStep.ordinaryAssignments line 1100
  96. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialStep.ordinaryAssignments_coherent line 1109
  97. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialStep.initialCanonicalMap line 1119
  98. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialStep.canonicalize line 1127
  99. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialStep.canonicalize_copies line 1134
  100. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialStep.repairedInitialExecution line 1139
  101. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialStep.repairedInitialExecution_copies line 1154
  102. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialExact.assignedDeletion line 1190
  103. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialExact.assignedDeletion_eq_self_of_support line 1196
  104. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialExact.Isolated line 1213
  105. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialExact.assignments_on_ideal line 1222
  106. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialExact.branch_eq_masked_ideal line 1257
  107. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialExact.branch_eq_ideal line 1272
  108. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialExact.selectedExecution line 1296
  109. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialExact.selectedExecution_copies line 1330
  110. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialState.CanonicalKey line 1361
  111. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialState.PlacementPositions line 1363
  112. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialState.classPosition line 1366
  113. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialState.classPosition_shape line 1372
  114. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialState.prod_classPosition line 1381
  115. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialState.StateWords line 1416
  116. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialState.toCanonical line 1418
  117. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialState.coefficient line 1424
  118. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialState.map line 1462
  119. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialState.execution line 1474
  120. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialState.execution_copies line 1482