OAI/NumberTheory/OrdinaryCorrelations/AbsoluteDefect/IntegralInverseFiveQuarters.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.OrdinaryHalaszEnvelopes.integral_inverse_five_quarters line 21
2. lemma OAI.OrdinaryHalaszEnvelopes.band_envelope_identity line 27
3. lemma OAI.OrdinaryHalaszEnvelopes.band_envelope_integral line 37
4. lemma OAI.OrdinaryHalaszEnvelopes.band_scale_identity line 76
5. lemma OAI.OrdinaryHalaszEnvelopes.band_scaled_expression line 83
6. lemma OAI.OrdinaryHalaszEnvelopes.band_normalized_bound line 90