OAI/LinearAlgebra/MatrixMultiplication/FieldConstruction/ActiveLaws.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

Tensor extraction over arbitrary fields and its asymptotic rate.

  1. def OAI.MatrixMultiplication.AllFieldActiveLaws.branchProbability line 18
  2. theorem OAI.MatrixMultiplication.AllFieldActiveLaws.branchProbability_nonneg line 24
  3. theorem OAI.MatrixMultiplication.AllFieldActiveLaws.branchProbability_total line 31
  4. def OAI.MatrixMultiplication.AllFieldActiveLaws.branchLaw line 46
  5. theorem OAI.MatrixMultiplication.AllFieldActiveLaws.branchLaw_mass line 51
  6. def OAI.MatrixMultiplication.AllFieldActiveLaws.placedLaw line 54
  7. theorem OAI.MatrixMultiplication.AllFieldActiveLaws.placedLaw_mass line 57
  8. theorem OAI.MatrixMultiplication.AllFieldActiveLaws.placedLaw_mass_branch line 64
  9. theorem OAI.MatrixMultiplication.AllFieldActiveLaws.placedLaw_entropy line 68
  10. theorem OAI.MatrixMultiplication.AllFieldActiveLaws.placedLaw_sideMass line 72
  11. theorem OAI.MatrixMultiplication.AllFieldActiveLaws.branchPopulation_cast_rat line 89
  12. theorem OAI.MatrixMultiplication.AllFieldActiveLaws.branchPopulation_cast line 99
  13. theorem OAI.MatrixMultiplication.AllFieldActiveLaws.jointCounts_cast line 107
  14. theorem OAI.MatrixMultiplication.AllFieldActiveLaws.jointCounts_ratio line 119
  15. theorem OAI.MatrixMultiplication.AllFieldActiveLaws.jointCounts_normalized line 128
  16. theorem OAI.MatrixMultiplication.AllFieldActiveLaws.population_cast_real line 135
  17. theorem OAI.MatrixMultiplication.AllFieldActiveLaws.jointCounts_source_cast line 141
  18. theorem OAI.MatrixMultiplication.AllFieldActiveLaws.jointCounts_source_ratio line 148
  19. theorem OAI.MatrixMultiplication.AllFieldActiveLaws.jointCounts_source_rate line 159
  20. theorem OAI.MatrixMultiplication.AllFieldActiveLaws.populationLength_dilation line 168
  21. theorem OAI.MatrixMultiplication.AllFieldActiveLaws.jointCounts_dilation_ratio line 173
  22. theorem OAI.MatrixMultiplication.AllFieldActiveLaws.jointCounts_dilation_rate line 182
  23. def OAI.MatrixMultiplication.AllFieldActiveLaws.orderLaw line 192
  24. def OAI.MatrixMultiplication.AllFieldActiveLaws.orderMass line 195
  25. def OAI.MatrixMultiplication.AllFieldActiveLaws.orderCounts line 199
  26. theorem OAI.MatrixMultiplication.AllFieldActiveLaws.orderMass_nonneg line 203
  27. theorem OAI.MatrixMultiplication.AllFieldActiveLaws.orderCounts_source_cast line 208
  28. theorem OAI.MatrixMultiplication.AllFieldActiveLaws.orderCounts_source_rate line 216
  29. theorem OAI.MatrixMultiplication.AllFieldActiveLaws.orderCounts_dilation_rate line 223