OAI/LinearAlgebra/MatrixFields/Construction/ExactStatisticWords.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatrixAllFields.MatrixMultiplication.LeafVolumes.zeroXMatching line 19
  2. def OAI.MatrixAllFields.MatrixMultiplication.LeafVolumes.zeroYMatching line 20
  3. def OAI.MatrixAllFields.MatrixMultiplication.LeafVolumes.zeroZMatching line 21
  4. theorem OAI.MatrixAllFields.MatrixMultiplication.LeafVolumes.zeroXMatching_matrixCoefficients line 23
  5. theorem OAI.MatrixAllFields.MatrixMultiplication.LeafVolumes.zeroYMatching_matrixCoefficients line 31
  6. theorem OAI.MatrixAllFields.MatrixMultiplication.LeafVolumes.zeroZMatching_matrixCoefficients line 39
  7. def OAI.MatrixAllFields.MatrixMultiplication.LeafVolumes.complementaryMatching line 47
  8. theorem OAI.MatrixAllFields.MatrixMultiplication.LeafVolumes.complementaryMatching_pullback line 50
  9. theorem OAI.MatrixAllFields.MatrixMultiplication.LeafVolumes.zeroXMatching_subtype line 56
  10. theorem OAI.MatrixAllFields.MatrixMultiplication.LeafVolumes.matchingPower_leaf line 63
  11. theorem OAI.MatrixAllFields.MatrixMultiplication.LeafVolumes.matchingPower_matrixCoefficients line 75
  12. theorem OAI.MatrixAllFields.MatrixMultiplication.LeafVolumes.rankAtMost_matchingPower_leaf line 91
  13. abbrev OAI.MatrixAllFields.MatrixMultiplication.LeafVolumes.LabeledExactWords line 104
  14. theorem OAI.MatrixAllFields.MatrixMultiplication.LeafVolumes.labelings_card line 107
  15. theorem OAI.MatrixAllFields.MatrixMultiplication.LeafVolumes.labeledExactWords_card line 122
  16. theorem OAI.MatrixAllFields.MatrixMultiplication.LeafVolumes.labeledExactWords_card_pos line 136
  17. structure OAI.MatrixAllFields.MatrixMultiplication.LeafVolumes.Dimensions line 150
  18. def OAI.MatrixAllFields.MatrixMultiplication.LeafVolumes.Dimensions.volume line 156
  19. def OAI.MatrixAllFields.MatrixMultiplication.LeafVolumes.Dimensions.product line 158
  20. theorem OAI.MatrixAllFields.MatrixMultiplication.LeafVolumes.Dimensions.volume_product line 161
  21. def OAI.MatrixAllFields.MatrixMultiplication.LeafVolumes.historyDimensions line 166
  22. theorem OAI.MatrixAllFields.MatrixMultiplication.LeafVolumes.historyDimensions_volume line 169
  23. abbrev OAI.MatrixAllFields.MatrixMultiplication.ExactStatisticWords.Words line 188
  24. def OAI.MatrixAllFields.MatrixMultiplication.ExactStatisticWords.statisticWord line 192
  25. theorem OAI.MatrixAllFields.MatrixMultiplication.ExactStatisticWords.empiricalLaw_eq line 197
  26. theorem OAI.MatrixAllFields.MatrixMultiplication.ExactStatisticWords.typeWindow_of_counts line 205
  27. theorem OAI.MatrixAllFields.MatrixMultiplication.ExactStatisticWords.sum_statistic_weight line 214
  28. def OAI.MatrixAllFields.MatrixMultiplication.ExactStatisticWords.fiberEquiv line 233
  29. theorem OAI.MatrixAllFields.MatrixMultiplication.ExactStatisticWords.card line 252
  30. theorem OAI.MatrixAllFields.MatrixMultiplication.ExactStatisticWords.card_of_supported line 281
  31. theorem OAI.MatrixAllFields.MatrixMultiplication.ExactStatisticWords.card_fixedWeight_fiber line 295
  32. theorem OAI.MatrixAllFields.MatrixMultiplication.ExactStatisticWords.card_pos_of_supported line 308