OAI/Dynamics/ConditionalShuffle/CycleIterate.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Thorp.Conditional.OverlayEnergy.cycles line 9
2. def OAI.Thorp.Conditional.OverlayEnergy.cyclesPerm line 13
3. lemma OAI.Thorp.Conditional.OverlayEnergy.cycles_free line 17
4. lemma OAI.Thorp.Conditional.OverlayEnergy.cycles_count line 25
5. lemma OAI.Thorp.Conditional.OverlayEnergy.cycles_mass line 31
6. lemma OAI.Thorp.Conditional.OverlayEnergy.cycles_support line 37
7. lemma OAI.Thorp.Conditional.OverlayEnergy.cycles_energy_le line 44
8. lemma OAI.Thorp.Conditional.OverlayEnergy.cycles_expected_energy line 50