OAI/NumberTheory/DirichletL/CubicSieve/DyadicKernel.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SecondPassArithmetic.finite_bounded_rows_smoothed_expand line 81
  2. lemma OAI.SecondPassArithmetic.multiplicityRow_norm_le_one line 128
  3. lemma OAI.SecondPassArithmetic.multiplicityRow_support line 141
  4. def OAI.SecondPassArithmetic.reopenedCanonicalRow line 151
  5. theorem OAI.SecondPassArithmetic.reopenedCanonicalRow_smoothed_expand line 158
  6. def OAI.CompletedGauss.completedDualScale line 219
  7. theorem OAI.CompletedGauss.positive_log_scale_identity line 222
  8. theorem OAI.CompletedGauss.completed_ideal_kernel_scale line 235
  9. theorem OAI.CompletedDyadic.weighted_scale_identity line 254
  10. theorem OAI.CompletedDyadic.double_kernel_sum_bound line 261
  11. def OAI.CompletedDyadic.ramifiedScale line 290
  12. theorem OAI.CompletedDyadic.ramifiedScale_pos line 292
  13. theorem OAI.CompletedDyadic.triple_kernel_sum_bound line 295
  14. def OAI.CompletedDyadic.normMajorant line 356
  15. theorem OAI.CompletedDyadic.normMajorant_nonneg line 360
  16. theorem OAI.CompletedDyadic.normMajorant_eq line 364
  17. theorem OAI.CompletedDyadic.smooth_energy_le_normMajorant_sq line 375
  18. def OAI.CompletedDyadic.tripleTerm line 395
  19. theorem OAI.CompletedDyadic.tripleTerm_nonneg line 399
  20. theorem OAI.CompletedDyadic.triple_product_kernel_sum_bound line 405
  21. theorem OAI.CompletedDyadic.normMajorant_eq_triples line 433
  22. theorem OAI.CompletedDyadic.normMajorant_sum_bound line 440
  23. theorem OAI.CompletedGauss.finite_tsum_energy_bound line 478
  24. def OAI.CompletedGauss.completedSmoothDyadicBlock line 511
  25. theorem OAI.CompletedGauss.completed_smooth_series line 524