OAI/NumberTheory/DirichletL/CubicSieve/RankMargins.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SecondPassArithmetic.canonicalPadding line 79
  2. theorem OAI.SecondPassArithmetic.canonicalPadding_budget line 82
  3. theorem OAI.SecondPassArithmetic.canonicalRankMargin_le line 101
  4. theorem OAI.SecondPassArithmetic.canonicalRankMargin_reserved line 107
  5. theorem OAI.SecondPassArithmetic.canonicalRankMargin_initial_bound line 116
  6. theorem OAI.SecondPassArithmetic.canonicalRankMargin_final_bound line 125
  7. theorem OAI.CanonicalRowCompletion.canonicalLogEnergy_eq_completed_rows line 145
  8. theorem OAI.CanonicalRowCompletion.log_rows_family_binned_energy line 176
  9. def OAI.CompletedHeight.fixedLogReturnCLM line 206
  10. lemma OAI.CompletedHeight.fixedLogReturnCLM_apply line 212
  11. lemma OAI.CompletedHeight.positiveCutoff_support_bounds line 220
  12. theorem OAI.CompletedHeight.frequencyTwist_finite_uniform_degree line 228
  13. def OAI.CompletedHeight.uniformTwistedSchwartz line 250
  14. lemma OAI.CompletedHeight.uniformTwistedSchwartz_apply line 254
  15. theorem OAI.CompletedHeight.normTwistedSource_uniform_degree line 273
  16. def OAI.CompletedHeight.HasUniformPolynomialKernel line 294
  17. abbrev OAI.CompletedHeight.SupportedSmoothSource line 300
  18. theorem OAI.CompletedHeight.normTwistedSource_uniform_polynomial_kernel line 303
  19. theorem OAI.CompletedHeight.uniform_polynomial_kernel_log_separation line 336
  20. theorem OAI.CompletedHeight.uniform_polynomial_kernel_three_window line 362
  21. theorem OAI.CompletedHeight.uniform_polynomial_smooth_quadratic line 398
  22. theorem OAI.CompletedHeight.uniform_polynomial_smooth_series_rowPhase line 518