OAI/NumberTheory/Jacobsthal/Estimates/SquarefreeHarmonic.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos970.NumberTheoryLean.SelbergOptimization.sum_multiples_reverse line 18
  2. def OAI.Erdos970.NumberTheoryLean.SelbergOptimization.lowerMobius line 34
  3. theorem OAI.Erdos970.NumberTheoryLean.SelbergOptimization.sum_lowerMobius line 37
  4. def OAI.Erdos970.NumberTheoryLean.SelbergOptimization.inverseMultiples line 43
  5. theorem OAI.Erdos970.NumberTheoryLean.SelbergOptimization.sum_inverseMultiples line 46
  6. def OAI.Erdos970.NumberTheoryLean.SelbergOptimization.normalization line 56
  7. theorem OAI.Erdos970.NumberTheoryLean.SelbergOptimization.normalization_pos line 59
  8. def OAI.Erdos970.NumberTheoryLean.SelbergOptimization.diagonalTarget line 74
  9. def OAI.Erdos970.NumberTheoryLean.SelbergOptimization.optimizedWeight line 77
  10. theorem OAI.Erdos970.NumberTheoryLean.SelbergOptimization.nu_mul_optimizedWeight line 80
  11. theorem OAI.Erdos970.NumberTheoryLean.SelbergOptimization.optimized_diagonal_coordinates line 87
  12. theorem OAI.Erdos970.NumberTheoryLean.SelbergOptimization.inverseMultiples_one line 102
  13. theorem OAI.Erdos970.NumberTheoryLean.SelbergOptimization.optimizedWeight_one line 110
  14. theorem OAI.Erdos970.NumberTheoryLean.SelbergOptimization.optimized_upperMoebius line 134
  15. theorem OAI.Erdos970.NumberTheoryLean.SelbergOptimization.optimized_mainSum line 138
  16. theorem OAI.Erdos970.NumberTheoryLean.SelbergOptimization.lowerMobius_abs_le line 164
  17. theorem OAI.Erdos970.NumberTheoryLean.SelbergOptimization.sum_abs_diagonalTarget line 180
  18. theorem OAI.Erdos970.NumberTheoryLean.SelbergOptimization.optimizedWeight_abs_le_inv_nu line 198
  19. theorem OAI.Erdos970.NumberTheoryLean.SelbergOptimization.optimizedWeight_eq_zero_of_cutoff_lt line 219
  20. theorem OAI.Erdos970.NumberTheoryLean.SelbergOptimization.sum_lambdaSquared line 239
  21. theorem OAI.Erdos970.NumberTheoryLean.SelbergOptimization.sum_abs_lambdaSquared_le line 268
  22. theorem OAI.Erdos970.NumberTheoryLean.SelbergOptimization.optimizedWeight_sum_abs_le_sq line 287
  23. theorem OAI.Erdos970.NumberTheoryLean.SelbergOptimization.optimized_lambda_error_norm line 321
  24. theorem OAI.Erdos970.NumberTheoryLean.SelbergOptimization.siftedSum_le_optimized line 334
  25. def OAI.Erdos970.NumberTheoryLean.SelbergOptimization.cutoffNormalization line 351
  26. theorem OAI.Erdos970.NumberTheoryLean.SelbergOptimization.cutoffNormalization_pos line 355
  27. theorem OAI.Erdos970.NumberTheoryLean.SelbergOptimization.cutoffSurvivors_le_optimized line 358
  28. def OAI.Erdos970.NumberTheoryLean.SquarefreeHarmonic.squarefreeUpTo line 392
  29. theorem OAI.Erdos970.NumberTheoryLean.SquarefreeHarmonic.mem_squarefreeUpTo line 396
  30. def OAI.Erdos970.NumberTheoryLean.SquarefreeHarmonic.squarefreeHarmonic line 402
  31. theorem OAI.Erdos970.NumberTheoryLean.SquarefreeHarmonic.interval_subset_square_product line 405
  32. theorem OAI.Erdos970.NumberTheoryLean.SquarefreeHarmonic.sum_inv_sq_le_two line 422
  33. theorem OAI.Erdos970.NumberTheoryLean.SquarefreeHarmonic.harmonic_le_twice_squarefreeHarmonic line 431
  34. theorem OAI.Erdos970.NumberTheoryLean.SquarefreeHarmonic.log_le_twice_squarefreeHarmonic line 455
  35. theorem OAI.Erdos970.NumberTheoryLean.SquarefreeHarmonic.nu_le_selbergTerms line 461
  36. theorem OAI.Erdos970.NumberTheoryLean.SquarefreeHarmonic.squarefreeUpTo_subset_cutoff_divisors line 475
  37. theorem OAI.Erdos970.NumberTheoryLean.SquarefreeHarmonic.squarefreeHarmonic_le_selberg_sum line 493
  38. theorem OAI.Erdos970.NumberTheoryLean.SquarefreeHarmonic.log_le_twice_selberg_sum line 518
  39. theorem OAI.Erdos970.NumberTheoryLean.SquarefreeHarmonic.log_le_twice_cutoffNormalization line 527
  40. theorem OAI.Erdos970.NumberTheoryLean.SquarefreeHarmonic.cutoffSurvivors_le_log_bound line 531
  41. theorem OAI.Erdos970.NumberTheoryLean.SquarefreeHarmonic.cutoffSurvivors_le_seventeen_of_eighth_radius line 546
  42. theorem OAI.Erdos970.NumberTheoryLean.SquarefreeHarmonic.cutoffSurvivors_le_seventeen line 597
  43. theorem OAI.Erdos970.NumberTheoryLean.SquarefreeHarmonic.cutoffSurvivors_le_seventeen_of_le_cutoff line 609
  44. theorem OAI.Erdos970.NumberTheoryLean.SquarefreeHarmonic.cutoffSurvivors_le_uniform_log line 617