OAI/NumberTheory/OrdinaryCorrelations/AbsoluteDefect/Line.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.OrdinaryHorizontalHalasz.line line 22
  2. lemma OAI.OrdinaryHorizontalHalasz.line_re line 23
  3. lemma OAI.OrdinaryHorizontalHalasz.line_add line 24
  4. def OAI.OrdinaryHorizontalHalasz.energyConstant line 28
  5. def OAI.OrdinaryHorizontalHalasz.rootGaussian line 31
  6. lemma OAI.OrdinaryHorizontalHalasz.norm_rootGaussian line 33
  7. lemma OAI.OrdinaryHorizontalHalasz.rootGaussian_sq line 36
  8. lemma OAI.OrdinaryHorizontalHalasz.continuous_rootGaussian line 39
  9. lemma OAI.OrdinaryHorizontalHalasz.continuous_lseries_comp line 43
  10. lemma OAI.OrdinaryHorizontalHalasz.continuous_vertical line 51
  11. lemma OAI.OrdinaryHorizontalHalasz.continuous_shifted line 59
  12. lemma OAI.OrdinaryHorizontalHalasz.weighted_energy_integrable line 68
  13. lemma OAI.OrdinaryHorizontalHalasz.weighted_energy_on line 74
  14. lemma OAI.OrdinaryHorizontalHalasz.root_energy_on line 84
  15. lemma OAI.OrdinaryHorizontalHalasz.horizontal_weighted_decomposition line 90
  16. lemma OAI.OrdinaryHorizontalHalasz.weighted_derivative_integrand line 144
  17. theorem OAI.OrdinaryHorizontalHalasz.weighted_derivative_bound line 154