Finite-prime counting bounds and comparison with the Euler product density.

theorem LeanPool.DeadEnds.count_upper_bound (b : ℕ) (T : Finset ℕ) (S : Finset Nat.Primes) (X : ℕ) : have M := primeSquareProduct S; have A := validResiduesMod b T S; have count := {N ∈ Finset.Icc 1 X | ∀ p ∈ S, ¬↑p ^ 2 ∣ N ∧ ∀ d ∈ T, ¬↑p ^ 2 ∣ b * N + d}.card; count ≤ (X / M + 1) * A.card

theorem LeanPool.DeadEnds.count_bounds (b : ℕ) (T : Finset ℕ) (S : Finset Nat.Primes) (X : ℕ) : have M := primeSquareProduct S; have A := validResiduesMod b T S; have count := {N ∈ Finset.Icc 1 X | ∀ p ∈ S, ¬↑p ^ 2 ∣ N ∧ ∀ d ∈ T, ¬↑p ^ 2 ∣ b * N + d}.card; X / M * A.card ≤ count ∧ count ≤ (X / M + 1) * A.card

theorem LeanPool.DeadEnds.localDensityProduct_nonneg (b : ℕ) (T : Finset ℕ) (S : Finset Nat.Primes) : 0 ≤ localDensityProduct b T S

Helper: localDensityProduct is non-negative (product of non-negative factors).

theorem LeanPool.DeadEnds.interval_bound {a b lo hi d : ℝ} (ha_lo : lo ≤ a) (ha_hi : a ≤ hi) (hb_lo : lo ≤ b) (hb_hi : b ≤ hi) (hd : hi - lo ≤ d) : |a - b| ≤ d

theorem LeanPool.DeadEnds.floor_div_bounds (X M : ℕ) (hM : 0 < M) : X / M * M ≤ X ∧ X < (X / M + 1) * M

theorem LeanPool.DeadEnds.count_real_bounds (b : ℕ) (hb : 2 ≤ b) (T : Finset ℕ) (hT : T ⊆ Finset.range b) (S : Finset Nat.Primes) (X : ℕ) : have M := primeSquareProduct S; have L := localDensityProduct b T S; have q := X / M; have count := {N ∈ Finset.Icc 1 X | ∀ p ∈ S, ¬↑p ^ 2 ∣ N ∧ ∀ d ∈ T, ¬↑p ^ 2 ∣ b * N + d}.card; ↑q * ↑M * L ≤ ↑count ∧ ↑count ≤ (↑q + 1) * ↑M * L

Helper: From count_bounds + validResidues_card_eq_mul, get the real-valued bounds.

theorem LeanPool.DeadEnds.xL_real_bounds (X M : ℕ) (L : ℝ) (hL : 0 ≤ L) (hM : 0 < M) : have q := X / M; ↑q * ↑M * L ≤ ↑X * L ∧ ↑X * L ≤ (↑q + 1) * ↑M * L

theorem LeanPool.DeadEnds.final_error_bound {count X M : ℕ} {L : ℝ} {q : ℕ} (hcount_lo : ↑q * ↑M * L ≤ ↑count) (hcount_hi : ↑count ≤ (↑q + 1) * ↑M * L) (hxL_lo : ↑q * ↑M * L ≤ ↑X * L) (hxL_hi : ↑X * L ≤ (↑q + 1) * ↑M * L) (_hL_nonneg : 0 ≤ L) (hL_le_one : L ≤ 1) : |↑count - ↑X * L| ≤ ↑M

theorem LeanPool.DeadEnds.error_bound_empty_case (b : ℕ) (_hb : 2 ≤ b) (T : Finset ℕ) (_hT : T ⊆ Finset.range b) (S : Finset Nat.Primes) (X : ℕ) (hM : primeSquareProduct S = 0) : have M := primeSquareProduct S; have L := localDensityProduct b T S; have count := {N ∈ Finset.Icc 1 X | ∀ p ∈ S, ¬↑p ^ 2 ∣ N ∧ ∀ d ∈ T, ¬↑p ^ 2 ∣ b * N + d}.card; |↑count - ↑X * L| ≤ ↑M

theorem LeanPool.DeadEnds.error_bound (b : ℕ) (hb : 2 ≤ b) (T : Finset ℕ) (hT : T ⊆ Finset.range b) (S : Finset Nat.Primes) (X : ℕ) : have M := primeSquareProduct S; have L := localDensityProduct b T S; have count := {N ∈ Finset.Icc 1 X | ∀ p ∈ S, ¬↑p ^ 2 ∣ N ∧ ∀ d ∈ T, ¬↑p ^ 2 ∣ b * N + d}.card; |↑count - ↑X * L| ≤ ↑M

Finite-prime counts differ from the expected local-density main term by at most the modulus.

theorem LeanPool.DeadEnds.count_finite_prime_approx (b : ℕ) (hb : 2 ≤ b) (T : Finset ℕ) (hT : T ⊆ Finset.range b) (S : Finset Nat.Primes) (X : ℕ) : |↑{N ∈ Finset.Icc 1 X | ∀ p ∈ S, ¬↑p ^ 2 ∣ N ∧ ∀ d ∈ T, ¬↑p ^ 2 ∣ b * N + d}.card - ↑X * ∏ p ∈ S, localDensityFactor (↑p) b T| ≤ ∏ p ∈ S, ↑↑p ^ 2

theorem LeanPool.DeadEnds.hasProd_implies_finite_approx (b : ℕ) (hb : 2 ≤ b) (T : Finset ℕ) (hT : T ⊆ Finset.range b) (ε : ℝ) (hε : 0 < ε) : ∃ (A : Finset Nat.Primes), ∀ (S : Finset Nat.Primes), A ⊆ S → |∏ p ∈ S, localDensityFactor (↑p) b T - jointSquarefreeDensity b T| < ε

theorem LeanPool.DeadEnds.finite_product_converges_to_density (b : ℕ) (hb : 2 ≤ b) (T : Finset ℕ) (hT : T ⊆ Finset.range b) (ε : ℝ) (hε : 0 < ε) : ∃ (y : ℕ), ∀ (S : Finset Nat.Primes), (∀ (p : Nat.Primes), ↑p ≤ y → p ∈ S) → |∏ p ∈ S, localDensityFactor (↑p) b T - jointSquarefreeDensity b T| < ε

For any ε > 0, the tail contribution from primes p > y to the joint density (measuring how much the finite product differs from the infinite product) can be made arbitrarily small by choosing y large enough. Uses jointSquarefreeDensity_multipliable to ensure convergence.

theorem LeanPool.DeadEnds.count_upper_bound_via_finite (b : ℕ) (_hb : 2 ≤ b) (T : Finset ℕ) (_hT : T ⊆ Finset.range b) (S : Finset Nat.Primes) (X : ℕ) : ↑(countJointSquarefree b T X) ≤ ↑{N ∈ Finset.Icc 1 X | ∀ p ∈ S, ¬↑p ^ 2 ∣ N ∧ ∀ d ∈ T, ¬↑p ^ 2 ∣ b * N + d}.card

Upper bound: For any S, C(X) ≤ #{N ≤ X : N satisfies S-conditions} since C(X) imposes more constraints. Combined with count_finite_prime_approx, this gives limsup C(X)/X ≤ D(b,T).

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

The number of N ∈ [1, X] such that for every p ∈ S we have p² ∤ N and p² ∤ b * N + d for all d ∈ T (i.e. the square-free conditions checked only at the primes in S).

Equations

• LeanPool.DeadEnds.countFinitePrime b T S X = {N ∈ Finset.Icc 1 X | ∀ p ∈ S, ¬↑p ^ 2 ∣ N ∧ ∀ d ∈ T, ¬↑p ^ 2 ∣ b * N + d}.card

def LeanPool.DeadEnds.primesUpTo (n : ℕ) : Finset Nat.Primes

The primes p ≤ n, packaged as a Finset Nat.Primes.

Equations

• One or more equations did not get rendered due to their size.

theorem LeanPool.DeadEnds.mem_primesUpTo (n : ℕ) (p : Nat.Primes) : ↑p ≤ n → p ∈ primesUpTo n

theorem LeanPool.DeadEnds.crt_error_bound (b : ℕ) (hb : 2 ≤ b) (T : Finset ℕ) (hT : T ⊆ Finset.range b) (S : Finset Nat.Primes) (X : ℕ) : |↑(countFinitePrime b T S X) - ↑X * localDensityProduct b T S| ≤ ↑(primeSquareProduct S)

theorem LeanPool.DeadEnds.count_finite_lower (b : ℕ) (hb : 2 ≤ b) (T : Finset ℕ) (hT : T ⊆ Finset.range b) (S : Finset Nat.Primes) (X : ℕ) : ↑(countFinitePrime b T S X) ≥ ↑X * localDensityProduct b T S - ↑(primeSquareProduct S)

theorem LeanPool.DeadEnds.finite_product_ge_density (b : ℕ) (hb : 2 ≤ b) (T : Finset ℕ) (hT : T ⊆ Finset.range b) (S : Finset Nat.Primes) : localDensityProduct b T S ≥ jointSquarefreeDensity b T

theorem LeanPool.DeadEnds.jointSquarefree_subset_finitePrime (b : ℕ) (T : Finset ℕ) (S : Finset Nat.Primes) (X : ℕ) : {N ∈ Finset.Icc 1 X | Squarefree N ∧ ∀ d ∈ T, Squarefree (b * N + d)} ⊆ {N ∈ Finset.Icc 1 X | ∀ p ∈ S, ¬↑p ^ 2 ∣ N ∧ ∀ d ∈ T, ¬↑p ^ 2 ∣ b * N + d}

theorem LeanPool.DeadEnds.not_squarefree_has_prime_sq_divisor (n : ℕ) (h : ¬Squarefree n) : ∃ (p : Nat.Primes), ↑p ^ 2 ∣ n

theorem LeanPool.DeadEnds.sdiff_subset_violations (b : ℕ) (T : Finset ℕ) (S : Finset Nat.Primes) (X : ℕ) : {N ∈ Finset.Icc 1 X | ∀ p ∈ S, ¬↑p ^ 2 ∣ N ∧ ∀ d ∈ T, ¬↑p ^ 2 ∣ b * N + d} \ {N ∈ Finset.Icc 1 X | Squarefree N ∧ ∀ d ∈ T, Squarefree (b * N + d)} ⊆ {N ∈ Finset.Icc 1 X | ∃ q ∉ S, ↑q ^ 2 ∣ N ∨ ∃ d ∈ T, ↑q ^ 2 ∣ b * N + d}

theorem LeanPool.DeadEnds.count_ge_finite_minus_violations (b : ℕ) (_hb : 2 ≤ b) (T : Finset ℕ) (_hT : T ⊆ Finset.range b) (S : Finset Nat.Primes) (X : ℕ) : ↑(countJointSquarefree b T X) ≥ ↑(countFinitePrime b T S X) - ↑{N ∈ Finset.Icc 1 X | ∃ q ∉ S, ↑q ^ 2 ∣ N ∨ ∃ d ∈ T, ↑q ^ 2 ∣ b * N + d}.card

theorem LeanPool.DeadEnds.combine_bounds_lower (b : ℕ) (hb : 2 ≤ b) (T : Finset ℕ) (hT : T ⊆ Finset.range b) (S : Finset Nat.Primes) (X : ℕ) (hX : 0 < X) (δ₁ δ₂ : ℝ) (hδ₁ : ↑{N ∈ Finset.Icc 1 X | ∃ q ∉ S, ↑q ^ 2 ∣ N ∨ ∃ d ∈ T, ↑q ^ 2 ∣ b * N + d}.card / ↑X < δ₁) (hδ₂ : ↑(primeSquareProduct S) / ↑X < δ₂) : ↑(countJointSquarefree b T X) / ↑X ≥ jointSquarefreeDensity b T - δ₁ - δ₂