-
Notifications
You must be signed in to change notification settings - Fork 2
Expand file tree
/
Copy pathLongGapsBetweenPrimes.lean
More file actions
4546 lines (4217 loc) · 226 KB
/
Copy pathLongGapsBetweenPrimes.lean
File metadata and controls
4546 lines (4217 loc) · 226 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
/-
Formalization of "Improved Long Gaps Between Primes" by OpenAI.
We prove that, for all sufficiently large X,
G(X) >> log(X) * log(log(X))^2 * log(log(log(log(X))))
/ log(log(log(X)))^2,
where G(X) is the largest gap between consecutive primes not exceeding X.
Here, log denotes the natural logarithm and >> denotes a lower bound up to
a positive multiplicative constant independent of X.
The main results are `short_translates` (Proposition 1.2) and
`long_gap_theorem` (Theorem 1.1). The proof uses weak Mertens estimates,
κ = 1/8, and a larger fixed constant in the auxiliary smoothness cutoff.
Released under Apache 2.0 license as described in the file LICENSE.
SPDX-License-Identifier: Apache-2.0
-/
import Mathlib
namespace LongGapsBetweenPrimes
noncomputable section
/-- The j-fold natural logarithm used in the statement of Theorem 1.1. -/
def iteratedLog (j : ℕ) (x : ℝ) : ℝ := (Real.log^[j]) x
/-- The function on the right hand side of Theorem 1.1, without its constant. -/
def gapScale (x : ℝ) : ℝ :=
Real.log x * (iteratedLog 2 x) ^ 2 * iteratedLog 4 x / (iteratedLog 3 x) ^ 2
/-- Consecutive primes, specified without choosing an enumeration. -/
def ConsecutivePrimes (p q : ℕ) : Prop :=
p.Prime ∧ q.Prime ∧ p < q ∧ ∀ r : ℕ, p < r → r < q → ¬r.Prime
/-- The precise conclusion to be proved. -/
def LongGapTheorem : Prop :=
∃ c : ℝ, 0 < c ∧ ∀ᶠ X : ℝ in Filter.atTop,
∃ p q : ℕ, ConsecutivePrimes p q ∧ (q : ℝ) ≤ X ∧ c * gapScale X ≤ (q - p : ℕ)
/-- The short-translate assertion of Proposition 1.2. -/
def ShortTranslates : Prop :=
∃ δ : ℝ, 0 < δ ∧ δ < 1 / 2 ∧ ∀ᶠ x : ℝ in Filter.atTop,
∀ H : ℕ, x < H → (H : ℝ) ≤ x * (Real.log x) ^ 2 →
∀ S : Finset ℕ, S ⊆ Finset.Icc 1 H → (S.card : ℝ) ≤ δ * x →
∀ b : ℕ, b < primorial ⌊x⌋₊ →
∃ t : ℕ, 1 ≤ t ∧ (t : ℝ) ≤ Real.exp x ∧
∀ s ∈ S, ¬Nat.Prime (b + primorial ⌊x⌋₊ * t + s)
/-- The normalization B in (3.1). -/
def normalizer (P : ℕ) : ℝ :=
∑ d ∈ P.divisors.erase 1, 1 / ((d.totient : ℝ) * Real.log d)
/-- The coefficient a(d) in (3.1). -/
def coefficient (P d : ℕ) : ℝ :=
if d = 1 then 1 else -1 / (normalizer P * Real.log d)
/-- A divisor other than one is greater than one. -/
lemma one_lt_of_mem_divisors_erase_one {P d : ℕ}
(hd : d ∈ P.divisors.erase 1) : 1 < d := by
exact lt_of_le_of_ne (Nat.pos_of_mem_divisors (Finset.mem_of_mem_erase hd))
(Finset.ne_of_mem_erase hd).symm
/-- The normalizer is positive when `P > 1`. -/
lemma normalizer_pos {P : ℕ} (hP : 1 < P) : 0 < normalizer P := by
unfold normalizer
apply Finset.sum_pos
· intro d hd
have hd' := one_lt_of_mem_divisors_erase_one hd
have ht : 0 < (d.totient : ℝ) := by
exact_mod_cast Nat.totient_pos.mpr (by omega : 0 < d)
exact one_div_pos.mpr (mul_pos ht (Real.log_pos (by exact_mod_cast hd')))
· exact ⟨P, Finset.mem_erase.mpr ⟨ne_of_gt hP, Nat.mem_divisors_self P (by omega)⟩⟩
/-- For `P > 1`, coefficients at `d > 1` are negative. -/
lemma coefficient_neg {P d : ℕ} (hP : 1 < P) (hd : 1 < d) :
coefficient P d < 0 := by
rw [coefficient, if_neg (ne_of_gt hd)]
exact div_neg_of_neg_of_pos (by norm_num)
(mul_pos (normalizer_pos hP) (Real.log_pos (by exact_mod_cast hd)))
/-- Exact cancellation, equations (3.2) and (3.5). -/
theorem coefficient_cancellation {P : ℕ} (hP : 1 < P) :
∑ d ∈ P.divisors, coefficient P d / d.totient = 0 := by
have hB : normalizer P ≠ 0 := ne_of_gt (normalizer_pos hP)
have hsum : ∑ d ∈ P.divisors.erase 1, coefficient P d / d.totient =
-(normalizer P)⁻¹ * normalizer P := by
change _ = -(normalizer P)⁻¹ *
∑ d ∈ P.divisors.erase 1, 1 / ((d.totient : ℝ) * Real.log d)
rw [Finset.mul_sum]
apply Finset.sum_congr rfl
intro d hd
simp only [coefficient, if_neg (Finset.ne_of_mem_erase hd)]
ring
rw [← Finset.sum_erase_add _ _ (Nat.one_mem_divisors.mpr (by omega : P ≠ 0)),
hsum]
simp [coefficient, hB]
/-- The omitted terms in (3.11) have positive total mass. -/
theorem partial_cancellation {P : ℕ} (hP : 1 < P)
(E : Finset ℕ) (hE : E ⊆ P.divisors) (h1 : 1 ∈ E) :
∑ d ∈ E, coefficient P d / d.totient =
∑ d ∈ P.divisors \ E, |coefficient P d| / d.totient := by
have hsum := Finset.sum_sdiff hE (f := fun d => coefficient P d / d.totient)
rw [coefficient_cancellation hP] at hsum
rw [eq_neg_of_add_eq_zero_right hsum, ← Finset.sum_neg_distrib]
apply Finset.sum_congr rfl
intro d hd
rcases Finset.mem_sdiff.mp hd with ⟨hd, hdE⟩
have hd1 : d ≠ 1 := by
rintro rfl
exact hdE h1
rw [abs_of_neg (coefficient_neg hP
(one_lt_of_mem_divisors_erase_one (Finset.mem_erase.mpr ⟨hd1, hd⟩))), neg_div]
/-- A divisor subsum containing one has nonnegative weighted coefficient sum. -/
lemma partial_cancellation_nonneg {P : ℕ} (hP : 1 < P)
(E : Finset ℕ) (hE : E ⊆ P.divisors) (h1 : 1 ∈ E) :
0 ≤ ∑ d ∈ E, coefficient P d / d.totient := by
rw [partial_cancellation hP E hE h1]
positivity
/-- The local factor as a function of a residue class with specified root. -/
def residueFactor {p : ℕ} (a t : Fin p) : ℝ :=
if t = a then -1 else 1 / ((p : ℝ) - 1)
/-- Sum a constant function with one exceptional value. -/
lemma sum_one_exception {p : ℕ} (a : Fin p) (c d : ℝ) :
(∑ t : Fin p, if t = a then c else d) = c + ((p : ℝ) - 1) * d := by
simp [Finset.sum_ite, Finset.filter_eq', Finset.filter_ne',
Nat.cast_sub (Nat.succ_le_of_lt (Fin.pos a))]
/-- The local mean is zero (Section 3.1). -/
theorem sum_residueFactor {p : ℕ} (hp : 1 < p) (a : Fin p) :
∑ t : Fin p, residueFactor a t = 0 := by
have hp' : (p : ℝ) - 1 ≠ 0 := sub_ne_zero.mpr (by exact_mod_cast ne_of_gt hp)
simp [residueFactor, sum_one_exception, hp']
/-- The local square mean is 1/(p-1), before dividing the sum by p. -/
theorem sum_residueFactor_sq {p : ℕ} (hp : 1 < p) (a : Fin p) :
(∑ t : Fin p, (residueFactor a t) ^ 2) = (p : ℝ) / ((p : ℝ) - 1) := by
have hp' : (p : ℝ) - 1 ≠ 0 := sub_ne_zero.mpr (by exact_mod_cast ne_of_gt hp)
simp only [residueFactor, ite_pow, neg_one_sq, sum_one_exception]
field_simp
ring
/-- Distinct roots have negative covariance, as used in (3.9). -/
theorem sum_residueFactor_mul {p : ℕ} (hp : 1 < p) (a b : Fin p) (hab : a ≠ b) :
(∑ t : Fin p, residueFactor a t * residueFactor b t) =
-(p : ℝ) / ((p : ℝ) - 1) ^ 2 := by
have hmul (t : Fin p) :
residueFactor a t * residueFactor b t =
(1 / ((p : ℝ) - 1)) * (residueFactor a t + residueFactor b t) -
(1 / ((p : ℝ) - 1)) ^ 2 := by
unfold residueFactor
split_ifs with ha hb
· exact (hab (ha.symm.trans hb)).elim
all_goals ring
simp_rw [hmul]
rw [Finset.sum_sub_distrib, ← Finset.mul_sum, Finset.sum_add_distrib,
sum_residueFactor hp a, sum_residueFactor hp b]
simp
ring
/-- For squarefree `d`, its totient is the product of `p - 1` over its prime factors. -/
lemma totient_eq_prod_sub_one_of_squarefree {d : ℕ} (hd : Squarefree d) :
d.totient = ∏ p ∈ d.primeFactors, (p - 1) := by
have h := Nat.totient_mul_prod_primeFactors d
rw [Nat.prod_primeFactors_of_squarefree hd] at h
exact mul_right_cancel₀ hd.ne_zero (h.trans (mul_comm _ _))
/-- A_gamma in Lemma 3.1; A is its value at gamma = 0. -/
def coefficientMoment (P : ℕ) (γ : ℝ) : ℝ :=
∑ d ∈ P.divisors, coefficient P d ^ 2 * (d : ℝ) ^ γ / d.totient
/-- The absolute coefficient moment over nontrivial divisors. -/
def coefficientAbsMoment (P : ℕ) (γ : ℝ) : ℝ :=
∑ d ∈ P.divisors.erase 1, |coefficient P d| * (d : ℝ) ^ γ / d.totient
/-- Expand the coefficient moment at exponent zero. -/
lemma coefficientMoment_zero (P : ℕ) :
coefficientMoment P 0 = ∑ d ∈ P.divisors, coefficient P d ^ 2 / d.totient := by
simp [coefficientMoment]
/-- The divisor one gives a lower bound of one for the coefficient moment. -/
lemma coefficientMoment_ge_one {P : ℕ} (hP : P ≠ 0) (γ : ℝ) :
1 ≤ coefficientMoment P γ := by
have h := Finset.single_le_sum
(f := fun d => coefficient P d ^ 2 * (d : ℝ) ^ γ / d.totient)
(fun d _ => div_nonneg (mul_nonneg (sq_nonneg _) (Real.rpow_nonneg (Nat.cast_nonneg _) _))
(Nat.cast_nonneg _)) (Nat.one_mem_divisors.mpr hP)
simpa [coefficientMoment, coefficient] using h
/-- The exponential increment is at most `x * exp x`. -/
lemma exp_sub_one_le_mul_exp (x : ℝ) : Real.exp x - 1 ≤ x * Real.exp x := by
have h := mul_le_mul_of_nonneg_right (Real.add_one_le_exp (-x)) (Real.exp_nonneg x)
rw [← Real.exp_add, neg_add_cancel, Real.exp_zero] at h
linarith
/-- The power increment is at most `γ * v ^ γ * log v`. -/
lemma rpow_sub_one_le {v γ : ℝ} (hv : 0 < v) :
v ^ γ - 1 ≤ γ * v ^ γ * Real.log v := by
rw [Real.rpow_def_of_pos hv]
nlinarith [exp_sub_one_le_mul_exp (Real.log v * γ)]
/-- A squared coefficient times `log d` equals its normalized absolute value. -/
lemma coefficient_sq_mul_log {P d : ℕ} (hP : 1 < P) (hd : 1 < d) :
coefficient P d ^ 2 * Real.log d = |coefficient P d| / normalizer P := by
rw [abs_of_neg (coefficient_neg hP hd), coefficient, if_neg (ne_of_gt hd)]
have hB := ne_of_gt (normalizer_pos hP)
have hlog := ne_of_gt (Real.log_pos (by exact_mod_cast hd : (1 : ℝ) < d))
field_simp
/-- Control the change in the squared moment by the absolute moment. -/
lemma coefficientMoment_sub_le {P : ℕ} (hP : 1 < P) (γ : ℝ) :
coefficientMoment P γ - coefficientMoment P 0 ≤
(γ / normalizer P) * coefficientAbsMoment P γ := by
rw [coefficientMoment, coefficientMoment_zero, ← Finset.sum_sub_distrib,
← Finset.sum_erase_add _ _ (Nat.one_mem_divisors.mpr (by omega : P ≠ 0))]
simp only [Nat.cast_one, Real.one_rpow, Nat.totient_one, mul_one, div_one,
sub_self, add_zero]
unfold coefficientAbsMoment
rw [Finset.mul_sum]
apply Finset.sum_le_sum
intro d hd
have hd' := one_lt_of_mem_divisors_erase_one hd
calc
coefficient P d ^ 2 * (d : ℝ) ^ γ / d.totient -
coefficient P d ^ 2 / d.totient =
coefficient P d ^ 2 * ((d : ℝ) ^ γ - 1) / d.totient := by ring
_ ≤ coefficient P d ^ 2 * (γ * (d : ℝ) ^ γ * Real.log d) / d.totient :=
div_le_div_of_nonneg_right
(mul_le_mul_of_nonneg_left
(rpow_sub_one_le (by exact_mod_cast (zero_lt_one.trans hd'))) (sq_nonneg _))
(Nat.cast_nonneg _)
_ = (coefficient P d ^ 2 * Real.log d) * (γ * (d : ℝ) ^ γ) / d.totient := by ring
_ = (γ / normalizer P) * (|coefficient P d| * (d : ℝ) ^ γ / d.totient) := by
rw [coefficient_sq_mul_log hP hd']
ring
/-- Rankin's tail estimate, in the finite form needed for (3.10). -/
theorem moment_tail_le {α : Type*} (s : Finset α) (f v : α → ℝ) (D β : ℝ)
(hD : 0 < D) (hβ : 0 ≤ β) (hf : ∀ a ∈ s, 0 ≤ f a)
(hv : ∀ a ∈ s, 0 ≤ v a) :
(∑ a ∈ s.filter (fun a => D < v a), f a) ≤
D ^ (-β) * ∑ a ∈ s, f a * (v a) ^ β := by
rw [Real.rpow_neg hD.le, ← div_eq_inv_mul]
apply (le_div_iff₀ (Real.rpow_pos_of_pos hD β)).mpr
rw [Finset.sum_mul]
calc
_ ≤ ∑ a ∈ s.filter (fun a => D < v a), f a * (v a) ^ β := by
apply Finset.sum_le_sum
intro a ha
obtain ⟨has, hav⟩ := Finset.mem_filter.mp ha
exact mul_le_mul_of_nonneg_left
(Real.rpow_le_rpow hD.le hav.le hβ) (hf a has)
_ ≤ _ := Finset.sum_le_sum_of_subset_of_nonneg (Finset.filter_subset _ _)
(fun a ha _ => mul_nonneg (hf a ha) (Real.rpow_nonneg (hv a ha) _))
/-- Divisors regarded as a finite index type. -/
abbrev DivisorIndex (P : ℕ) := {d : ℕ // d ∈ P.divisors}
/-- Tuples of `k` divisors of `P`. -/
abbrev DivisorTuple (P k : ℕ) := Fin k → DivisorIndex P
/-- The product of the divisors in a tuple. -/
def tupleProduct {P k : ℕ} (r : DivisorTuple P k) : ℕ := ∏ i, (r i).val
/-- The common truncated region R_k of (3.3). -/
def tupleRegion (P k : ℕ) (D : ℝ) : Finset (DivisorTuple P k) := by
classical
exact Finset.univ.filter fun r =>
(∀ i j, i ≠ j → Nat.Coprime (r i).val (r j).val) ∧ (tupleProduct r : ℝ) ≤ D
/-- The diagonal mass attached to one tuple in (3.9). -/
def tupleMass {P k : ℕ} (r : DivisorTuple P k) : ℝ :=
∏ i, coefficient P (r i).val ^ 2 / ((r i).val.totient : ℝ)
/-- The diagonal mass of a divisor tuple is nonnegative. -/
lemma tupleMass_nonneg {P k : ℕ} (r : DivisorTuple P k) : 0 ≤ tupleMass r := by
unfold tupleMass
positivity
/-- Rewrite a sum over divisor indices as a sum over the divisor finset. -/
lemma sum_divisorIndex (P : ℕ) (f : ℕ → ℝ) :
(∑ d : DivisorIndex P, f d.val) = ∑ d ∈ P.divisors, f d := by
exact Finset.sum_attach P.divisors f
/-- The total tuple mass is the `k`th power of the zero coefficient moment. -/
lemma sum_tupleMass (P k : ℕ) :
(∑ r : DivisorTuple P k, tupleMass r) = coefficientMoment P 0 ^ k := by
classical
unfold tupleMass
rw [← Fintype.prod_sum (fun (_ : Fin k) (d : DivisorIndex P) =>
coefficient P d.val ^ 2 / (d.val.totient : ℝ))]
rw [sum_divisorIndex P (fun d => coefficient P d ^ 2 / (d.totient : ℝ)),
← coefficientMoment_zero]
simp
/-- The tilted tuple mass factors as a power of the coefficient moment. -/
lemma sum_tupleMass_mul_rpow (P k : ℕ) (γ : ℝ) :
(∑ r : DivisorTuple P k, tupleMass r * (tupleProduct r : ℝ) ^ γ) =
coefficientMoment P γ ^ k := by
classical
unfold tupleMass tupleProduct
simp_rw [Nat.cast_prod,
← Real.finsetProd_rpow _ _ (fun _ _ => Nat.cast_nonneg _),
← Finset.prod_mul_distrib, div_mul_eq_mul_div]
rw [← Fintype.prod_sum (fun (_ : Fin k) (d : DivisorIndex P) =>
coefficient P d.val ^ 2 * (d.val : ℝ) ^ γ / (d.val.totient : ℝ))]
rw [sum_divisorIndex P (fun d => coefficient P d ^ 2 * (d : ℝ) ^ γ / d.totient)]
simp [coefficientMoment]
/-- The first inequality in (3.10), with no asymptotic assumptions. -/
theorem diagonal_tail_le (P k : ℕ) {D β : ℝ} (hD : 0 < D) (hβ : 0 ≤ β) :
(∑ r ∈ (Finset.univ : Finset (DivisorTuple P k)).filter
(fun r => D < (tupleProduct r : ℝ)), tupleMass r) ≤
D ^ (-β) * coefficientMoment P β ^ k := by
classical
simpa only [sum_tupleMass_mul_rpow] using
moment_tail_le Finset.univ tupleMass (fun r : DivisorTuple P k => (tupleProduct r : ℝ))
D β hD hβ (fun r _ => tupleMass_nonneg r) (fun r _ => Nat.cast_nonneg _)
/-- Convert an additive bound into an exponential bound on powers. -/
lemma pow_le_mul_exp {A B t : ℝ} (hA : 1 ≤ A) (hB : 0 ≤ B)
(ht : 0 ≤ t) (hBA : B ≤ A + t) (k : ℕ) :
B ^ k ≤ A ^ k * Real.exp ((k : ℝ) * t) := by
have hbase : B ≤ A * Real.exp t := by
have he := Real.add_one_le_exp t
nlinarith [mul_nonneg (sub_nonneg.mpr hA) ht,
mul_le_mul_of_nonneg_left he (by linarith : 0 ≤ A)]
calc
B ^ k ≤ (A * Real.exp t) ^ k := pow_le_pow_left₀ hB hbase k
_ = A ^ k * Real.exp ((k : ℝ) * t) := by rw [mul_pow, Real.exp_nat_mul]
/-- Bound powers of a tilted coefficient moment relative to the zero moment. -/
lemma coefficientMoment_pow_le {P : ℕ} (hP : 1 < P) {C γ : ℝ}
(hC : 0 ≤ C) (hγ : 0 ≤ γ)
(hM : coefficientAbsMoment P γ ≤ C * normalizer P) (k : ℕ) :
coefficientMoment P γ ^ k ≤
coefficientMoment P 0 ^ k * Real.exp ((k : ℝ) * C * γ) := by
have hP0 : P ≠ 0 := by omega
have hB := normalizer_pos hP
have hbound : coefficientMoment P γ - coefficientMoment P 0 ≤ C * γ := by
calc
_ ≤ γ / normalizer P * coefficientAbsMoment P γ := coefficientMoment_sub_le hP γ
_ ≤ γ / normalizer P * (C * normalizer P) :=
mul_le_mul_of_nonneg_left hM (div_nonneg hγ hB.le)
_ = C * γ := by field_simp
simpa [mul_assoc] using pow_le_mul_exp (coefficientMoment_ge_one hP0 0)
(zero_le_one.trans (coefficientMoment_ge_one hP0 γ)) (mul_nonneg hC hγ)
(by linarith : coefficientMoment P γ ≤ coefficientMoment P 0 + C * γ) k
/-- The elementary passage from a prime-free interval to consecutive primes.
Bertrand's postulate supplies the upper endpoint bound used in Section 2. -/
theorem consecutivePrimes_of_composite_interval {N H : ℕ} (hN : 2 ≤ N)
(hcomposite : ∀ n : ℕ, N < n → n ≤ N + H → ¬n.Prime) :
∃ p q : ℕ, ConsecutivePrimes p q ∧ p ≤ N ∧ N + H < q ∧ q ≤ 2 * N ∧ H < q - p := by
have hex := Nat.exists_prime_lt_and_le_two_mul N (by omega)
let q := Nat.find hex
obtain ⟨hq, hNq, hqN⟩ : q.Prime ∧ N < q ∧ q ≤ 2 * N := Nat.find_spec hex
let p := Nat.findGreatest Nat.Prime N
have hp : p.Prime := Nat.findGreatest_spec hN Nat.prime_two
have hpN : p ≤ N := Nat.findGreatest_le N
have hNHq : N + H < q := by
by_contra! h
exact hcomposite q hNq h hq
refine ⟨p, q, ⟨hp, hq, hpN.trans_lt hNq, ?_⟩, hpN, hNHq, hqN, by omega⟩
intro r hpr hrq hr
by_cases hrN : r ≤ N
· exact Nat.findGreatest_is_greatest hpr hrN hr
· exact Nat.find_min hex hrq ⟨hr, by omega, by omega⟩
/-- The initial zero-residue sieve leaves only primes and z-smooth integers. -/
theorem prime_or_smooth_of_survives {n H : ℕ} {x w z : ℝ}
(hn : 1 ≤ n) (hnH : n ≤ H) (hx : 0 < x) (hsmall : 2 * (H : ℝ) < x * w)
(hsurvives : ∀ p : ℕ, p.Prime → ((p : ℝ) ≤ w ∨ (z < p ∧ (p : ℝ) ≤ x / 2)) → ¬p ∣ n) :
n.Prime ∨ ∀ p : ℕ, p.Prime → p ∣ n → (p : ℝ) ≤ z := by
by_cases hprime : n.Prime
· exact Or.inl hprime
right
intro p hp hpn
by_contra! hpz
have hpbig : x / 2 < (p : ℝ) := by
by_contra! hpx
exact hsurvives p hp (Or.inr ⟨hpz, hpx⟩) hpn
obtain ⟨k, rfl⟩ := hpn
have hk1 : k ≠ 1 := by
intro hk
simp [hk, hp] at hprime
obtain ⟨q, hq, hqk⟩ := Nat.exists_prime_and_dvd hk1
have hqn : q ∣ p * k := dvd_mul_of_dvd_right hqk p
have hqbig : w < (q : ℝ) := by
by_contra! hqw
exact hsurvives q hq (Or.inl hqw) hqn
have hkn : q ≤ k := Nat.le_of_dvd (Nat.pos_of_ne_zero (by rintro rfl; simp at hn)) hqk
have hpkH : (p : ℝ) * k ≤ H := by exact_mod_cast hnH
have hqk' : (q : ℝ) ≤ k := by exact_mod_cast hkn
have hp0 : 0 ≤ (p : ℝ) := Nat.cast_nonneg p
have hq0 : 0 < (q : ℝ) := by exact_mod_cast hq.pos
nlinarith [mul_le_mul_of_nonneg_left hqk' hp0,
mul_lt_mul_of_pos_right hpbig hq0,
mul_lt_mul_of_pos_left hqbig hx]
/-- Elements of `S` avoiding the selected residue classes. -/
def survivors (S ps : Finset ℕ) (a : ℕ → ℕ) : Finset ℕ :=
S.filter fun n => ∀ p ∈ ps, n % p ≠ a p
/-- The greedy product bound in (2.1), before applying Mertens' estimate. -/
theorem greedy_residue_classes (S ps : Finset ℕ) (hpos : ∀ p ∈ ps, 0 < p) :
∃ a : ℕ → ℕ, (∀ p ∈ ps, a p < p) ∧
((survivors S ps a).card : ℝ) ≤ (S.card : ℝ) * ∏ p ∈ ps, (1 - 1 / (p : ℝ)) := by
classical
induction ps using Finset.induction_on with
| empty =>
exact ⟨fun _ => 0, by simp, by simp [survivors]⟩
| @insert p ps hp ih =>
have hp0 : 0 < p := hpos p (Finset.mem_insert_self p ps)
have hpR : 0 < (p : ℝ) := by exact_mod_cast hp0
obtain ⟨a, ha, hcard⟩ := ih (fun q hq => hpos q (Finset.mem_insert_of_mem hq))
let T := survivors S ps a
have hsum : (∑ r ∈ Finset.range p,
((T.filter fun n => n % p = r).card : ℝ)) = T.card := by
exact_mod_cast (Finset.card_eq_sum_card_fiberwise
(f := fun n => n % p) (s := T) (t := Finset.range p)
(by intro n _; exact Finset.mem_range.mpr (Nat.mod_lt n hp0))).symm
obtain ⟨r, hr, hlarge⟩ : ∃ r ∈ Finset.range p,
(T.card : ℝ) / p ≤ ((T.filter fun n => n % p = r).card : ℝ) := by
apply Finset.exists_le_of_sum_le (Finset.nonempty_range_iff.mpr hp0.ne')
rw [hsum]
simp only [Finset.sum_const, Finset.card_range, nsmul_eq_mul]
exact le_of_eq (by field_simp)
have hsplit : ((T.filter fun n => n % p = r).card : ℝ) +
((T.filter fun n => n % p ≠ r).card : ℝ) = T.card := by
exact_mod_cast T.card_filter_add_card_filter_not (fun n => n % p = r)
have hstep : ((T.filter fun n => n % p ≠ r).card : ℝ) ≤
(T.card : ℝ) * (1 - 1 / (p : ℝ)) := by
rw [div_eq_mul_inv] at hlarge
simp only [one_div]
nlinarith
refine ⟨Function.update a p r, ?_, ?_⟩
· intro q hq
rcases Finset.mem_insert.mp hq with rfl | hq
· simpa using Finset.mem_range.mp hr
· simpa [Function.update_of_ne (ne_of_mem_of_not_mem hq hp)] using ha q hq
· have hsurvivors : survivors S (insert p ps) (Function.update a p r) =
T.filter (fun n => n % p ≠ r) := by
have hupdate : ∀ q ∈ ps, Function.update a p r q = a q := by
intro q hq
exact Function.update_of_ne (ne_of_mem_of_not_mem hq hp) r a
ext n
simp (config := { contextual := true }) only [survivors, Finset.mem_filter,
Finset.mem_insert, forall_eq_or_imp, Function.update_self, T, hupdate]
tauto
rw [hsurvivors, Finset.prod_insert hp]
calc
_ ≤ (T.card : ℝ) * (1 - 1 / (p : ℝ)) := hstep
_ ≤ ((S.card : ℝ) * ∏ q ∈ ps, (1 - 1 / (q : ℝ))) *
(1 - 1 / (p : ℝ)) :=
mul_le_mul_of_nonneg_right hcard (by
have : (1 : ℝ) ≤ p := by exact_mod_cast hp0
exact sub_nonneg.mpr ((div_le_one hpR).mpr this))
_ = _ := by ring
/-- A symmetric matrix is controlled by its absolute row sums. This is the
2|ab| ≤ a²+b² argument invoked in the proof of (3.9). -/
theorem abs_quadratic_form_le_rows {ι : Type*} [Fintype ι]
(c : ι → ℝ) (K : ι → ι → ℝ) (hK : ∀ i j, |K i j| = |K j i|) :
|∑ i, ∑ j, c i * c j * K i j| ≤ ∑ i, c i ^ 2 * ∑ j, |K i j| := by
calc
|∑ i, ∑ j, c i * c j * K i j| ≤ ∑ i, ∑ j, |c i * c j * K i j| :=
(Finset.abs_sum_le_sum_abs _ _).trans
(Finset.sum_le_sum fun i _ => Finset.abs_sum_le_sum_abs _ _)
_ ≤ ∑ i, ∑ j, (c i ^ 2 + c j ^ 2) / 2 * |K i j| := by
apply Finset.sum_le_sum
intro i _
apply Finset.sum_le_sum
intro j _
rw [abs_mul, abs_mul]
apply mul_le_mul_of_nonneg_right _ (abs_nonneg _)
nlinarith [sq_nonneg (|c i| - |c j|), sq_abs (c i), sq_abs (c j)]
_ = ∑ i, c i ^ 2 * ∑ j, |K i j| := by
simp_rw [add_div, add_mul, Finset.sum_add_distrib]
rw [Finset.sum_comm (f := fun i j => c j ^ 2 / 2 * |K i j|)]
simp_rw [← hK, ← Finset.mul_sum, ← Finset.sum_add_distrib, ← add_mul, add_halves]
/-- Row sums away from the diagonal bound the quadratic error from the identity. -/
lemma quadratic_form_near_diagonal {ι : Type*} [Fintype ι] [DecidableEq ι]
(c : ι → ℝ) (K : ι → ι → ℝ) (ε : ℝ)
(hsym : ∀ i j, K i j = K j i) (hdiag : ∀ i, K i i = 1)
(hrow : ∀ i, (∑ j, if j = i then 0 else |K i j|) ≤ ε) :
|(∑ i, ∑ j, c i * c j * K i j) - ∑ i, c i ^ 2| ≤ ε * ∑ i, c i ^ 2 := by
let L : ι → ι → ℝ := fun i j => if j = i then 0 else K i j
have hL (i j : ι) : c i * c j * L i j =
c i * c j * K i j - if j = i then c i ^ 2 else 0 := by
by_cases hij : j = i <;> simp [L, hij, hdiag, pow_two]
calc
_ = |∑ i, ∑ j, c i * c j * L i j| := by
simp_rw [hL, Finset.sum_sub_distrib]
simp
_ ≤ ∑ i, c i ^ 2 * ∑ j, |L i j| :=
abs_quadratic_form_le_rows c L (by
intro i j
simp only [L, eq_comm, hsym i j])
_ ≤ ∑ i, c i ^ 2 * ε := by
apply Finset.sum_le_sum
intro i _
apply mul_le_mul_of_nonneg_left _ (sq_nonneg _)
simpa only [L, apply_ite abs, abs_zero] using hrow i
_ = _ := by rw [← Finset.sum_mul, mul_comm]
/-- The product of selected local basis functions over all coordinates. -/
def productBasis {α : Type*} [Fintype α] {Ω J : α → Type*}
(f : (p : α) → J p → Ω p → ℝ) (σ : (p : α) → J p) (t : (p : α) → Ω p) : ℝ :=
∏ p, f p (σ p) (t p)
/-- The residue factor has mean zero. -/
lemma average_residueFactor {p : ℕ} (hp : 1 < p) (a : Fin p) :
Finset.expect Finset.univ (residueFactor a) = 0 := by
simp [Finset.expect, sum_residueFactor hp]
/-- The residue factor has second moment `1 / (p - 1)`. -/
lemma average_residueFactor_sq {p : ℕ} (hp : 1 < p) (a : Fin p) :
Finset.expect Finset.univ (fun t => residueFactor a t ^ 2) = 1 / ((p : ℝ) - 1) := by
have hp0 : p ≠ 0 := by omega
simp [Finset.expect_eq_sum_div_card, sum_residueFactor_sq hp, div_eq_mul_inv,
mul_right_comm, hp0]
/-- Distinct residue factors have covariance `-1 / (p - 1)^2`. -/
lemma average_residueFactor_mul {p : ℕ} (hp : 1 < p) (a b : Fin p) (hab : a ≠ b) :
Finset.expect Finset.univ (fun t => residueFactor a t * residueFactor b t) =
-1 / ((p : ℝ) - 1) ^ 2 := by
have hp0 : p ≠ 0 := by omega
simp [Finset.expect_eq_sum_div_card, sum_residueFactor_mul hp a b hab,
div_eq_mul_inv, mul_right_comm, hp0]
/-- The constant function and residue factors scaled to have variance one. -/
def localBasis {p k : ℕ} (root : Fin k → Fin p) (i : Option (Fin k)) (t : Fin p) : ℝ :=
match i with
| none => 1
| some j => Real.sqrt ((p : ℝ) - 1) * residueFactor (root j) t
/-- The Gram kernel for the normalized local basis. -/
def localKernel (p : ℕ) {k : ℕ} (i j : Option (Fin k)) : ℝ :=
match i, j with
| none, none => 1
| none, some _ => 0
| some _, none => 0
| some a, some b => if a = b then 1 else -1 / ((p : ℝ) - 1)
/-- The local Gram matrix, with the nonconstant factors normalized to variance one. -/
theorem average_localBasis_mul {p k : ℕ} (hp : 1 < p) (root : Fin k → Fin p)
(hroot : Function.Injective root) (i j : Option (Fin k)) :
Finset.expect Finset.univ (fun t => localBasis root i t * localBasis root j t) =
localKernel p i j := by
classical
have hpR : 0 < (p : ℝ) - 1 := sub_pos.mpr (by exact_mod_cast hp)
have : NeZero p := ⟨by omega⟩
cases i with
| none =>
cases j <;>
simp [localBasis, localKernel, ← Finset.mul_expect, average_residueFactor hp,
Finset.expect_const Finset.univ_nonempty]
| some a =>
cases j with
| none =>
simp [localBasis, localKernel, ← Finset.mul_expect, average_residueFactor hp]
| some b =>
simp_rw [localBasis, mul_mul_mul_comm (Real.sqrt _) _ (Real.sqrt _) _]
rw [← Finset.mul_expect, ← pow_two, Real.sq_sqrt hpR.le]
by_cases hab : a = b
· subst b
simp only [localKernel, ← pow_two, average_residueFactor_sq hp]
exact mul_one_div_cancel (ne_of_gt hpR)
· rw [average_residueFactor_mul hp _ _ (hroot.ne hab)]
simp only [localKernel, if_neg hab]
field_simp
/-- The absolute row sum of the local Gram kernel. -/
def localRow (p k : ℕ) (i : Option (Fin k)) : ℝ :=
match i with
| none => 1
| some _ => 1 + ((k : ℝ) - 1) / ((p : ℝ) - 1)
/-- The local Gram kernel is symmetric. -/
lemma localKernel_symm (p : ℕ) {k : ℕ} (i j : Option (Fin k)) :
localKernel p i j = localKernel p j i := by
cases i <;> cases j <;> simp [localKernel, eq_comm]
/-- The local Gram kernel has diagonal entries equal to one. -/
lemma localKernel_diag (p : ℕ) {k : ℕ} (i : Option (Fin k)) :
localKernel p i i = 1 := by cases i <;> simp [localKernel]
/-- Summing the absolute local kernel entries gives `localRow`. -/
lemma sum_abs_localKernel {p k : ℕ} (hp : 1 < p) (i : Option (Fin k)) :
(∑ j, |localKernel p i j|) = localRow p k i := by
have hpR : 0 ≤ (p : ℝ) - 1 := sub_nonneg.mpr (by exact_mod_cast hp.le)
cases i with
| none => simp [localKernel, localRow, Fintype.sum_option]
| some a =>
simp only [Fintype.sum_option, localKernel, abs_zero, zero_add, apply_ite abs,
abs_one, abs_div, abs_neg, abs_of_nonneg hpR]
simpa [localRow, eq_comm, div_eq_mul_inv] using
sum_one_exception a 1 (1 / ((p : ℝ) - 1))
/-- The product of local Gram kernels over all coordinates. -/
def productKernel {α : Type*} [Fintype α] (size : α → ℕ) {k : ℕ}
(σ τ : α → Option (Fin k)) : ℝ := ∏ p, localKernel (size p) (σ p) (τ p)
/-- The product Gram kernel is symmetric. -/
lemma productKernel_symm {α : Type*} [Fintype α] (size : α → ℕ) {k : ℕ}
(σ τ : α → Option (Fin k)) : productKernel size σ τ = productKernel size τ σ := by
exact Finset.prod_congr rfl fun p _ => localKernel_symm (size p) (σ p) (τ p)
/-- The product Gram kernel has diagonal entries equal to one. -/
lemma productKernel_diag {α : Type*} [Fintype α] (size : α → ℕ) {k : ℕ}
(σ : α → Option (Fin k)) : productKernel size σ σ = 1 := by
simp [productKernel, localKernel_diag]
/-- The product of local row sums from the proof of (3.9). -/
theorem sum_abs_productKernel {α : Type*} [Fintype α] [DecidableEq α]
(size : α → ℕ) (hsize : ∀ p, 1 < size p) {k : ℕ} (σ : α → Option (Fin k)) :
(∑ τ, |productKernel size σ τ|) = ∏ p, localRow (size p) k (σ p) := by
simp only [productKernel, Finset.abs_prod]
rw [← Fintype.prod_sum (fun p (j : Option (Fin k)) =>
|localKernel (size p) (σ p) j|)]
simp_rw [sum_abs_localKernel (hsize _)]
/-- Products of local basis functions have Gram kernel `productKernel`. -/
lemma average_productBasis_localBasis {α : Type*} [Fintype α] [DecidableEq α]
(size : α → ℕ) (hsize : ∀ p, 1 < size p) {k : ℕ}
(root : (p : α) → Fin k → Fin (size p)) (hroot : ∀ p, Function.Injective (root p))
(σ τ : α → Option (Fin k)) :
Finset.expect Finset.univ (fun t => productBasis (fun p => localBasis (root p)) σ t *
productBasis (fun p => localBasis (root p)) τ t) = productKernel size σ τ := by
classical
simp only [productBasis, ← Finset.prod_mul_distrib]
rw [Finset.expect_eq_sum_div_card, Finset.card_univ, Fintype.card_pi,
Nat.cast_prod, ← Fintype.prod_sum (fun p t =>
localBasis (root p) (σ p) t * localBasis (root p) (τ p) t),
← Finset.prod_div_distrib]
exact Finset.prod_congr rfl fun p _ =>
(Finset.expect_eq_sum_div_card _ _).symm.trans
(average_localBasis_mul (hsize p) (root p) (hroot p) (σ p) (τ p))
/-- Coordinates assigned to a nonconstant local basis function. -/
def assignmentSupport {α : Type*} [Fintype α] {k : ℕ}
(σ : α → Option (Fin k)) : Finset α := Finset.univ.filter fun p => (σ p).isSome
/-- The product of coordinate sizes on an assignment's support. -/
def assignmentProduct {α : Type*} [Fintype α] (size : α → ℕ) {k : ℕ}
(σ : α → Option (Fin k)) : ℕ := ∏ p ∈ assignmentSupport σ, size p
/-- The cutoff controls the row sums uniformly, independently of the
number of auxiliary primes in P. -/
theorem assignment_row_bound {α : Type*} [Fintype α]
(size : α → ℕ) {k : ℕ} (hk : 1 ≤ k) (σ : α → Option (Fin k))
{z D : ℝ} (hz : 1 < z) (hsize : ∀ p, z ≤ (size p : ℝ))
(hcut : (assignmentProduct size σ : ℝ) ≤ D) :
(∏ p, localRow (size p) k (σ p)) ≤
Real.exp ((k : ℝ) * Real.log D / ((z - 1) * Real.log z)) := by
classical
have hz0 : 0 < z := zero_lt_one.trans hz
have hz1 : 0 < z - 1 := sub_pos.mpr hz
have hk1 : 0 ≤ (k : ℝ) - 1 := sub_nonneg.mpr (by exact_mod_cast hk)
have hpos (p : α) : 0 < (size p : ℝ) := hz0.trans_le (hsize p)
have hlog : ((assignmentSupport σ).card : ℝ) * Real.log z ≤ Real.log D := by
calc
_ = ∑ p ∈ assignmentSupport σ, Real.log z := by simp
_ ≤ ∑ p ∈ assignmentSupport σ, Real.log (size p) :=
Finset.sum_le_sum fun p _ => Real.log_le_log hz0 (hsize p)
_ = Real.log (assignmentProduct size σ) := by
rw [assignmentProduct, Nat.cast_prod, Real.log_prod (fun p _ => (hpos p).ne')]
_ ≤ Real.log D := Real.log_le_log (by
rw [assignmentProduct, Nat.cast_prod]
exact Finset.prod_pos fun p _ => hpos p) hcut
calc
(∏ p, localRow (size p) k (σ p)) =
∏ p ∈ assignmentSupport σ, (1 + ((k : ℝ) - 1) / ((size p : ℝ) - 1)) := by
simp only [assignmentSupport, Finset.prod_filter]
apply Finset.prod_congr rfl
intro p _
cases σ p <;> simp [localRow]
_ ≤ ∏ _ ∈ assignmentSupport σ, Real.exp ((k : ℝ) / (z - 1)) := by
apply Finset.prod_le_prod
· intro p _
exact add_nonneg zero_le_one
(div_nonneg hk1 (hz1.le.trans (sub_le_sub_right (hsize p) 1)))
· intro p _
calc
_ ≤ 1 + (k : ℝ) / (z - 1) := add_le_add (le_refl 1)
(div_le_div₀ (Nat.cast_nonneg k) (sub_le_self _ zero_le_one) hz1
(sub_le_sub_right (hsize p) 1))
_ ≤ Real.exp ((k : ℝ) / (z - 1)) := by
simpa [add_comm] using Real.add_one_le_exp ((k : ℝ) / (z - 1))
_ = Real.exp (((assignmentSupport σ).card : ℝ) * ((k : ℝ) / (z - 1))) := by
simp [Real.exp_nat_mul]
_ ≤ _ := by
apply Real.exp_le_exp.mpr
have hcount := (le_div_iff₀ (Real.log_pos hz)).mpr hlog
have hbound := mul_le_mul_of_nonneg_right hcount
(div_nonneg (Nat.cast_nonneg k) hz1.le)
calc
_ ≤ Real.log D / Real.log z * ((k : ℝ) / (z - 1)) := hbound
_ = _ := by
simp only [div_eq_mul_inv, mul_inv_rev]
ring
/-- The indicator of the residue class `a` modulo `m`. -/
def residueIndicator (m a n : ℕ) : ℝ := if n % m = a then 1 else 0
/-- The error of counting one congruence class is at most one. -/
theorem residue_count_error_le_one {m a : ℕ} (ha : a < m) (T : ℕ) :
|(∑ n ∈ Finset.range T, residueIndicator m a n) - (T : ℝ) / m| ≤ 1 := by
have hlo : ((T / m : ℕ) : ℝ) ≤ (T : ℝ) / m := Nat.cast_div_le
have hhi : (T : ℝ) / m < ((T / m : ℕ) : ℝ) + 1 := by
simpa only [Nat.floor_div_natCast, Nat.floor_natCast] using Nat.lt_floor_add_one ((T : ℝ) / m)
have hcount := congrArg (fun n : ℕ => (n : ℝ))
(Nat.count_modEq_card T (by omega : 0 < m) a)
simp only [Nat.count_eq_card_filter_range, Nat.ModEq, Nat.mod_eq_of_lt ha,
Nat.cast_add, Nat.cast_ite, Nat.cast_one, Nat.cast_zero] at hcount
simp only [residueIndicator, Finset.sum_boole]
rw [hcount]
split_ifs <;> rw [abs_le] <;> constructor <;> linarith
/-- A residue class has frequency error at most `1 / T` on an interval of length `T`. -/
lemma residue_average_error {m a T : ℕ} (ha : a < m) (hT : 0 < T) :
|(∑ n ∈ Finset.range T, residueIndicator m a n) / (T : ℝ) - 1 / (m : ℝ)| ≤
1 / (T : ℝ) := by
have hTr : (0 : ℝ) < T := by exact_mod_cast hT
have he : (∑ n ∈ Finset.range T, residueIndicator m a n) / (T : ℝ) - 1 / (m : ℝ) =
((∑ n ∈ Finset.range T, residueIndicator m a n) - (T : ℝ) / m) / T := by
field_simp [ne_of_gt hTr]
rw [he, abs_div, abs_of_pos hTr]
exact div_le_div_of_nonneg_right (residue_count_error_le_one ha T) hTr.le
/-- A weighted union bound, stated without a probability-space interface. -/
theorem weighted_union_bound {Ω ι : Type*} [Fintype Ω] [Fintype ι]
(w : Ω → ℝ) (event : ι → Ω → Prop) [∀ i, DecidablePred (event i)]
(hw : ∀ t, 0 ≤ w t) :
(∑ t, w t * if ∃ i, event i t then 1 else 0) ≤
∑ i, ∑ t, w t * if event i t then 1 else 0 := by
classical
rw [Finset.sum_comm]
apply Finset.sum_le_sum
intro t _
by_cases h : ∃ i, event i t
· obtain ⟨i, hi⟩ := h
simpa [show ∃ j, event j t from ⟨i, hi⟩, hi] using
(Finset.single_le_sum (s := Finset.univ)
(f := fun j => w t * if event j t then 1 else 0)
(fun j _ => by split_ifs <;> simp [hw]) (Finset.mem_univ i))
· simp [not_exists.mp h]
/-- Independence of two marked coordinates under a product of normalized masses. -/
theorem sum_pair_marked_product {ι Ω : Type*} [Fintype ι] [DecidableEq ι]
[Fintype Ω] (w : Ω → ℝ) (hw : ∑ d, w d = 1)
(mark : Ω → Prop) [DecidablePred mark] (i j : ι) (hij : i ≠ j) :
(∑ r : ι → Ω, (∏ ℓ, w (r ℓ)) * if mark (r i) ∧ mark (r j) then 1 else 0) =
(∑ d, w d * if mark d then 1 else 0) ^ 2 := by
classical
calc
_ = ∏ ℓ, ∑ d, w d * if (ℓ = i ∨ ℓ = j) → mark d then 1 else 0 := by
rw [Fintype.prod_sum]
apply Finset.sum_congr rfl
intro r _
rw [Finset.prod_mul_distrib, Finset.prod_boole]
congr 1
simp only [Finset.mem_univ, forall_true_left, or_imp, forall_and, forall_eq]
_ = ∏ ℓ ∈ ({i, j} : Finset ι), ∑ d, w d * if mark d then 1 else 0 := by
rw [← Finset.prod_subset (Finset.subset_univ ({i, j} : Finset ι))]
· simp [hij, Finset.prod_pair hij]
· intro ℓ _ hℓ
simp only [Finset.mem_insert, Finset.mem_singleton, not_or] at hℓ
simp [hℓ.1, hℓ.2, hw]
_ = _ := by simp [Finset.prod_pair hij, pow_two]
/-- The collision estimate for independently chosen divisors: a common mark
in two coordinates costs at most the square of its one-coordinate mass. -/
theorem product_collision_bound {α Ω : Type*} [Fintype α] [Fintype Ω]
(w : Ω → ℝ) (hw : ∀ d, 0 ≤ w d) (hsum : ∑ d, w d = 1)
(mark : α → Ω → Prop) [∀ p, DecidablePred (mark p)] (k : ℕ) :
(∑ r : Fin k → Ω, (∏ i, w (r i)) *
if ∃ p i j, i ≠ j ∧ mark p (r i) ∧ mark p (r j) then 1 else 0) ≤
(k : ℝ) ^ 2 * ∑ p, (∑ d, w d * if mark p d then 1 else 0) ^ 2 := by
classical
have h := weighted_union_bound
(fun r : Fin k → Ω => ∏ i, w (r i))
(fun (x : α × Fin k × Fin k) r =>
x.2.1 ≠ x.2.2 ∧ mark x.1 (r x.2.1) ∧ mark x.1 (r x.2.2))
(fun r => Finset.prod_nonneg fun i _ => hw (r i))
calc
_ ≤ ∑ p, ∑ i : Fin k, ∑ j : Fin k,
∑ r : Fin k → Ω, (∏ ℓ, w (r ℓ)) *
if i ≠ j ∧ mark p (r i) ∧ mark p (r j) then 1 else 0 := by
simpa only [Prod.exists, Fintype.sum_prod_type] using h
_ ≤ ∑ p, ∑ _i : Fin k, ∑ _j : Fin k,
(∑ d, w d * if mark p d then 1 else 0) ^ 2 := by
apply Finset.sum_le_sum
intro p _
apply Finset.sum_le_sum
intro i _
apply Finset.sum_le_sum
intro j _
by_cases hij : i = j
· simp [hij, sq_nonneg]
· simpa only [hij, ne_eq, not_false_eq_true, true_and] using
(sum_pair_marked_product w hsum (mark p) i j hij).le
_ = _ := by simp [Finset.mul_sum, pow_two, mul_assoc]
/-- Divisors divisible by p are parametrized by the divisors of P/p. -/
theorem sum_divisors_dvd_eq {P p : ℕ} (hP : P ≠ 0) (hp : 0 < p) (hpP : p ∣ P)
(f : ℕ → ℝ) :
(∑ d ∈ P.divisors.filter (fun d => p ∣ d), f d) =
∑ e ∈ (P / p).divisors, f (p * e) := by
symm
refine Finset.sum_bij (fun e _ => p * e) ?_ ?_ ?_ (fun _ _ => rfl)
· intro e he
exact Finset.mem_filter.mpr
⟨Nat.mem_divisors.mpr
⟨(Nat.dvd_div_iff_mul_dvd hpP).mp (Nat.dvd_of_mem_divisors he), hP⟩,
dvd_mul_right p e⟩
· intro e₁ _ e₂ _ h
exact Nat.mul_left_cancel hp h
· intro d hd
obtain ⟨hd, hpd⟩ := Finset.mem_filter.mp hd
refine ⟨d / p, Nat.mem_divisors.mpr ⟨?_, ?_⟩, Nat.mul_div_cancel' hpd⟩
· exact Nat.div_dvd_div hpd (Nat.dvd_of_mem_divisors hd)
· intro h
apply hP
rw [← Nat.mul_div_cancel' hpP, h, mul_zero]
/-- Multiplying a nontrivial divisor by a prime decreases the absolute coefficient. -/
theorem abs_coefficient_mul_le {P p e : ℕ} (hP : 1 < P) (hp : 1 ≤ p) (he : 1 < e) :
|coefficient P (p * e)| ≤ |coefficient P e| := by
have hpe : e ≤ p * e := by simpa using Nat.mul_le_mul_right e hp
have hpe1 : 1 < p * e := he.trans_le hpe
rw [abs_of_neg (coefficient_neg hP hpe1), abs_of_neg (coefficient_neg hP he)]
simp only [coefficient, if_neg (ne_of_gt hpe1), if_neg (ne_of_gt he),
neg_div, neg_neg]
apply one_div_le_one_div_of_le
· exact mul_pos (normalizer_pos hP) (Real.log_pos (by exact_mod_cast he))
· exact mul_le_mul_of_nonneg_left
(Real.log_le_log (by exact_mod_cast (zero_lt_one.trans he))
(by exact_mod_cast hpe)) (normalizer_pos hP).le
/-- The absolute coefficient moment at exponent zero equals one. -/
lemma coefficientAbsMoment_zero {P : ℕ} (hP : 1 < P) : coefficientAbsMoment P 0 = 1 := by
have h := partial_cancellation hP {1}
(by simpa using Nat.one_mem_divisors.mpr (by omega : P ≠ 0)) (by simp)
simpa [coefficientAbsMoment, coefficient, Finset.sdiff_singleton_eq_erase] using h.symm
/-- The sum of absolute coefficients divided by totients equals two. -/
lemma sum_abs_coefficient_div_totient {P : ℕ} (hP : 1 < P) :
(∑ d ∈ P.divisors, |coefficient P d| / d.totient) = 2 := by
rw [← Finset.sum_erase_add _ _ (Nat.one_mem_divisors.mpr (by omega : P ≠ 0))]
have h := coefficientAbsMoment_zero hP
simp only [coefficientAbsMoment, Real.rpow_zero, mul_one] at h
rw [h]
norm_num [coefficient]
/-- The incidence bound (3.7), with an explicit constant once |a(p)| ≤ 1. -/
theorem coefficient_prime_incidence {P p : ℕ} (hP : 1 < P) (hsq : Squarefree P)
(hp : p.Prime) (hpP : p ∣ P) (hcoeff : |coefficient P p| ≤ 1) :
(∑ d ∈ P.divisors.filter (fun d => p ∣ d), |coefficient P d| / d.totient) ≤
4 / (p : ℝ) := by
have hP0 : P ≠ 0 := by omega
have hpR : 0 < (p : ℝ) - 1 := sub_pos.mpr (by exact_mod_cast hp.one_lt)
rw [sum_divisors_dvd_eq hP0 hp.pos hpP]
calc
_ ≤ ∑ e ∈ (P / p).divisors,
(|coefficient P e| / e.totient) / ((p : ℝ) - 1) := by
apply Finset.sum_le_sum
intro e he
have hcop : p.Coprime e := by
apply hp.coprime_iff_not_dvd.mpr
intro hpe
have hpeP := (Nat.dvd_div_iff_mul_dvd hpP).mp (Nat.dvd_of_mem_divisors he)
exact hp.ne_one (Nat.isUnit_iff.mp (hsq p ((mul_dvd_mul_left p hpe).trans hpeP)))
have hcoeff' : |coefficient P (p * e)| ≤ |coefficient P e| := by
by_cases he1 : e = 1
· simpa [he1, coefficient] using hcoeff
· exact abs_coefficient_mul_le hP hp.one_le
(by have := Nat.pos_of_mem_divisors he; omega)
rw [Nat.totient_mul hcop, Nat.totient_prime hp, Nat.cast_mul,
Nat.cast_sub hp.one_le, Nat.cast_one]
calc
_ ≤ |coefficient P e| / (((p : ℝ) - 1) * e.totient) :=
div_le_div_of_nonneg_right hcoeff' (mul_nonneg hpR.le (Nat.cast_nonneg _))
_ = _ := by rw [mul_comm, div_mul_eq_div_div]
_ = (∑ e ∈ (P / p).divisors, |coefficient P e| / e.totient) /
((p : ℝ) - 1) := by rw [Finset.sum_div]
_ ≤ 2 / ((p : ℝ) - 1) := by
apply div_le_div_of_nonneg_right _ hpR.le
calc
_ ≤ ∑ e ∈ P.divisors, |coefficient P e| / e.totient :=
Finset.sum_le_sum_of_subset_of_nonneg
(Nat.divisors_subset_of_dvd hP0 (Nat.div_dvd_of_dvd hpP))
(fun _ _ _ => by positivity)
_ = 2 := sum_abs_coefficient_div_totient hP
_ ≤ 4 / (p : ℝ) := by
apply (div_le_div_iff₀ hpR (by exact_mod_cast hp.pos)).mpr
have : (2 : ℝ) ≤ p := by exact_mod_cast hp.two_le
linarith
/-- The logarithms of distinct prime divisors sum to at most `log n`. -/
lemma sum_log_prime_divisors_le_log {n N : ℕ} (hn : 0 < n) (hnN : n ≤ N) :
(∑ p ∈ N.primesLE, if p ∣ n then Real.log p else 0) ≤ Real.log n := by
have hfilter : N.primesLE.filter (fun p => p ∣ n) = n.primeFactors := by
ext p
simp only [Finset.mem_filter, Nat.mem_primesLE, Nat.mem_primeFactors]
exact ⟨fun h => ⟨h.1.2, h.2, hn.ne'⟩,
fun h => ⟨⟨(Nat.le_of_dvd hn h.2.1).trans hnN, h.1⟩, h.2.1⟩⟩
rw [← Finset.sum_filter, hfilter, ← Real.log_prod (fun p hp =>
Nat.cast_ne_zero.mpr (Nat.mem_primeFactors.mp hp).1.ne_zero)]
apply Real.log_le_log
· exact Finset.prod_pos fun p hp =>
Nat.cast_pos.mpr (Nat.mem_primeFactors.mp hp).1.pos
· rw [← Nat.cast_prod]
exact_mod_cast Nat.le_of_dvd hn (Nat.prod_primeFactors_dvd n)
/-- An elementary upper bound for the logarithmically weighted prime harmonic sum. -/
theorem sum_prime_log_div_le {N : ℕ} (hN : 1 ≤ N) :
(∑ p ∈ N.primesLE, Real.log p / p) ≤ Real.log N + Real.log 4 := by
classical
have hNr : (0 : ℝ) < N := by exact_mod_cast (by omega : 0 < N)
have hcount (p : ℕ) (_hp : p ∈ N.primesLE) :
(N : ℝ) / p - 1 ≤ (N / p : ℕ) := by
simpa only [Nat.floor_div_natCast, Nat.floor_natCast] using
(Nat.sub_one_lt_floor ((N : ℝ) / p)).le
have hsum : (∑ p ∈ N.primesLE, ((N / p : ℕ) : ℝ) * Real.log p) ≤
(N : ℝ) * Real.log N := by
calc
_ = ∑ p ∈ N.primesLE, ∑ n ∈ Finset.range N,
if p ∣ n + 1 then Real.log p else 0 := by
apply Finset.sum_congr rfl
intro p _
rw [← Nat.card_multiples N p, ← Finset.sum_boole]
simp only [Finset.sum_mul, ite_mul, one_mul, zero_mul]
_ = ∑ n ∈ Finset.range N, ∑ p ∈ N.primesLE,
if p ∣ n + 1 then Real.log p else 0 := Finset.sum_comm
_ ≤ ∑ n ∈ Finset.range N, Real.log N := by
apply Finset.sum_le_sum
intro n hn
have hnN : n + 1 ≤ N := by simpa using Finset.mem_range.mp hn
exact (sum_log_prime_divisors_le_log (by omega : 0 < n + 1) hnN).trans
(Real.log_le_log (by positivity) (by exact_mod_cast hnN))
_ = (N : ℝ) * Real.log N := by simp
have hlower : (N : ℝ) * (∑ p ∈ N.primesLE, Real.log p / p) -
Chebyshev.theta N ≤ (N : ℝ) * Real.log N := by
apply le_trans _ hsum
rw [Chebyshev.theta_eq_sum_primesLE_log, Finset.mul_sum, ← Finset.sum_sub_distrib]
apply Finset.sum_le_sum
intro p hp
have h := mul_le_mul_of_nonneg_right (hcount p hp)
(Nat.mem_primesLE.mp hp).2.log_pos.le
calc
(N : ℝ) * (Real.log p / p) - Real.log p =
((N : ℝ) / p - 1) * Real.log p := by ring
_ ≤ _ := h
have htheta := Chebyshev.theta_le_log4_mul_x hNr.le
apply (mul_le_mul_iff_right₀ hNr).mp
nlinarith
/-- The finite Euler product over primes at most N. -/
def eulerProduct (N : ℕ) (σ : ℝ) : ℝ :=
∏ p ∈ N.primesLE, (1 - (p : ℝ) ^ (-σ))⁻¹
/-- The multiplicative weight `n ↦ n ^ (-σ)`. -/
def natPowerHom (σ : ℝ) : ℕ →* ℝ where
toFun n := (n : ℝ) ^ (-σ)
map_one' := by simp
map_mul' a b := by
simp only [Nat.cast_mul]
exact Real.mul_rpow (Nat.cast_nonneg _) (Nat.cast_nonneg _)
/-- The weighted sum over smooth numbers is bounded by the finite Euler product. -/
lemma sum_smooth_le_eulerProduct {N : ℕ} {σ : ℝ} (hσ : 0 < σ)
(S : Finset ℕ) (hS : ∀ n ∈ S, n ∈ (N + 1).smoothNumbers) :
(∑ n ∈ S, (n : ℝ) ^ (-σ)) ≤ eulerProduct N σ := by
classical
have hprime {p : ℕ} (hp : p.Prime) : ‖natPowerHom σ p‖ < 1 := by
change ‖(p : ℝ) ^ (-σ)‖ < 1
rw [Real.norm_eq_abs, abs_of_nonneg (Real.rpow_nonneg (Nat.cast_nonneg p) _)]
exact Real.rpow_lt_one_of_one_lt_of_neg
(by exact_mod_cast hp.one_lt) (neg_neg_of_pos hσ)
have hsum :=
(EulerProduct.summable_and_hasSum_smoothNumbers_prod_primesBelow_geometric
(f := natPowerHom σ) hprime (N + 1)).2
rw [← Finset.sum_subtype_of_mem _ hS]
exact sum_le_hasSum _ (fun n _ => Real.rpow_nonneg (Nat.cast_nonneg _) _) hsum
/-- The lower half of the weak Mertens product estimate. -/
theorem log_le_eulerProduct_one (N : ℕ) : Real.log N ≤ eulerProduct N 1 := by
have h := sum_smooth_le_eulerProduct (N := N) (by norm_num : (0 : ℝ) < 1)
(Finset.Icc 1 N) (fun n hn => Nat.mem_smoothNumbers_of_lt
(by have := Finset.mem_Icc.mp hn; omega)
(by have := Finset.mem_Icc.mp hn; omega))
have hlog := log_le_harmonic_floor (N : ℝ) (Nat.cast_nonneg _)
rw [Nat.floor_natCast, harmonic_eq_sum_Icc] at hlog
simp only [Rat.cast_sum, Rat.cast_inv, Rat.cast_natCast] at hlog