OAI/NumberTheory/DirichletL/RowCompletion/PolynomialHeight.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CanonicalRowCompletion.outside_separated_cube_coefficient_bound line 83
  2. def OAI.CompletedHeight.positiveCutoff line 121
  3. lemma OAI.CompletedHeight.positiveCutoff_one line 127
  4. lemma OAI.CompletedHeight.positiveCutoff_zero line 134
  5. def OAI.CompletedHeight.logCorrection line 143
  6. def OAI.CompletedHeight.patchedLog line 146
  7. lemma OAI.CompletedHeight.logCorrection_compact line 148
  8. lemma OAI.CompletedHeight.logCorrection_smooth line 151
  9. lemma OAI.CompletedHeight.patchedLog_temperate line 164
  10. lemma OAI.CompletedHeight.patchedLog_proper line 169
  11. lemma OAI.CompletedHeight.patchedLog_eq_log line 182
  12. def OAI.CompletedHeight.sourceTwistCLM line 187
  13. lemma OAI.CompletedHeight.sourceTwistCLM_apply line 192
  14. def OAI.CompletedHeight.normTwistedSource line 199
  15. lemma OAI.CompletedHeight.normTwistedSource_support line 201
  16. theorem OAI.CompletedHeight.frequencyTwist_finite_bound line 206
  17. theorem OAI.CompletedHeight.normTwistedSource_schwartz line 227
  18. theorem OAI.LocalLogFourier.coupled_positive_log_separation_linear_constant line 268
  19. def OAI.CompletedHeight.HasPolynomialKernel line 412
  20. theorem OAI.CompletedHeight.normTwistedSource_polynomial_kernel line 418
  21. theorem OAI.CompletedHeight.polynomial_kernel_log_separation line 448
  22. theorem OAI.CompletedHeight.polynomial_kernel_three_window line 471
  23. theorem OAI.CompletedHeight.polynomial_smooth_quadratic line 504
  24. theorem OAI.CompletedHeight.polynomial_smooth_series_rowPhase line 621