OAI/Dynamics/ConditionalShuffle/PrepEnergy.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Thorp.Conditional.rawEnergy_nonneg line 9
2. lemma OAI.Thorp.Conditional.rawIterate_energy_le line 12
3. lemma OAI.Thorp.Conditional.rawPermute_eq_of_free line 18
4. def OAI.Thorp.Conditional.extendTuple line 43
5. lemma OAI.Thorp.Conditional.extendTuple_extends line 47
6. lemma OAI.Thorp.Conditional.rawPermute_extend_free line 52
7. lemma OAI.Thorp.Conditional.prep_score_bound line 72
8. lemma OAI.Thorp.Conditional.prep_sweep_energy line 110