OAI/LinearAlgebra/MatrixFields/Construction/InitialFamily.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialGibbs.coordinateWeight line 19
  2. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialGibbs.orderedWeight line 22
  3. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialGibbs.initialNormalizer line 25
  4. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialGibbs.initialPotential line 27
  5. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialGibbs.initialLogNormalizer line 29
  6. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialGibbs.coordinateWeight_pos line 31
  7. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialGibbs.orderedWeight_pos line 36
  8. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialGibbs.initialNormalizer_pos line 39
  9. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialGibbs.orderedWeight_source line 44
  10. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialGibbs.initialWeight_source line 51
  11. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialGibbs.placedInitialLaw_mass line 60
  12. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialGibbs.orderedInitialLaw_mass line 68
  13. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialGibbs.orderedInitialLaw_zero line 90
  14. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialGibbs.orderedInitialLaw_mass_eq line 103
  15. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialGibbs.orderedInitialLaw_positive line 111
  16. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialGibbs.orderedInitialLaw_support line 117
  17. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialGibbs.log_orderedWeight line 124
  18. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialGibbs.orderedInitialLaw_log line 133
  19. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialFamily.grid line 156
  20. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialFamily.grid_pos line 158
  21. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialFamily.populationLength_eq_mul_grid line 161
  22. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialFamily.initialJointCounts_dilation_ratio line 165
  23. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialFamily.initialJointCounts_dilation_rate line 173
  24. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialFamily.native_dilation_capacity line 181
  25. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialFamily.hashRate line 191
  26. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialFamily.selection_exponent line 195
  27. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialFamily.Sample line 205
  28. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialFamily.Good line 210
  29. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialFamily.executionWithWidth line 219
  30. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialFamily.executionWithWidth_copies line 236
  31. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialFamily.execution line 244
  32. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialFamily.execution_copies line 254
  33. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialFamily.eventually_exists_execution_with_width line 260
  34. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialFamily.eventually_exists_execution line 294