OAI/NumberTheory/OrdinaryCorrelations/AbsoluteDefect/Vertical.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.OrdinaryRieszPerron.vertical line 20
  2. def OAI.OrdinaryRieszPerron.cutoffSeries line 22
  3. def OAI.OrdinaryRieszPerron.perronConstant line 25
  4. lemma OAI.OrdinaryRieszPerron.vertical_re line 27
  5. lemma OAI.OrdinaryRieszPerron.term_norm_vertical line 29
  6. lemma OAI.OrdinaryRieszPerron.continuous_vertical_kernel line 33
  7. lemma OAI.OrdinaryRieszPerron.continuous_vertical_term line 49
  8. lemma OAI.OrdinaryRieszPerron.scaled_term line 62
  9. lemma OAI.OrdinaryRieszPerron.norm_scaled_integrand line 71
  10. lemma OAI.OrdinaryRieszPerron.integrable_scaled_term line 76
  11. lemma OAI.OrdinaryRieszPerron.perron_term line 88
  12. theorem OAI.OrdinaryRieszPerron.cutoffSeries_perron line 104