OAI/LinearAlgebra/MatrixFields/Entropy/StageCTerminalRates.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldStageCTerminalRates.sum_populationHistory_rate line 19
2. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldStageCTerminalRates.log_populationVolume_eq_bPositive line 51
3. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldStageCTerminalRates.normalized_log_populationVolume_eq_bPositive line 60
4. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldStageCTerminalRates.normalized_log_populationVolume_allocation_independent line 70
5. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldStageCTerminalRates.tendsto_normalized_log_populationVolume line 80
6. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldStageCTerminalRates.interiorS2 line 91
7. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldStageCTerminalRates.bPositive_rate_eq_interior line 97
8. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldStageCTerminalRates.log_populationVolume_eq_interior line 105
9. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldStageCTerminalRates.normalized_log_populationVolume_eq_interior line 112