OAI/Probability/CriticalPercolation/Modular/PushMass.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CriticalPercolation.FiniteEntropy.pushMass line 19
2. lemma OAI.CriticalPercolation.FiniteEntropy.pushMass_nonneg line 23
3. lemma OAI.CriticalPercolation.FiniteEntropy.pushMass_sum line 27
4. lemma OAI.CriticalPercolation.FiniteEntropy.le_pushMass line 35
5. lemma OAI.CriticalPercolation.FiniteEntropy.sum_pushMass_mul line 43
6. lemma OAI.CriticalPercolation.FiniteEntropy.log_sum_inequality line 53
7. theorem OAI.CriticalPercolation.FiniteEntropy.divergence_pushMass_le line 96