Prime-tail and single-prime divisibility estimates.

theorem LeanPool.DeadEnds.gt_sup_imp_not_mem (s : Finset Nat.Primes) (q : Nat.Primes) (hq : ↑q > s.sup fun (x : Nat.Primes) => ↑x) : q ∉ s

theorem LeanPool.DeadEnds.tsum_primes_gt_le_tsum_compl (f : Nat.Primes → ℝ) (hf : ∀ (p : Nat.Primes), 0 ≤ f p) (hsum : Summable f) (s : Finset Nat.Primes) : ∑' (p : { q : Nat.Primes // ↑q > s.sup fun (x : Nat.Primes) => ↑x }), f ↑p ≤ ∑' (p : { q : Nat.Primes // q ∉ s }), f ↑p

theorem LeanPool.DeadEnds.exists_finset_tsum_compl_lt (f : Nat.Primes → ℝ) (_hf : ∀ (p : Nat.Primes), 0 ≤ f p) (_hsum : Summable f) (ε : ℝ) (hε : 0 < ε) : ∃ (s : Finset Nat.Primes), ∑' (p : { q : Nat.Primes // q ∉ s }), f ↑p < ε

theorem LeanPool.DeadEnds.prime_tail_sum_small (ε : ℝ) (hε : 0 < ε) : ∃ (y : ℕ), ∑' (p : { q : Nat.Primes // ↑q > y }), 1 / ↑↑↑p ^ 2 < ε

theorem LeanPool.DeadEnds.prime_count_le_sqrt (M : ℕ) : M.sqrt.primesBelow.card ≤ M.sqrt

theorem LeanPool.DeadEnds.sqrt_div_X_small (ε : ℝ) (hε : 0 < ε) : ∃ (X₀ : ℕ), ∀ X ≥ X₀, ↑X.sqrt / ↑X < ε

theorem LeanPool.DeadEnds.card_multiples_Icc (q X : ℕ) : {N ∈ Finset.Icc 1 X | q ^ 2 ∣ N}.card ≤ X / q ^ 2

theorem LeanPool.DeadEnds.floor_diff_bound_rat (X v r : ℕ) (hr : 0 < r) : ⌊(↑X - ↑v) / ↑r⌋ - ⌊-↑v / ↑r⌋ ≤ ⌊↑X / ↑r⌋ + 1

The number of N ∈ (0, X] satisfying N ≡ v (mod r) is at most X / r + 1.

The exact count is given by Nat.Ioc_filter_modEq_card: {x ∈ Finset.Ioc a b | x ≡ v [MOD r]}.card = max(⌊(b - v)/r⌋ - ⌊(a - v)/r⌋, 0) For a = 0, b = X, the count equals max(⌊(X - v)/r⌋ - ⌊-v/r⌋, 0). By floor_diff_bound, the expression ⌊(X - v)/r⌋ - ⌊-v/r⌋ ≤ ⌊X/r⌋ + 1. Since X, r are naturals, ⌊(X : ℝ)/r⌋ = X / r (integer division). The nonnegative floor difference is at most the upper bound, giving count ≤ X / r + 1.

theorem LeanPool.DeadEnds.card_modEq_Icc_bound (v r X : ℕ) (hr : 0 < r) : {N ∈ Finset.Ioc 0 X | N ≡ v [MOD r]}.card ≤ X / r + 1

theorem LeanPool.DeadEnds.gcd_psq_b_eq_one (p : ℕ) (hp : Nat.Prime p) (b : ℕ) (hb : 2 ≤ b) (hbp : b < p) : (p ^ 2).gcd b = 1

theorem LeanPool.DeadEnds.prime_sq_pos (p : ℕ) (hp : Nat.Prime p) : 0 < p ^ 2

p² > 0 when p is prime.

theorem LeanPool.DeadEnds.zmod_mul_inv_add_eq_zero (n b d : ℕ) (_hn : 0 < n) (hb : b.Coprime n) : ↑b * (-↑d * (↑b)⁻¹) + ↑d = 0

theorem LeanPool.DeadEnds.exists_inverse_residue (p : ℕ) (hp : Nat.Prime p) (b : ℕ) (hb : 2 ≤ b) (hbp : b < p) (d : ℕ) : ∃ v < p ^ 2, p ^ 2 ∣ b * v + d

Constructs a unique residue v such that bv ≡ -d (mod p²) for prime p > b ≥ 2. In ZMod (p²), since b is a unit (coprime to p²), we can define v = b⁻¹ * (-d). The result is a natural number v < p² such that p² | bv + d.

theorem LeanPool.DeadEnds.dvd_iff_modEq_of_coprime (p b v d N : ℕ) (hcop : (p ^ 2).gcd b = 1) (hdvd_v : p ^ 2 ∣ b * v + d) : p ^ 2 ∣ b * N + d ↔ N ≡ v [MOD p ^ 2]

theorem LeanPool.DeadEnds.dvd_shift_iff_modEq_unique (b : ℕ) (hb : 2 ≤ b) (q : Nat.Primes) (hq : ↑q > b) (d : ℕ) : ∃ (v : ℕ), ∀ (N : ℕ), ↑q ^ 2 ∣ b * N + d ↔ N ≡ v [MOD ↑q ^ 2]

theorem LeanPool.DeadEnds.filter_shifted_dvd_eq_filter_modEq (b : ℕ) (hb : 2 ≤ b) (q : Nat.Primes) (hq : ↑q > b) (d : ℕ) (S : Finset ℕ) : ∃ (v : ℕ), {N ∈ S | ↑q ^ 2 ∣ b * N + d} = {N ∈ S | N ≡ v [MOD ↑q ^ 2]}

theorem LeanPool.DeadEnds.card_shifted_divisible_bound (b : ℕ) (hb : 2 ≤ b) (q : Nat.Primes) (hq : ↑q > b) (d X : ℕ) : {N ∈ Finset.Icc 1 X | ↑q ^ 2 ∣ b * N + d}.card ≤ X / ↑q ^ 2 + 1

For a fixed d, the count of N in [1,X] with q²|(bN+d) is at most X/q² + 1. Since q > b and q is prime, gcd(b,q²) = 1, so the congruence bN ≡ -d (mod q²) has a unique solution mod q². The solutions form an arithmetic progression with common difference q², so there are at most ⌊X/q²⌋ + 1 solutions in [1,X].

theorem LeanPool.DeadEnds.card_union_shifted_bound (b : ℕ) (hb : 2 ≤ b) (T : Finset ℕ) (_hT : T ⊆ Finset.range b) (q : Nat.Primes) (hq : ↑q > b) (X : ℕ) : {N ∈ Finset.Icc 1 X | ∃ d ∈ T, ↑q ^ 2 ∣ b * N + d}.card ≤ T.card * (X / ↑q ^ 2 + 1)

The count of N in [1,X] with ∃d∈T, q²|(bN+d) is at most |T|*(X/q² + 1). This follows from the union bound over T applied to card_shifted_divisible_bound. Uses Finset.card_biUnion_le_card_mul : ∀ (s : Finset ι) (f : ι → Finset β) (n : ℕ), (∀ a ∈ s, (f a).card ≤ n) → (s.biUnion f).card ≤ s.card * n.

theorem LeanPool.DeadEnds.combined_bound_aux (T : Finset ℕ) (X q_sq : ℕ) : X / q_sq + T.card * (X / q_sq + 1) ≤ (T.card + 1) * (X / q_sq + 1)

theorem LeanPool.DeadEnds.single_prime_violation_bound (b : ℕ) (hb : 2 ≤ b) (T : Finset ℕ) (hT : T ⊆ Finset.range b) (q : Nat.Primes) (hq : ↑q > b) (X : ℕ) : {N ∈ Finset.Icc 1 X | ↑q ^ 2 ∣ N ∨ ∃ d ∈ T, ↑q ^ 2 ∣ b * N + d}.card ≤ (T.card + 1) * (X / ↑q ^ 2 + 1)