OAI/Probability/CriticalPercolation/Criticality/ReverseReference.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CriticalPercolation.ReverseReference.weight line 13
2. def OAI.CriticalPercolation.ReverseReference.recover line 19
3. lemma OAI.CriticalPercolation.ReverseReference.weight_nonneg line 24
4. lemma OAI.CriticalPercolation.ReverseReference.weight_sum_le line 31
5. def OAI.CriticalPercolation.ReverseReference.terminalWeight line 50
6. lemma OAI.CriticalPercolation.ReverseReference.terminalWeight_nonneg line 54
7. lemma OAI.CriticalPercolation.ReverseReference.terminalWeight_sum line 59
8. def OAI.CriticalPercolation.ReverseReference.joint line 65
9. lemma OAI.CriticalPercolation.ReverseReference.joint_nonneg line 70
10. lemma OAI.CriticalPercolation.ReverseReference.joint_marginal_le line 76
11. lemma OAI.CriticalPercolation.FiniteEntropy.pushMass_at_supported_injection line 94
12. lemma OAI.CriticalPercolation.FiniteEntropy.divergence_reference_mono line 108
13. theorem OAI.CriticalPercolation.FiniteEntropy.mapped_entropy_le line 121