OAI/NumberTheory/OrdinaryCorrelations/AbsoluteDefect/FourierMass.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.OrdinaryAnalyticCutoff.fourierMass line 28
2. lemma OAI.OrdinaryAnalyticCutoff.fourierMass_nonneg line 29
3. lemma OAI.OrdinaryAnalyticCutoff.inversion line 32
4. lemma OAI.OrdinaryAnalyticCutoff.integrable_kernel line 40
5. lemma OAI.OrdinaryAnalyticCutoff.linear_cutoff_bound line 48
6. lemma OAI.OrdinaryAnalyticCutoff.bilinear_cutoff_bound line 81