OAI/LinearAlgebra/MatrixMultiplication/JointExtraction/OrdinaryPopulationSelection.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

Joint tensor extraction, compatibility and entropy estimates.

  1. def OAI.MatrixMultiplication.JointOrdinaryPopulationSelection.entropyRate line 23
  2. def OAI.MatrixMultiplication.JointOrdinaryPopulationSelection.sideDegreeRate line 26
  3. def OAI.MatrixMultiplication.JointOrdinaryPopulationSelection.degreeRate line 29
  4. def OAI.MatrixMultiplication.JointOrdinaryPopulationSelection.sideCapacity line 32
  5. theorem OAI.MatrixMultiplication.JointOrdinaryPopulationSelection.entropyRate_sub_degreeRate_eq line 36
  6. theorem OAI.MatrixMultiplication.JointOrdinaryPopulationSelection.sideMass_entropy_le line 42
  7. theorem OAI.MatrixMultiplication.JointOrdinaryPopulationSelection.sideDegreeRate_nonneg line 48
  8. theorem OAI.MatrixMultiplication.JointOrdinaryPopulationSelection.degreeRate_nonneg line 54
  9. theorem OAI.MatrixMultiplication.JointOrdinaryPopulationSelection.sideDegreeRate_le line 59
  10. def OAI.MatrixMultiplication.JointOrdinaryPopulationSelection.uniformDegree line 67
  11. theorem OAI.MatrixMultiplication.JointOrdinaryPopulationSelection.ordinary_neighbors_eq line 71
  12. theorem OAI.MatrixMultiplication.JointOrdinaryPopulationSelection.neighbors_card_le_uniformDegree line 87
  13. theorem OAI.MatrixMultiplication.JointOrdinaryPopulationSelection.uniformDegree_attained line 97
  14. theorem OAI.MatrixMultiplication.JointOrdinaryPopulationSelection.uniformDegree_log_upper_of_all_targets line 109
  15. theorem OAI.MatrixMultiplication.JointOrdinaryPopulationSelection.tendsto_sum_gibbsExponent line 121
  16. theorem OAI.MatrixMultiplication.JointOrdinaryPopulationSelection.uniformDegree_log_upper_of_word_support line 147
  17. theorem OAI.MatrixMultiplication.JointOrdinaryPopulationSelection.uniformDegree_log_upper line 173
  18. def OAI.MatrixMultiplication.JointOrdinaryPopulationSelection.selectionHashRate line 190
  19. theorem OAI.MatrixMultiplication.JointOrdinaryPopulationSelection.eventually_exists_selection_of_word_support line 193
  20. theorem OAI.MatrixMultiplication.JointOrdinaryPopulationSelection.eventually_exists_selection line 248