OAI/Combinatorics/RamseyFive/Entropy/GuardedNodeOriginal.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SharpRamseyFive.FiniteEntropy.eventMass_pure_filter_of_not line 11
2. theorem OAI.SharpRamseyFive.ProjectiveIncidence.guardedNode_original line 27
3. theorem OAI.SharpRamseyFive.ProjectiveIncidence.nextAmbientCapLaw_original line 57
4. theorem OAI.SharpRamseyFive.ProjectiveIncidence.second_ambient_unconditioned line 85
5. theorem OAI.SharpRamseyFive.ProjectiveIncidence.first_ambient_chronology line 101
6. def OAI.SharpRamseyFive.FiniteEntropy.inheritedSupport line 124
7. def OAI.SharpRamseyFive.FiniteEntropy.evictionFraction line 127
8. lemma OAI.SharpRamseyFive.FiniteEntropy.evictionFraction_nonneg line 129
9. lemma OAI.SharpRamseyFive.FiniteEntropy.inherited_eviction line 132
10. lemma OAI.SharpRamseyFive.FiniteEntropy.trim_failure_eviction line 144
11. theorem OAI.SharpRamseyFive.FiniteEntropy.trim_failure_mass line 156