OAI/NumberTheory/DirichletL/GaussSum/CompletedDyadicRows.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CompletedGauss.two_pow_clog_le_double line 82
  2. def OAI.CompletedGauss.completedRowDyad line 94
  3. def OAI.CompletedGauss.completedRowDyadicLength line 97
  4. theorem OAI.CompletedGauss.completedRowDyad_bounds line 99
  5. theorem OAI.CompletedGauss.completedRowDyad_sum line 112
  6. theorem OAI.CompletedGauss.completedRowDyadic_top line 122
  7. theorem OAI.CompletedGauss.completedRowDyadic_scale line 128
  8. theorem OAI.CompletedGauss.completedRowDyadic_mass line 133
  9. theorem OAI.CompletedGauss.completedRowDyadic_shape line 148
  10. def OAI.CompletedGauss.HasExactCompletedDyadicModels line 178
  11. theorem OAI.CompletedGauss.completed_mean_square_of_exact_reflection line 183
  12. def OAI.CompletedGauss.completedRamifiedInitial line 253
  13. def OAI.CompletedGauss.completedRamifiedStep line 254
  14. theorem OAI.CompletedGauss.completedRamifiedInitial_pos line 256
  15. theorem OAI.CompletedGauss.completedRamifiedStep_gt_one line 260
  16. theorem OAI.CompletedGauss.actual_ramified_scale line 263
  17. theorem OAI.CompletedGauss.actual_ramified_norm line 270
  18. theorem OAI.CompletedGauss.cusp_coefficient_normalization line 276
  19. def OAI.CompletedGauss.normalizedCuspAmplitude line 291
  20. theorem OAI.CompletedGauss.normalizedCuspAmplitude_norm line 294
  21. theorem OAI.CompletedGauss.cusp_coefficient_norm line 300
  22. theorem OAI.CompletedGauss.short_completed_average_of_exact_reflection line 314
  23. def OAI.InitialMeanSquare.initialSquarefreeSector line 395
  24. theorem OAI.InitialMeanSquare.initial_weight_squarefree line 398
  25. theorem OAI.InitialMeanSquare.initial_source_eq_squarefree line 407
  26. theorem OAI.InitialMeanSquare.initial_squarefree_label_admissible line 432
  27. theorem OAI.InitialMeanSquare.initial_squarefree_target_admissible line 459
  28. theorem OAI.InitialMeanSquare.initial_subbin_transfer line 476
  29. theorem OAI.InitialMeanSquare.initialBinCost_of_canonical_bound line 542