OAI/LinearAlgebra/MatrixMultiplication/Entropy/ComplexAnalyticValue.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

Finite entropy, rate estimates and ordered asymptotic limits.

  1. theorem OAI.MatrixMultiplication.Foundation.unitInterval_subset_closure_rat line 23
  2. structure OAI.MatrixMultiplication.Foundation.FiniteConstructionRates line 39
  3. def OAI.MatrixMultiplication.Foundation.FiniteConstructionRates.score line 49
  4. structure OAI.MatrixMultiplication.Foundation.AttainableFamily line 53
  5. def OAI.MatrixMultiplication.Foundation.finiteConstructionFamily line 57
  6. def OAI.MatrixMultiplication.Foundation.AttainableFamily.pairs line 65
  7. def OAI.MatrixMultiplication.Foundation.AttainableFamily.closedPairs line 68
  8. def OAI.MatrixMultiplication.Foundation.AttainableFamily.fiber line 70
  9. def OAI.MatrixMultiplication.Foundation.AttainableFamily.value line 72
  10. theorem OAI.MatrixMultiplication.Foundation.AttainableFamily.finite_mem_closedPairs line 74
  11. theorem OAI.MatrixMultiplication.Foundation.AttainableFamily.closedPairs_law_mem_of_isClosed line 77
  12. theorem OAI.MatrixMultiplication.Foundation.AttainableFamily.closedPairs_downward line 86
  13. theorem OAI.MatrixMultiplication.Foundation.AttainableFamily.isClosed_fiber line 100
  14. theorem OAI.MatrixMultiplication.Foundation.AttainableFamily.value_mem_closedPairs line 103
  15. theorem OAI.MatrixMultiplication.Foundation.AttainableFamily.mem_closedPairs_iff_le_value line 107
  16. theorem OAI.MatrixMultiplication.Foundation.AttainableFamily.closedPairs_le_continuous_cap line 114
  17. theorem OAI.MatrixMultiplication.Foundation.AttainableFamily.value_le_continuous_cap line 122
  18. theorem OAI.MatrixMultiplication.Foundation.AttainableFamily.value_nonneg line 127
  19. theorem OAI.MatrixMultiplication.Foundation.AttainableFamily.upperSemicontinuous_value line 131
  20. theorem OAI.MatrixMultiplication.Foundation.AttainableFamily.upperSemicontinuous_value_comp line 147
  21. theorem OAI.MatrixMultiplication.Foundation.AttainableFamily.exists_finite_in_open_gt line 165
  22. theorem OAI.MatrixMultiplication.Foundation.AttainableFamily.exists_finite_gt line 174
  23. theorem OAI.MatrixMultiplication.Foundation.AttainableFamily.concaveOn_value line 183
  24. theorem OAI.MatrixMultiplication.Foundation.AttainableFamily.closedPairs_convex_of_rational_mixing line 199
  25. abbrev OAI.MatrixMultiplication.Foundation.realSimplex line 249
  26. theorem OAI.MatrixMultiplication.Foundation.convex_realSimplex line 252
  27. theorem OAI.MatrixMultiplication.Foundation.simplex_residual line 260
  28. theorem OAI.MatrixMultiplication.Foundation.concave_simplex_domination line 269
  29. theorem OAI.MatrixMultiplication.Foundation.lowerSemicontinuousOn_nonneg_concave_simplex line 287
  30. theorem OAI.MatrixMultiplication.Foundation.lowerSemicontinuous_comp_of_mem line 319
  31. theorem OAI.MatrixMultiplication.Foundation.AttainableFamily.continuous_value_on_simplex_chart line 328