OAI/NumberTheory/Ostmann/QuadraticCenter/WalshTensor.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.QuadraticCenter.signMean_const line 10
2. theorem OAI.Ostmann.QuadraticCenter.signMean_mono line 14
3. theorem OAI.Ostmann.QuadraticCenter.signMean_pair_flip line 18
4. theorem OAI.Ostmann.QuadraticCenter.restrictedWalsh_even_moment_le line 25
5. theorem OAI.Ostmann.QuadraticCenter.walsh_even_moment_le_weighted_energy line 74