OAI/NumberTheory/Ostmann/QuadraticCenter/BiasSelectionWindows.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.QuadraticCenter.positiveIntegerEmbedding line 12
2. def OAI.Ostmann.QuadraticCenter.negativeIntegerEmbedding line 17
3. def OAI.Ostmann.QuadraticCenter.positiveIntegerWindow line 22
4. def OAI.Ostmann.QuadraticCenter.negativeIntegerWindow line 25
5. def OAI.Ostmann.QuadraticCenter.integerQuadraticMean line 28
6. lemma OAI.Ostmann.QuadraticCenter.oriented_integerQuadraticMean line 31
7. lemma OAI.Ostmann.QuadraticCenter.quadraticCharacter_nat_translate line 39
8. lemma OAI.Ostmann.QuadraticCenter.quadraticCharacter_neg_nat_translate line 45
9. lemma OAI.Ostmann.QuadraticCenter.positive_window_complex_mean line 51
10. lemma OAI.Ostmann.QuadraticCenter.negative_window_complex_mean line 63
11. lemma OAI.Ostmann.QuadraticCenter.quadratic_complement_density_relation line 75