OAI/LinearAlgebra/MatrixFields/Parameters/JointOrdinaryPopulationSelection.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MatrixAllFields.MatrixMultiplication.JointCapacityAlgebra.total_sub_max_degrees line 16
  2. theorem OAI.MatrixAllFields.MatrixMultiplication.JointCapacityAlgebra.weighted_joint_capacity line 21
  3. def OAI.MatrixAllFields.MatrixMultiplication.JointOrdinaryPopulationSelection.entropyRate line 49
  4. def OAI.MatrixAllFields.MatrixMultiplication.JointOrdinaryPopulationSelection.sideDegreeRate line 52
  5. def OAI.MatrixAllFields.MatrixMultiplication.JointOrdinaryPopulationSelection.degreeRate line 55
  6. def OAI.MatrixAllFields.MatrixMultiplication.JointOrdinaryPopulationSelection.sideCapacity line 58
  7. theorem OAI.MatrixAllFields.MatrixMultiplication.JointOrdinaryPopulationSelection.entropyRate_sub_degreeRate_eq line 62
  8. theorem OAI.MatrixAllFields.MatrixMultiplication.JointOrdinaryPopulationSelection.sideMass_entropy_le line 68
  9. theorem OAI.MatrixAllFields.MatrixMultiplication.JointOrdinaryPopulationSelection.sideDegreeRate_nonneg line 74
  10. theorem OAI.MatrixAllFields.MatrixMultiplication.JointOrdinaryPopulationSelection.degreeRate_nonneg line 80
  11. theorem OAI.MatrixAllFields.MatrixMultiplication.JointOrdinaryPopulationSelection.sideDegreeRate_le line 85
  12. def OAI.MatrixAllFields.MatrixMultiplication.JointOrdinaryPopulationSelection.uniformDegree line 93
  13. theorem OAI.MatrixAllFields.MatrixMultiplication.JointOrdinaryPopulationSelection.ordinary_neighbors_eq line 97
  14. theorem OAI.MatrixAllFields.MatrixMultiplication.JointOrdinaryPopulationSelection.neighbors_card_le_uniformDegree line 106
  15. theorem OAI.MatrixAllFields.MatrixMultiplication.JointOrdinaryPopulationSelection.uniformDegree_attained line 116
  16. theorem OAI.MatrixAllFields.MatrixMultiplication.JointOrdinaryPopulationSelection.uniformDegree_log_upper_of_all_targets line 128
  17. theorem OAI.MatrixAllFields.MatrixMultiplication.JointOrdinaryPopulationSelection.tendsto_sum_gibbsExponent line 140
  18. theorem OAI.MatrixAllFields.MatrixMultiplication.JointOrdinaryPopulationSelection.uniformDegree_log_upper_of_word_support line 166
  19. theorem OAI.MatrixAllFields.MatrixMultiplication.JointOrdinaryPopulationSelection.uniformDegree_log_upper line 192
  20. def OAI.MatrixAllFields.MatrixMultiplication.JointOrdinaryPopulationSelection.selectionHashRate line 209
  21. theorem OAI.MatrixAllFields.MatrixMultiplication.JointOrdinaryPopulationSelection.eventually_exists_selection_of_word_support line 212
  22. theorem OAI.MatrixAllFields.MatrixMultiplication.JointOrdinaryPopulationSelection.eventually_exists_selection line 267