OAI/LinearAlgebra/MatrixMultiplication/Entropy/CurveLaws.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

Finite entropy, rate estimates and ordered asymptotic limits.

  1. theorem OAI.MatrixMultiplication.CurveLaws.fiberSize_real_pos line 16
  2. def OAI.MatrixMultiplication.CurveLaws.uniformLift line 19
  3. theorem OAI.MatrixMultiplication.CurveLaws.uniformLift_marginal line 26
  4. theorem OAI.MatrixMultiplication.CurveLaws.entropyTerm_div_fiber line 39
  5. theorem OAI.MatrixMultiplication.CurveLaws.uniformLift_entropy line 47
  6. def OAI.MatrixMultiplication.CurveLaws.partition line 58
  7. theorem OAI.MatrixMultiplication.CurveLaws.partition_pos line 61
  8. theorem OAI.MatrixMultiplication.CurveLaws.partition_closed line 67
  9. def OAI.MatrixMultiplication.CurveLaws.marginal line 72
  10. theorem OAI.MatrixMultiplication.CurveLaws.marginal_pos line 80
  11. theorem OAI.MatrixMultiplication.CurveLaws.marginal_lt_one line 83
  12. def OAI.MatrixMultiplication.CurveLaws.leafLaw line 92
  13. theorem OAI.MatrixMultiplication.CurveLaws.leafLaw_pos line 94
  14. theorem OAI.MatrixMultiplication.CurveLaws.marginal_of_leafLaw line 97
  15. theorem OAI.MatrixMultiplication.CurveLaws.leafLaw_uniform_in_fibers line 102
  16. def OAI.MatrixMultiplication.CurveLaws.hidden line 108
  17. def OAI.MatrixMultiplication.CurveLaws.incident line 111
  18. theorem OAI.MatrixMultiplication.CurveLaws.log_marginal line 113
  19. theorem OAI.MatrixMultiplication.CurveLaws.incident_entropy line 120
  20. theorem OAI.MatrixMultiplication.CurveLaws.incident_pos line 136
  21. theorem OAI.MatrixMultiplication.CurveLaws.hidden_nonneg line 144
  22. theorem OAI.MatrixMultiplication.CurveLaws.leaf_entropy line 151
  23. theorem OAI.MatrixMultiplication.CurveLaws.conditional_entropy line 156
  24. theorem OAI.MatrixMultiplication.CurveLaws.hidden_closed line 162
  25. theorem OAI.MatrixMultiplication.CurveLaws.incident_rate line 174
  26. theorem OAI.MatrixMultiplication.CurveLaws.hidden_rate line 180