OAI/LinearAlgebra/MatrixMultiplication/Entropy/ComplexSeparationAsymptotics.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

Finite entropy, rate estimates and ordered asymptotic limits.

  1. theorem OAI.MatrixMultiplication.Foundation.Separation.scale_exists line 23
  2. def OAI.MatrixMultiplication.Foundation.Separation.gridScale line 28
  3. theorem OAI.MatrixMultiplication.Foundation.Separation.population_le_scale line 30
  4. theorem OAI.MatrixMultiplication.Foundation.Separation.previous_scale_lt_population line 33
  5. theorem OAI.MatrixMultiplication.Foundation.Separation.scale_pos line 37
  6. theorem OAI.MatrixMultiplication.Foundation.Separation.scale_gt_of_population_gt line 44
  7. theorem OAI.MatrixMultiplication.Foundation.Separation.gridScale_monotone line 52
  8. def OAI.MatrixMultiplication.Foundation.Separation.gridDimension line 56
  9. def OAI.MatrixMultiplication.Foundation.Separation.gridWidth line 58
  10. def OAI.MatrixMultiplication.Foundation.Separation.gridGroupOrder line 60
  11. theorem OAI.MatrixMultiplication.Foundation.Separation.gridDimension_pos line 62
  12. theorem OAI.MatrixMultiplication.Foundation.Separation.gridWidth_ge_two line 65
  13. theorem OAI.MatrixMultiplication.Foundation.Separation.dimension_le_power line 69
  14. theorem OAI.MatrixMultiplication.Foundation.Separation.grid_population_bound line 78
  15. theorem OAI.MatrixMultiplication.Foundation.Separation.gridGroupOrder_eq line 104
  16. theorem OAI.MatrixMultiplication.Foundation.Separation.gridGroupOrder_pos line 114
  17. theorem OAI.MatrixMultiplication.Foundation.Separation.population_le_gridGroupOrder line 118
  18. theorem OAI.MatrixMultiplication.Foundation.Separation.gridGroupOrder_monotone line 124
  19. theorem OAI.MatrixMultiplication.Foundation.Separation.asymptotic_grid_tags_slices line 130
  20. theorem OAI.MatrixMultiplication.Foundation.Separation.log_gridGroupOrder line 139
  21. theorem OAI.MatrixMultiplication.Foundation.Separation.log_population_le_log_gridGroupOrder line 144
  22. theorem OAI.MatrixMultiplication.Foundation.Separation.previous_scale_log_lt line 149
  23. theorem OAI.MatrixMultiplication.Foundation.Separation.log_gridGroupOrder_le_of_scale line 158
  24. theorem OAI.MatrixMultiplication.Foundation.Separation.scale_error_bound line 175
  25. theorem OAI.MatrixMultiplication.Foundation.Separation.eventually_log_gridGroupOrder_le line 182
  26. theorem OAI.MatrixMultiplication.Foundation.Separation.uniform_log_gridGroupOrder_le line 203
  27. theorem OAI.MatrixMultiplication.Foundation.Separation.tendsto_log_gridGroupOrder_div_log_population line 223
  28. theorem OAI.MatrixMultiplication.Foundation.Separation.tendsto_log_gridGroupOrder_div_nat line 245
  29. theorem OAI.MatrixMultiplication.Foundation.Separation.log_nat_prod line 279
  30. theorem OAI.MatrixMultiplication.Foundation.Separation.tendsto_log_nat_prod_div_nat line 286
  31. theorem OAI.MatrixMultiplication.Foundation.Separation.tendsto_log_gridGroupOrder_prod_div_nat line 299
  32. theorem OAI.MatrixMultiplication.Foundation.Separation.tendsto_log_nat_weighted_prod_div_nat line 309
  33. theorem OAI.MatrixMultiplication.Foundation.Separation.tendsto_log_gridGroupOrder_weighted_prod_div_nat line 323