OAI/Dynamics/ConditionalShuffle/UniformEnergy.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Thorp.Conditional.ofSubtype_symm_apply_not_mem line 9
2. lemma OAI.Thorp.Conditional.ofSubtype_bool_preserves line 15
3. lemma OAI.Thorp.Conditional.sum_subtype_supported line 24
4. def OAI.Thorp.Conditional.rawPermute line 37
5. lemma OAI.Thorp.Conditional.rawPermute_energy line 40
6. lemma OAI.Thorp.Conditional.rawPermute_free_assignment line 44
7. lemma OAI.Thorp.Conditional.rawPermute_weight_assignment line 50
8. lemma OAI.Thorp.Conditional.rawIterate_assignment_matrix line 81
9. lemma OAI.Thorp.Conditional.rawIterate_assignment_energy_le line 97
10. lemma OAI.Thorp.Conditional.raw_uniform_sweep line 123