Counting functions for joint conditions

@[implicit_reducible]

noncomputable instance LeanPool.DeadEnds.decidablePredViolation (b : ℕ) (T : Finset ℕ) (S : Finset Nat.Primes) : DecidablePred fun (N : ℕ) => ∃ q ∉ S, ↑q ^ 2 ∣ N ∨ ∃ d ∈ T, ↑q ^ 2 ∣ b * N + d

Equations

• LeanPool.DeadEnds.decidablePredViolation b T S x✝ = Classical.propDecidable ((fun (N : ℕ) => ∃ q ∉ S, ↑q ^ 2 ∣ N ∨ ∃ d ∈ T, ↑q ^ 2 ∣ b * N + d) x✝)

def LeanPool.DeadEnds.IsBaseBDeadEnd (b N : ℕ) : Prop

A positive integer N is a base-b dead end: N is square-free, yet b * N + d fails to be square-free for every digit d ∈ {0, …, b - 1}.

Equations

• LeanPool.DeadEnds.IsBaseBDeadEnd b N = (0 < N ∧ Squarefree N ∧ ∀ d ∈ Finset.range b, ¬Squarefree (b * N + d))

@[implicit_reducible]

instance LeanPool.DeadEnds.instDecidableIsBaseBDeadEnd (b N : ℕ) : Decidable (IsBaseBDeadEnd b N)

Equations

• LeanPool.DeadEnds.instDecidableIsBaseBDeadEnd b N = id inferInstance

def LeanPool.DeadEnds.countBaseBDeadEnds (b X : ℕ) : ℕ

The number of base-b dead ends in [1, X].

Equations

• LeanPool.DeadEnds.countBaseBDeadEnds b X = {N ∈ Finset.Icc 1 X | LeanPool.DeadEnds.IsBaseBDeadEnd b N}.card

def LeanPool.DeadEnds.HasAsymptoticDensity (b : ℕ) (D : ℝ) : Prop

The asymptotic density of base-b dead ends equals D, i.e. countBaseBDeadEnds b X / X → D as X → ∞.

Equations

• LeanPool.DeadEnds.HasAsymptoticDensity b D = Filter.Tendsto (fun (X : ℕ) => ↑(LeanPool.DeadEnds.countBaseBDeadEnds b X) / ↑X) Filter.atTop (nhds D)

noncomputable def LeanPool.DeadEnds.localDensityFactor (p b : ℕ) (T : Finset ℕ) : ℝ

The local density factor μ_p(b, T): the fraction of residues r ∈ [0, p²) with p² ∤ r and p² ∤ b * r + d for every d ∈ T.

Equations

• LeanPool.DeadEnds.localDensityFactor p b T = ↑{r ∈ Finset.range (p ^ 2) | ¬p ^ 2 ∣ r ∧ ∀ d ∈ T, ¬p ^ 2 ∣ b * r + d}.card / ↑(p ^ 2)

noncomputable def LeanPool.DeadEnds.jointSquarefreeDensity (b : ℕ) (T : Finset ℕ) : ℝ

The joint square-free density α(b, T) = ∏_p μ_p(b, T), the infinite product over all primes.

Equations

• LeanPool.DeadEnds.jointSquarefreeDensity b T = ∏' (p : Nat.Primes), LeanPool.DeadEnds.localDensityFactor (↑p) b T

noncomputable def LeanPool.DeadEnds.explicitDensityFormula (b : ℕ) : ℝ

The explicit inclusion-exclusion formula ∑_{T ⊆ {0,…,b-1}} (-1)^{|T|} α(b, T) for D_b.

Equations

• LeanPool.DeadEnds.explicitDensityFormula b = ∑ T ∈ (Finset.range b).powerset, (-1) ^ T.card * LeanPool.DeadEnds.jointSquarefreeDensity b T

def LeanPool.DeadEnds.countJointSquarefree (b : ℕ) (T : Finset ℕ) (X : ℕ) : ℕ

Count N in [1,X] such that N is squarefree and bN+d is squarefree for all d in T

Equations

• LeanPool.DeadEnds.countJointSquarefree b T X = {N ∈ Finset.Icc 1 X | Squarefree N ∧ ∀ d ∈ T, Squarefree (b * N + d)}.card

Helper lemmas for summability of local density deviations

def LeanPool.DeadEnds.typeA (p : ℕ) : Finset ℕ

The residues r ∈ [0, p²) divisible by p² (just r = 0).

Equations

• LeanPool.DeadEnds.typeA p = {r ∈ Finset.range (p ^ 2) | p ^ 2 ∣ r}

theorem LeanPool.DeadEnds.typeA_card_eq_one (p : ℕ) (hp : Nat.Prime p) : (typeA p).card = 1

theorem LeanPool.DeadEnds.b_coprime_p_sq (p : ℕ) (hp : Nat.Prime p) (b : ℕ) (hb : 2 ≤ b) (hbp : b < p) : b.Coprime (p ^ 2)

theorem LeanPool.DeadEnds.r_eq_inv_image (p : ℕ) (hp : Nat.Prime p) (b : ℕ) (hb : 2 ≤ b) (hbp : b < p) (r : ℕ) (hr : r < p ^ 2) (d : ℕ) (hd : p ^ 2 ∣ b * r + d) : r = (-↑d * (↑b)⁻¹).val

theorem LeanPool.DeadEnds.filtered_subset_image (p : ℕ) (hp : Nat.Prime p) (b : ℕ) (hb : 2 ≤ b) (hbp : b < p) (T : Finset ℕ) (_hT : T ⊆ Finset.range b) : {r ∈ Finset.range (p ^ 2) | ∃ d ∈ T, p ^ 2 ∣ b * r + d} ⊆ Finset.image (fun (d : ℕ) => (-↑d * (↑b)⁻¹).val) T

theorem LeanPool.DeadEnds.bad_residues_type_B_card_le (p : ℕ) (hp : Nat.Prime p) (b : ℕ) (hb : 2 ≤ b) (hbp : b < p) (T : Finset ℕ) (hT : T ⊆ Finset.range b) : {r ∈ Finset.range (p ^ 2) | ∃ d ∈ T, p ^ 2 ∣ b * r + d}.card ≤ T.card

def LeanPool.DeadEnds.typeB (p b : ℕ) (T : Finset ℕ) : Finset ℕ

The residues r ∈ [0, p²) for which p² ∣ b * r + d for some d ∈ T.

Equations

• LeanPool.DeadEnds.typeB p b T = {r ∈ Finset.range (p ^ 2) | ∃ d ∈ T, p ^ 2 ∣ b * r + d}

theorem LeanPool.DeadEnds.bad_residues_card_le (p : ℕ) (hp : Nat.Prime p) (b : ℕ) (hb : 2 ≤ b) (hbp : b < p) (T : Finset ℕ) (hT : T ⊆ Finset.range b) : {r ∈ Finset.range (p ^ 2) | p ^ 2 ∣ r ∨ ∃ d ∈ T, p ^ 2 ∣ b * r + d}.card ≤ T.card + 1

theorem LeanPool.DeadEnds.valid_residues_card_ge (p : ℕ) (hp : Nat.Prime p) (b : ℕ) (hb : 2 ≤ b) (hbp : b < p) (T : Finset ℕ) (hT : T ⊆ Finset.range b) : p ^ 2 - (T.card + 1) ≤ {r ∈ Finset.range (p ^ 2) | ¬p ^ 2 ∣ r ∧ ∀ d ∈ T, ¬p ^ 2 ∣ b * r + d}.card

theorem LeanPool.DeadEnds.localDensityFactor_le_one (p b : ℕ) (T : Finset ℕ) : localDensityFactor p b T ≤ 1

theorem LeanPool.DeadEnds.localDensityFactor_nonneg (p b : ℕ) (T : Finset ℕ) : 0 ≤ localDensityFactor p b T

theorem LeanPool.DeadEnds.localDensityFactor_ge_sub (p : ℕ) (hp : Nat.Prime p) (b : ℕ) (hb : 2 ≤ b) (hbp : b < p) (T : Finset ℕ) (hT : T ⊆ Finset.range b) : 1 - (↑T.card + 1) / ↑p ^ 2 ≤ localDensityFactor p b T

theorem LeanPool.DeadEnds.localDensityFactor_near_one_large_prime (p : ℕ) (hp : Nat.Prime p) (b : ℕ) (hb : 2 ≤ b) (hbp : b < p) (T : Finset ℕ) (hT : T ⊆ Finset.range b) : |localDensityFactor p b T - 1| ≤ (↑T.card + 1) / ↑p ^ 2

theorem LeanPool.DeadEnds.primes_summable_one_div_sq : Summable fun (p : Nat.Primes) => 1 / ↑↑p ^ 2

theorem LeanPool.DeadEnds.bound_summable (b : ℕ) (_hb : 2 ≤ b) (T : Finset ℕ) (_hT : T ⊆ Finset.range b) : Summable fun (p : Nat.Primes) => (↑T.card + 1) / ↑↑p ^ 2

theorem LeanPool.DeadEnds.deviation_bound_for_large_prime (p : ℕ) (hp : Nat.Prime p) (b : ℕ) (hb : 2 ≤ b) (hbp : b < p) (T : Finset ℕ) (hT : T ⊆ Finset.range b) : ‖|localDensityFactor p b T - 1|‖ ≤ (↑T.card + 1) / ↑p ^ 2

theorem LeanPool.DeadEnds.finite_primes_le (b : ℕ) : {p : Nat.Primes | ↑p ≤ b}.Finite

theorem LeanPool.DeadEnds.deviation_bounded_eventually (b : ℕ) (hb : 2 ≤ b) (T : Finset ℕ) (hT : T ⊆ Finset.range b) : ∀ᶠ (p : Nat.Primes) in Filter.cofinite, ‖|localDensityFactor (↑p) b T - 1|‖ ≤ (↑T.card + 1) / ↑↑p ^ 2

theorem LeanPool.DeadEnds.sum_localDensityFactor_deviation_summable (b : ℕ) (hb : 2 ≤ b) (T : Finset ℕ) (hT : T ⊆ Finset.range b) : Summable fun (p : Nat.Primes) => |localDensityFactor (↑p) b T - 1|

The sum ∑_p |μ_p(b,T) - 1| converges. By localDensityFactor_near_one, |μ_p - 1| ≤ (|T|+1)/p². Since ∑_p 1/p² converges (it's bounded by ∑_n 1/n² = π²/6), the sum converges.

theorem LeanPool.DeadEnds.multipliable_of_deviation_summable (b : ℕ) (_hb : 2 ≤ b) (T : Finset ℕ) (_hT : T ⊆ Finset.range b) (h_sum : Summable fun (p : Nat.Primes) => |localDensityFactor (↑p) b T - 1|) : Multipliable fun (p : Nat.Primes) => localDensityFactor (↑p) b T

Multipliability from summability of deviations. Write μ_p = 1 + (μ_p - 1). If ∑|μ_p - 1| converges, then ∏ μ_p converges. Mathlib's Multipliable.of_norm_bounded or related lemmas apply when the factors are close to 1, which follows from sum_localDensityFactor_deviation_summable.

theorem LeanPool.DeadEnds.jointSquarefreeDensity_multipliable (b : ℕ) (hb : 2 ≤ b) (T : Finset ℕ) (hT : T ⊆ Finset.range b) : Multipliable fun (p : Nat.Primes) => localDensityFactor (↑p) b T

theorem LeanPool.DeadEnds.multipliable_of_deviation_summable_subtype (b : ℕ) (_hb : 2 ≤ b) (T : Finset ℕ) (_hT : T ⊆ Finset.range b) (U : Set Nat.Primes) (h_sum : Summable fun (p : ↑U) => |localDensityFactor (↑↑↑p) b T - 1|) : Multipliable fun (p : ↑U) => localDensityFactor (↑↑↑p) b T

theorem LeanPool.DeadEnds.multipliable_compl_of_multipliable (b : ℕ) (hb : 2 ≤ b) (T : Finset ℕ) (hT : T ⊆ Finset.range b) (S : Finset Nat.Primes) : Multipliable ((fun (p : Nat.Primes) => localDensityFactor (↑p) b T) ∘ Subtype.val)

theorem LeanPool.DeadEnds.tprod_compl_le_one (b : ℕ) (_hb : 2 ≤ b) (T : Finset ℕ) (_hT : T ⊆ Finset.range b) (S : Finset Nat.Primes) : ∏' (x : { p : Nat.Primes // p ∉ S }), localDensityFactor (↑↑x) b T ≤ 1