OAI/LinearAlgebra/MatrixFields/Entropy/ConditionalRateBridge.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MatrixAllFields.MatrixMultiplication.ConditionalLabels.normalizedCountLaw line 22
2. theorem OAI.MatrixAllFields.MatrixMultiplication.ConditionalLabels.normalizedCountLaw_mass line 29
3. theorem OAI.MatrixAllFields.MatrixMultiplication.ConditionalLabels.normalized_prefix_mass line 34
4. theorem OAI.MatrixAllFields.MatrixMultiplication.ConditionalLabels.zero_prefix_contribution_of_count_eq_zero line 45
5. theorem OAI.MatrixAllFields.MatrixMultiplication.ConditionalLabels.tendsto_log_prefix_multinomial line 54
6. theorem OAI.MatrixAllFields.MatrixMultiplication.ConditionalLabels.stageEntropyRate_div_eq_refinementEntropy line 79
7. theorem OAI.MatrixAllFields.MatrixMultiplication.ConditionalLabels.stagePairingRate_div_eq_lawPairingRate line 113
8. theorem OAI.MatrixAllFields.MatrixMultiplication.ConditionalLabels.tendsto_log_stagePairingSize_law line 129
9. theorem OAI.MatrixAllFields.MatrixMultiplication.ConditionalLabels.stageEntropyRate_div_eq_normalizedCountLaw_refinementEntropy line 140
10. theorem OAI.MatrixAllFields.MatrixMultiplication.ConditionalLabels.tendsto_log_stagePairingSize_normalizedCountLaw line 149