OAI/Dynamics/ConditionalShuffle/PhysicalMix.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Revealed.Physical.eight_block_coset_ratio line 11
2. def OAI.Revealed.Physical.fullConditionalRate line 28
3. lemma OAI.Revealed.Physical.fullConditionalRate_tendsto line 31
4. lemma OAI.Revealed.Physical.physical_distance_bound line 39
5. lemma OAI.Revealed.Physical.physical_distance_eventually line 73