OAI/NumberTheory/Jacobsthal/Sieve/BuchstabBridge.lean

GitHub source file

79 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos970.ErdosAverageCertificates.buchstabStage line 26
  2. theorem OAI.Erdos970.ErdosAverageCertificates.buchstabStage_zero line 32
  3. theorem OAI.Erdos970.ErdosAverageCertificates.buchstabStage_succ_eq_one line 34
  4. theorem OAI.Erdos970.ErdosAverageCertificates.buchstabStage_succ_eq_integral line 38
  5. theorem OAI.Erdos970.ErdosAverageCertificates.buchstabStage_succ_eq_stage line 43
  6. theorem OAI.Erdos970.ErdosAverageCertificates.buchstabStage_eq_of_le line 67
  7. def OAI.Erdos970.ErdosAverageCertificates.buchstabAux line 77
  8. def OAI.Erdos970.ErdosAverageCertificates.buchstabFunction line 80
  9. theorem OAI.Erdos970.ErdosAverageCertificates.buchstabAux_eq_stage line 83
  10. theorem OAI.Erdos970.ErdosAverageCertificates.buchstabFunction_eq_aux_div line 97
  11. theorem OAI.Erdos970.ErdosAverageCertificates.buchstabFunction_eq_stage_div line 101
  12. theorem OAI.Erdos970.ErdosAverageCertificates.buchstabAux_eq_one line 106
  13. theorem OAI.Erdos970.ErdosAverageCertificates.buchstabFunction_eq_inv line 110
  14. theorem OAI.Erdos970.ErdosAverageCertificates.mul_buchstabFunction line 115
  15. theorem OAI.Erdos970.ErdosAverageCertificates.buchstabAux_eq_one_add_integral line 120
  16. theorem OAI.Erdos970.ErdosAverageCertificates.mul_buchstabFunction_eq_one_add_integral line 144
  17. def OAI.Erdos970.ErdosAverageCertificates.buchstabStageIntegrand line 149
  18. theorem OAI.Erdos970.ErdosAverageCertificates.integral_buchstabStageIntegrand_eq line 152
  19. theorem OAI.Erdos970.ErdosAverageCertificates.continuous_buchstabStage line 162
  20. theorem OAI.Erdos970.ErdosAverageCertificates.continuousOn_buchstabAux line 197
  21. theorem OAI.Erdos970.ErdosAverageCertificates.continuousOn_buchstabFunction line 212
  22. def OAI.Erdos970.ErdosAverageCertificates.buchstabContinuousExtension line 220
  23. theorem OAI.Erdos970.ErdosAverageCertificates.continuous_buchstabContinuousExtension line 223
  24. theorem OAI.Erdos970.ErdosAverageCertificates.integral_buchstabContinuousExtension_eq line 232
  25. theorem OAI.Erdos970.ErdosAverageCertificates.hasDerivAt_buchstabAux line 241
  26. theorem OAI.Erdos970.ErdosAverageCertificates.hasDerivAt_mul_buchstabFunction line 265
  27. theorem OAI.Erdos970.ErdosAverageCertificates.hasDerivAt_buchstabFunction line 273
  28. theorem OAI.Erdos970.ErdosAverageCertificates.buchstabStage_nonneg line 287
  29. theorem OAI.Erdos970.ErdosAverageCertificates.buchstabStage_one_le line 301
  30. theorem OAI.Erdos970.ErdosAverageCertificates.buchstabAux_one_le line 315
  31. theorem OAI.Erdos970.ErdosAverageCertificates.buchstabFunction_nonneg line 321
  32. theorem OAI.Erdos970.ErdosAverageCertificates.inv_le_buchstabFunction line 326
  33. theorem OAI.Erdos970.ErdosAverageCertificates.buchstabFunction_le_one_induction line 331
  34. theorem OAI.Erdos970.ErdosAverageCertificates.buchstabFunction_le_one line 365
  35. theorem OAI.Erdos970.ErdosAverageCertificates.abs_buchstabFunction_le_one line 372
  36. theorem OAI.Erdos970.ErdosAverageCertificates.norm_deriv_mul_buchstabFunction_le_one line 377
  37. theorem OAI.Erdos970.ErdosAverageCertificates.abs_deriv_buchstabFunction_le_two_div line 383
  38. theorem OAI.Erdos970.ErdosAverageCertificates.abs_buchstabFunction_sub_shift_le_two_div line 397
  39. theorem OAI.Erdos970.ErdosAverageCertificates.abs_deriv_buchstabFunction_le_two_div_mul_sub_one line 417
  40. theorem OAI.Erdos970.ErdosAverageCertificates.continuousOn_deriv_buchstabFunction line 431
  41. theorem OAI.Erdos970.ErdosAverageCertificates.integrableOn_deriv_buchstabFunction line 451
  42. def OAI.Erdos970.ErdosAverageCertificates.buchstabLimit line 477
  43. theorem OAI.Erdos970.ErdosAverageCertificates.tendsto_buchstabFunction_atTop line 480
  44. theorem OAI.Erdos970.ErdosAverageCertificates.buchstabLimit_nonneg line 488
  45. theorem OAI.Erdos970.ErdosAverageCertificates.buchstabLimit_le_one line 493
  46. theorem OAI.Erdos970.ErdosAverageCertificates.abs_buchstabFunction_sub_le_two_div_sub_one line 498
  47. theorem OAI.Erdos970.ErdosAverageCertificates.abs_buchstabFunction_sub_limit_le_two_div_sub_one line 573
  48. theorem OAI.Erdos970.ErdosAverageCertificates.integrableOn_buchstabFunction_sub_limit_div line 586
  49. def OAI.Erdos970.ErdosAverageCertificates.buchstabLaplace line 626
  50. theorem OAI.Erdos970.ErdosAverageCertificates.measurable_buchstabFunction line 629
  51. theorem OAI.Erdos970.ErdosAverageCertificates.integrableOn_buchstabLaplace_integrand line 649
  52. theorem OAI.Erdos970.ErdosAverageCertificates.integrableOn_id_mul_exp_neg_mul line 667
  53. theorem OAI.Erdos970.ErdosAverageCertificates.integrableOn_buchstabLaplace_deriv_integrand line 687
  54. theorem OAI.Erdos970.ErdosAverageCertificates.hasDerivAt_buchstabLaplace line 711
  55. theorem OAI.Erdos970.ErdosAverageCertificates.differentiableOn_buchstabLaplace line 791
  56. theorem OAI.Erdos970.ErdosAverageCertificates.integrableOn_buchstabShift_mul_exp line 797
  57. theorem OAI.Erdos970.ErdosAverageCertificates.integrableOn_mul_buchstab_mul_exp_deriv line 817
  58. theorem OAI.Erdos970.ErdosAverageCertificates.integral_mul_buchstab_mul_exp_Ioi_two line 831
  59. theorem OAI.Erdos970.ErdosAverageCertificates.integral_buchstabShift_mul_exp_Ioi_two line 923
  60. theorem OAI.Erdos970.ErdosAverageCertificates.integral_mul_buchstab_mul_exp_Ioi_one line 960
  61. theorem OAI.Erdos970.ErdosAverageCertificates.buchstabLaplace_nonneg line 1005
  62. theorem OAI.Erdos970.ErdosAverageCertificates.buchstabLaplace_ode line 1012
  63. theorem OAI.Erdos970.ErdosAverageCertificates.tendsto_buchstabLaplace_atTop line 1022
  64. theorem OAI.Erdos970.ErdosAverageCertificates.one_add_buchstabLaplace_eq_exponentialIntegral line 1047
  65. theorem OAI.Erdos970.ErdosAverageCertificates.buchstabLimit_eq_exp_neg_eulerMascheroniConstant line 1055
  66. theorem OAI.Erdos970.ErdosAverageCertificates.abs_buchstabFunction_sub_exp_neg_eulerMascheroni_le line 1078
  67. theorem OAI.Erdos970.ErdosAverageCertificates.integrableOn_buchstabFunction_sub_exp_neg_eulerMascheroni_div line 1085
  68. theorem OAI.Erdos970.ErdosAverageCertificates.tendsto_mul_buchstabLaplace_zero_right line 1092
  69. theorem OAI.Erdos970.NumberTheoryLean.BuchstabBridge.plus_eq_buchstabAux line 1114
  70. theorem OAI.Erdos970.NumberTheoryLean.BuchstabBridge.plus_div_eq_buchstabFunction line 1133
  71. theorem OAI.Erdos970.NumberTheoryLean.BuchstabBridge.pair_sum_eq_buchstab line 1138
  72. def OAI.Erdos970.NumberTheoryLean.BuchstabBridge.sieveA line 1146
  73. theorem OAI.Erdos970.NumberTheoryLean.BuchstabBridge.sieveA_pos line 1148
  74. theorem OAI.Erdos970.NumberTheoryLean.BuchstabBridge.sieveA_gt_two line 1150
  75. theorem OAI.Erdos970.NumberTheoryLean.BuchstabBridge.sieveA_normalization line 1157
  76. theorem OAI.Erdos970.NumberTheoryLean.BuchstabBridge.normalized_pair_sum_tendsto_two line 1162
  77. theorem OAI.Erdos970.NumberTheoryLean.BuchstabBridge.pair_gap_tendsto_zero line 1171
  78. theorem OAI.Erdos970.NumberTheoryLean.BuchstabBridge.normalized_F_tendsto_one line 1185
  79. theorem OAI.Erdos970.NumberTheoryLean.BuchstabBridge.normalized_f_tendsto_one line 1192