OAI/NumberTheory/OrdinaryCorrelations/AbsoluteDefect/ContinuousOnShiftRpow.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.OrdinaryHalaszEnvelopes.continuousOn_shift_rpow line 18
2. lemma OAI.OrdinaryHalaszEnvelopes.integral_shift_rpow line 26
3. lemma OAI.OrdinaryHalaszEnvelopes.integral_inverse_sqrt line 39
4. lemma OAI.OrdinaryHalaszEnvelopes.integral_inverse_cube line 46
5. lemma OAI.OrdinaryHalaszEnvelopes.sqrt_energy_le line 56
6. lemma OAI.OrdinaryHalaszEnvelopes.envelope_identity line 66
7. lemma OAI.OrdinaryHalaszEnvelopes.envelope_integral line 73
8. lemma OAI.OrdinaryHalaszEnvelopes.scaled_expression line 104
9. lemma OAI.OrdinaryHalaszEnvelopes.normalized_bound line 111