OAI/Dynamics/ConditionalShuffle/SweepAverage.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Thorp.Conditional.freeCount_comp_equiv line 9
2. lemma OAI.Thorp.Conditional.card_without line 15
3. lemma OAI.Thorp.Conditional.freeCount_without line 21
4. lemma OAI.Thorp.Conditional.mean_right_randomize line 29
5. lemma OAI.Thorp.Conditional.ofSubtype_symm_apply line 37
6. lemma OAI.Thorp.Conditional.rawPoint_energy_product line 45
7. lemma OAI.Thorp.Conditional.rawPoint_uniform_sweep line 53