OAI/Probability/ThorpShuffle/FixedLists/Energy.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Thorp.Conditional.halfDensity_after_step_sixteen line 12

   Also declared: OAI/Dynamics/ConditionalShuffle/Disintegration.lean:154 (same declaration text).

2. theorem OAI.Thorp.Conditional.expectedNoise_dimension_sixteen line 29

   Also declared: OAI/Dynamics/ConditionalShuffle/Disintegration.lean:171 (same declaration text).

3. theorem OAI.Thorp.Conditional.expectedNoise_bound_sixteen line 68

   Also declared: OAI/Dynamics/ConditionalShuffle/Disintegration.lean:210 (same declaration text).

4. theorem OAI.Thorp.Conditional.expectedEnergy_decay_sixteen line 80

   Also declared: OAI/Dynamics/ConditionalShuffle/Disintegration.lean:229 (same declaration text).

5. theorem OAI.Thorp.Conditional.expectedEnergy_long line 94
6. theorem OAI.Thorp.Conditional.prefix_test_bound_sixteen line 102