OAI/Probability/ThorpShuffle/ConvolutionBounds.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Thorp.Fourier.hsSq_power_le line 17
2. lemma OAI.Thorp.Fourier.Family.eight_transform_bound line 26
3. lemma OAI.Thorp.Fourier.integrated_uniform_real line 55
4. lemma OAI.Thorp.Fourier.centered_trivial line 61
5. lemma OAI.Thorp.Fourier.centered_character line 72
6. theorem OAI.Thorp.Specht.permutation_eight_bound line 89