OAI/Probability/ThorpShuffle/SpectralDecay.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Thorp.Conditional.half_weight_sum line 14
2. theorem OAI.Thorp.Conditional.half_weight_geometric_identity line 22
3. theorem OAI.Thorp.Conditional.half_weight_geometric_bound line 35
4. theorem OAI.Thorp.Conditional.spectral_track_unroll line 49
5. theorem OAI.Thorp.Conditional.energy_of_spectral_tracks line 69
6. theorem OAI.Thorp.Conditional.scalar_decay line 77
7. theorem OAI.Thorp.Conditional.eight_block_geometric_choice line 138