OAI/LinearAlgebra/MatrixMultiplication/JointExtraction/PopulationRates.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Joint tensor extraction, compatibility and entropy estimates.

  1. theorem OAI.MatrixMultiplication.JointPopulationRates.tendsto_log_multinomial_div_of_total_div_zero line 18
  2. theorem OAI.MatrixMultiplication.JointPopulationRates.tendsto_log_multinomial_div_of_mass line 54
  3. theorem OAI.MatrixMultiplication.JointPopulationRates.tendsto_total_div_of_coordinate_rates line 77
  4. theorem OAI.MatrixMultiplication.JointPopulationRates.tendsto_empirical_of_coordinate_rates line 86
  5. theorem OAI.MatrixMultiplication.JointPopulationRates.finiteEntropy_scalar line 100
  6. theorem OAI.MatrixMultiplication.JointPopulationRates.weighted_empirical_entropy_eq line 106
  7. theorem OAI.MatrixMultiplication.JointPopulationRates.tendsto_weighted_empirical_entropy_of_coordinate_rates line 133
  8. def OAI.MatrixMultiplication.JointPopulationRates.sideCounts line 146
  9. def OAI.MatrixMultiplication.JointPopulationRates.sideMass line 149
  10. theorem OAI.MatrixMultiplication.JointPopulationRates.sideCounts_total line 152
  11. theorem OAI.MatrixMultiplication.JointPopulationRates.sideMass_total line 158
  12. theorem OAI.MatrixMultiplication.JointPopulationRates.tendsto_sideCounts_div_of_coordinate_rates line 164
  13. theorem OAI.MatrixMultiplication.JointPopulationRates.target_side_population line 189
  14. theorem OAI.MatrixMultiplication.JointPopulationRates.tendsto_weighted_target_side_entropy line 201
  15. theorem OAI.MatrixMultiplication.JointPopulationRates.tendsto_log_target_card_div line 218
  16. theorem OAI.MatrixMultiplication.JointPopulationRates.tendsto_log_target_card_div_of_coordinate_rates line 234
  17. theorem OAI.MatrixMultiplication.JointPopulationRates.tendsto_log_targetSet_card_div_of_coordinate_rates line 249