Asymptotic tail estimates that turn finite-prime counts into density bounds.

theorem LeanPool.DeadEnds.sqrt_bXb_div_X_small (b : ℕ) (_hb : 2 ≤ b) (ε : ℝ) (hε : 0 < ε) : ∃ (X₀ : ℕ), ∀ X ≥ X₀, ↑(b * X + b).sqrt / ↑X < ε

theorem LeanPool.DeadEnds.combine_violation_bounds (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 : ℕ) (hX : 0 < X) (ε : ℝ) (_hε : 0 < ε) (htail : (↑T.card + 1) * ∑' (p : { q : Nat.Primes // ↑q > y }), 1 / ↑↑↑p ^ 2 < ε / 2) (hsqrt : (↑T.card + 1) * (↑(b * X + b).sqrt / ↑X) < ε / 2) : ↑{N ∈ Finset.Icc 1 X | ∃ q ∉ S, ↑q ^ 2 ∣ N ∨ ∃ d ∈ T, ↑q ^ 2 ∣ b * N + d}.card / ↑X < ε

theorem LeanPool.DeadEnds.tail_sum_antitone (y y' : ℕ) (h : y ≤ y') : ∑' (p : { q : Nat.Primes // ↑q > y' }), 1 / ↑↑↑p ^ 2 ≤ ∑' (p : { q : Nat.Primes // ↑q > y }), 1 / ↑↑↑p ^ 2

theorem LeanPool.DeadEnds.choose_y_for_tail (b : ℕ) (_hb : 2 ≤ b) (T : Finset ℕ) (ε : ℝ) (hε : 0 < ε) : ∃ y ≥ b, (↑T.card + 1) * ∑' (p : { q : Nat.Primes // ↑q > y }), 1 / ↑↑↑p ^ 2 < ε / 2

Choose y large enough that the tail sum is small enough, and y ≥ b. Uses prime_tail_sum_small with ε/(2*(|T|+1)).

theorem LeanPool.DeadEnds.choose_X_for_sqrt (b : ℕ) (hb : 2 ≤ b) (T : Finset ℕ) (ε : ℝ) (hε : 0 < ε) : ∃ (X₀ : ℕ), 0 < X₀ ∧ ∀ X ≥ X₀, (↑T.card + 1) * (↑(b * X + b).sqrt / ↑X) < ε / 2

Choose X₀ large enough that the √(bX+b)/X term is small and X₀ > 0.

theorem LeanPool.DeadEnds.error_term_vanishes (b : ℕ) (hb : 2 ≤ b) (T : Finset ℕ) (_hT : T ⊆ Finset.range b) (ε : ℝ) (hε : 0 < ε) : ∃ (y : ℕ) (X₁ : ℕ), ∀ (S : Finset Nat.Primes), (∀ (p : Nat.Primes), ↑p ≤ y → p ∈ S) → ∀ X ≥ X₁, ↑{N ∈ Finset.Icc 1 X | ∃ q ∉ S, ↑q ^ 2 ∣ N ∨ ∃ d ∈ T, ↑q ^ 2 ∣ b * N + d}.card / ↑X < ε

The "violation count" (N failing for primes outside S) divided by X vanishes as S grows and X gets large.

theorem LeanPool.DeadEnds.exists_large_for_ratio (M : ℕ) (δ : ℝ) (hδ : 0 < δ) : ∃ (X₀ : ℕ), ∀ X ≥ X₀, ↑M / ↑X < δ

theorem LeanPool.DeadEnds.count_lower_bound_estimate (b : ℕ) (hb : 2 ≤ b) (T : Finset ℕ) (hT : T ⊆ Finset.range b) (ε : ℝ) (hε : 0 < ε) : ∃ (X₀ : ℕ), ∀ X ≥ X₀, ↑(countJointSquarefree b T X) / ↑X ≥ jointSquarefreeDensity b T - ε

Lower bound: for large X, C(X)/X ≥ D(b,T) - ε. The count equals the count for all primes up to some bound, which is close to X·D(b,T). Uses sum of X/p² for primes p > y, which is O(X/y).

theorem LeanPool.DeadEnds.finite_count_upper_bound (b : ℕ) (hb : 2 ≤ b) (T : Finset ℕ) (hT : T ⊆ Finset.range b) (S : Finset Nat.Primes) (X : ℕ) : ↑(countJointSquarefree b T X) ≤ ↑X * ∏ p ∈ S, localDensityFactor (↑p) b T + ↑(∏ p ∈ S, ↑p ^ 2)

theorem LeanPool.DeadEnds.finite_prod_lt_density_add (b : ℕ) (_hb : 2 ≤ b) (T : Finset ℕ) (_hT : T ⊆ Finset.range b) (S : Finset Nat.Primes) (ε : ℝ) (_hε : 0 < ε) (h : |∏ p ∈ S, localDensityFactor (↑p) b T - jointSquarefreeDensity b T| < ε) : ∏ p ∈ S, localDensityFactor (↑p) b T < jointSquarefreeDensity b T + ε

theorem LeanPool.DeadEnds.combine_upper_bounds (b : ℕ) (_hb : 2 ≤ b) (T : Finset ℕ) (_hT : T ⊆ Finset.range b) (S : Finset Nat.Primes) (X : ℕ) (ε : ℝ) (_hε : 0 < ε) (hX : 0 < X) (M : ℕ) (_hM : M = ∏ p ∈ S, ↑p ^ 2) (hcount : ↑(countJointSquarefree b T X) ≤ ↑X * ∏ p ∈ S, localDensityFactor (↑p) b T + ↑M) (hprod : ∏ p ∈ S, localDensityFactor (↑p) b T < jointSquarefreeDensity b T + ε / 2) (hratio : ↑M / ↑X < ε / 2) : ↑(countJointSquarefree b T X) / ↑X ≤ jointSquarefreeDensity b T + ε

theorem LeanPool.DeadEnds.exists_finite_prime_set (y : ℕ) : ∃ (S : Finset Nat.Primes), ∀ (p : Nat.Primes), ↑p ≤ y → p ∈ S

theorem LeanPool.DeadEnds.count_upper_bound_direct (b : ℕ) (hb : 2 ≤ b) (T : Finset ℕ) (hT : T ⊆ Finset.range b) (ε : ℝ) (hε : 0 < ε) : ∃ (X₀ : ℕ), ∀ X ≥ X₀, ↑(countJointSquarefree b T X) / ↑X ≤ jointSquarefreeDensity b T + ε

Upper bound: for large X, C(X)/X ≤ D(b,T) + ε.

theorem LeanPool.DeadEnds.joint_density_eq_euler_product (b : ℕ) (hb : 2 ≤ b) (T : Finset ℕ) (hT : T ⊆ Finset.range b) : Filter.Tendsto (fun (X : ℕ) => ↑(countJointSquarefree b T X) / ↑X) Filter.atTop (nhds (jointSquarefreeDensity b T))

The joint square-free density for subset T equals jointSquarefreeDensity b T. Uses Metric.tendsto_atTop: convergence iff for all ε > 0, eventually |f(n) - L| < ε. Lower bound: count_lower_bound_estimate. Upper bound: count_upper_bound_direct.