Bounding the finite set of primes relevant to square-divisibility violations.

noncomputable def LeanPool.DeadEnds.primesBelow' (n : ℕ) : Finset Nat.Primes

Convert Nat.primesBelow to a finset of bundled primes.

Equations

• LeanPool.DeadEnds.primesBelow' n = Finset.subtype Nat.Prime n.primesBelow

noncomputable def LeanPool.DeadEnds.relevantNotInS (b X : ℕ) (S : Finset Nat.Primes) : Finset Nat.Primes

The set of primes q with q ≤ √(bX+b) that are not in S. Any violation by q ∉ S must have q² ≤ bX+b, so q ≤ √(bX+b) < √(bX+b)+1. Either q² | N (so q² ≤ X ≤ bX+b) or q² | bN+d with d < b (so q² ≤ bX + b - 1 < bX+b).

Equations

• LeanPool.DeadEnds.relevantNotInS b X S = {x ∈ LeanPool.DeadEnds.primesBelow' ((b * X + b).sqrt + 1) | x ∉ S}

theorem LeanPool.DeadEnds.primesBelow_succ_card_le (k : ℕ) : (k + 1).primesBelow.card ≤ k

theorem LeanPool.DeadEnds.primesBelow'_card (n : ℕ) : (primesBelow' n).card = n.primesBelow.card

theorem LeanPool.DeadEnds.relevantNotInS_card_le (b X : ℕ) (S : Finset Nat.Primes) : (relevantNotInS b X S).card ≤ (b * X + b).sqrt

theorem LeanPool.DeadEnds.not_in_S_implies_gt_y (S : Finset Nat.Primes) (y : ℕ) (hy : ∀ (p : Nat.Primes), ↑p ≤ y → p ∈ S) (q : Nat.Primes) (hq : q ∉ S) : ↑q > y

theorem LeanPool.DeadEnds.relevantNotInS_gt_y (b X : ℕ) (S : Finset Nat.Primes) (y : ℕ) (hy : ∀ (p : Nat.Primes), ↑p ≤ y → p ∈ S) (q : Nat.Primes) (hq : q ∈ relevantNotInS b X S) : ↑q > y

theorem LeanPool.DeadEnds.relevantNotInS_gt_b (b X : ℕ) (S : Finset Nat.Primes) (y : ℕ) (hy : ∀ (p : Nat.Primes), ↑p ≤ y → p ∈ S) (hyb : y ≥ b) (q : Nat.Primes) (hq : q ∈ relevantNotInS b X S) : ↑q > b

theorem LeanPool.DeadEnds.prime_sq_bound_from_N_dvd (b X N : ℕ) (hb : 2 ≤ b) (q : Nat.Primes) (hN : N ∈ Finset.Icc 1 X) (hdvd : ↑q ^ 2 ∣ N) : ↑q < (b * X + b).sqrt + 1

theorem LeanPool.DeadEnds.prime_sq_bound_from_shifted_dvd (b X N d : ℕ) (hb : 2 ≤ b) (q : Nat.Primes) (hN : N ∈ Finset.Icc 1 X) (hd : d ∈ Finset.range b) (hdvd : ↑q ^ 2 ∣ b * N + d) : ↑q < (b * X + b).sqrt + 1

theorem LeanPool.DeadEnds.violation_subset_biUnion (b : ℕ) (hb : 2 ≤ b) (T : Finset ℕ) (hT : T ⊆ Finset.range b) (S : Finset Nat.Primes) (X : ℕ) : {N ∈ Finset.Icc 1 X | ∃ q ∉ S, ↑q ^ 2 ∣ N ∨ ∃ d ∈ T, ↑q ^ 2 ∣ b * N + d} ⊆ (relevantNotInS b X S).biUnion fun (q : Nat.Primes) => {N ∈ Finset.Icc 1 X | ↑q ^ 2 ∣ N ∨ ∃ d ∈ T, ↑q ^ 2 ∣ b * N + d}

theorem LeanPool.DeadEnds.union_card_bound (b : ℕ) (hb : 2 ≤ b) (T : Finset ℕ) (hT : T ⊆ Finset.range b) (S : Finset Nat.Primes) (y : ℕ) (hy : ∀ (p : Nat.Primes), ↑p ≤ y → p ∈ S) (hyb : y ≥ b) (X : ℕ) : {N ∈ Finset.Icc 1 X | ∃ q ∉ S, ↑q ^ 2 ∣ N ∨ ∃ d ∈ T, ↑q ^ 2 ∣ b * N + d}.card ≤ ∑ q ∈ relevantNotInS b X S, (T.card + 1) * (X / ↑q ^ 2 + 1)

Union bound: card(V) ≤ ∑_{q ∈ relevantNotInS} card(V_q). Combines violation_subset_biUnion with Finset.card_le_card and Finset.card_biUnion_le. Uses Finset.card_biUnion_le : (s.biUnion t).card ≤ ∑ a ∈ s, (t a).card.

theorem LeanPool.DeadEnds.finsum_le_tsum_tail (y : ℕ) (Q : Finset Nat.Primes) (hQ : ∀ q ∈ Q, ↑q > y) : ∑ q ∈ Q, 1 / ↑↑q ^ 2 ≤ ∑' (p : { q : Nat.Primes // ↑q > y }), 1 / ↑↑↑p ^ 2

The finite sum ∑{q∈Q} 1/q² over primes in Q is ≤ the tsum ∑'{p>y} 1/p² where all primes q in Q satisfy q > y. This uses that Q (as a subset of {primes p > y}) contributes to the infinite sum. Since 1/q² ≥ 0 for all primes q, and the sum over primes converges, the finite partial sum is bounded by the full tail sum. Uses Summable.sum_le_tsum : ∀ {ι : Type*} {f : ι → ℝ} (s : Finset ι), (∀ i ∉ s, 0 ≤ f i) → Summable f → ∑ i ∈ s, f i ≤ ∑' i, f i.

theorem LeanPool.DeadEnds.sum_expand (c : ℝ) (X : ℕ) (Q : Finset Nat.Primes) : ∑ q ∈ Q, c * (↑X / ↑↑q ^ 2 + 1) = c * ↑X * ∑ q ∈ Q, 1 / ↑↑q ^ 2 + c * ↑Q.card

theorem LeanPool.DeadEnds.sum_bound_real (T : Finset ℕ) (y X : ℕ) (Q : Finset Nat.Primes) (hQ : ∀ q ∈ Q, ↑q > y) : ∑ q ∈ Q, (↑T.card + 1) * (↑X / ↑↑q ^ 2 + 1) ≤ (↑T.card + 1) * ↑X * ∑' (p : { q : Nat.Primes // ↑q > y }), 1 / ↑↑↑p ^ 2 + (↑T.card + 1) * ↑Q.card

theorem LeanPool.DeadEnds.nat_div_floor_le_real_div (X : ℕ) (q : Nat.Primes) : ↑(X / ↑q ^ 2) ≤ ↑X / ↑↑q ^ 2

theorem LeanPool.DeadEnds.nat_sum_le_real_sum (T : Finset ℕ) (X : ℕ) (Q : Finset Nat.Primes) : ↑(∑ q ∈ Q, (T.card + 1) * (X / ↑q ^ 2 + 1)) ≤ ∑ q ∈ Q, (↑T.card + 1) * (↑X / ↑↑q ^ 2 + 1)

theorem LeanPool.DeadEnds.violation_count_bound (b : ℕ) (hb : 2 ≤ b) (T : Finset ℕ) (hT : T ⊆ Finset.range b) (S : Finset Nat.Primes) (y : ℕ) (hy : ∀ (p : Nat.Primes), ↑p ≤ y → p ∈ S) (hyb : y ≥ b) (X : ℕ) : ↑{N ∈ Finset.Icc 1 X | ∃ q ∉ S, ↑q ^ 2 ∣ N ∨ ∃ d ∈ T, ↑q ^ 2 ∣ b * N + d}.card ≤ (↑T.card + 1) * ↑X * ∑' (p : { q : Nat.Primes // ↑q > y }), 1 / ↑↑↑p ^ 2 + (↑T.card + 1) * ↑(b * X + b).sqrt

Violation count is bounded by the prime-square tail term plus a square-root count term.