OAI/MathematicalPhysics/AlternatingFlow/EffectiveProfiles.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.AlternatingNS.Effective.factorial line 14
2. lemma OAI.AlternatingNS.Effective.sum_range line 24
3. lemma OAI.AlternatingNS.Effective.choose line 36
4. lemma OAI.AlternatingNS.Effective.rhoBound line 47
5. lemma OAI.AlternatingNS.Effective.reciprocalBound line 52
6. lemma OAI.AlternatingNS.Effective.transitionInvBound line 63
7. lemma OAI.AlternatingNS.Effective.transitionBound line 69
8. theorem OAI.AlternatingNS.Effective.profile_bound_programs line 76