OAI/Dynamics/ConditionalShuffle/Sequences.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Thorp.Fourier.tv_realProduct line 10
2. lemma OAI.Thorp.Fourier.character_probability_norm line 30
3. lemma OAI.Thorp.Fourier.character_realProduct_last line 43
4. lemma OAI.Thorp.Specht.error_sum_sqrt_bound line 61
5. theorem OAI.Thorp.Specht.repaired_eight_tv line 71