OAI/LinearAlgebra/MatrixMultiplication/Entropy/ConditionalRateBridge.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Finite entropy, rate estimates and ordered asymptotic limits.

  1. def OAI.MatrixMultiplication.ConditionalLabels.normalizedCountLaw line 19
  2. theorem OAI.MatrixMultiplication.ConditionalLabels.normalizedCountLaw_mass line 26
  3. theorem OAI.MatrixMultiplication.ConditionalLabels.normalized_prefix_mass line 31
  4. theorem OAI.MatrixMultiplication.ConditionalLabels.zero_prefix_contribution_of_count_eq_zero line 42
  5. theorem OAI.MatrixMultiplication.ConditionalLabels.tendsto_log_prefix_multinomial line 51
  6. theorem OAI.MatrixMultiplication.ConditionalLabels.stageEntropyRate_div_eq_refinementEntropy line 76
  7. theorem OAI.MatrixMultiplication.ConditionalLabels.stagePairingRate_div_eq_lawPairingRate line 110
  8. theorem OAI.MatrixMultiplication.ConditionalLabels.tendsto_log_stagePairingSize_law line 126
  9. theorem OAI.MatrixMultiplication.ConditionalLabels.stageEntropyRate_div_eq_normalizedCountLaw_refinementEntropy line 137
  10. theorem OAI.MatrixMultiplication.ConditionalLabels.tendsto_log_stagePairingSize_normalizedCountLaw line 146