Helper lemmas for inclusion-exclusion

noncomputable def LeanPool.DeadEnds.sqfreeIndicator (n : ℕ) : ℝ

Indicator function for squarefree: returns 1 if squarefree, 0 otherwise

Equations

• LeanPool.DeadEnds.sqfreeIndicator n = if Squarefree n then 1 else 0

noncomputable def LeanPool.DeadEnds.shiftSqfreeIndicator (b N d : ℕ) : ℝ

Indicator function for "bN+d is squarefree"

Equations

• LeanPool.DeadEnds.shiftSqfreeIndicator b N d = if Squarefree (b * N + d) then 1 else 0

theorem LeanPool.DeadEnds.sum_over_subsets_containing_x (s : Finset ℕ) (x : ℕ) (hx : x ∉ s) (a : ℕ → ℝ) : ∑ T ∈ s.powerset, (-1) ^ (insert x T).card * ∏ d ∈ insert x T, a d = -a x * ∑ T ∈ s.powerset, (-1) ^ T.card * ∏ d ∈ T, a d

theorem LeanPool.DeadEnds.prod_one_sub_eq_sum_powerset (U : Finset ℕ) (a : ℕ → ℝ) : ∏ d ∈ U, (1 - a d) = ∑ T ∈ U.powerset, (-1) ^ T.card * ∏ d ∈ T, a d

theorem LeanPool.DeadEnds.deadEnd_indicator_eq (b N : ℕ) (hN : 1 ≤ N) : (if IsBaseBDeadEnd b N then 1 else 0) = sqfreeIndicator N * ∏ d ∈ Finset.range b, (1 - shiftSqfreeIndicator b N d)

theorem LeanPool.DeadEnds.countBaseBDeadEnds_as_sum (b X : ℕ) (_hb : 0 < b) : ↑(countBaseBDeadEnds b X) = ∑ N ∈ Finset.Icc 1 X, sqfreeIndicator N * ∏ d ∈ Finset.range b, (1 - shiftSqfreeIndicator b N d)

theorem LeanPool.DeadEnds.indicator_conjunction_eq_prod (b N : ℕ) (T : Finset ℕ) : (if Squarefree N ∧ ∀ d ∈ T, Squarefree (b * N + d) then 1 else 0) = sqfreeIndicator N * ∏ d ∈ T, shiftSqfreeIndicator b N d

theorem LeanPool.DeadEnds.countJointSquarefree_as_sum (b X : ℕ) (T : Finset ℕ) : ↑(countJointSquarefree b T X) = ∑ N ∈ Finset.Icc 1 X, sqfreeIndicator N * ∏ d ∈ T, shiftSqfreeIndicator b N d

theorem LeanPool.DeadEnds.dead_end_count_inclusion_exclusion (b : ℕ) (_hb : 2 ≤ b) (X : ℕ) : ↑(countBaseBDeadEnds b X) = ∑ T ∈ (Finset.range b).powerset, (-1) ^ T.card * ↑(countJointSquarefree b T X)

Finite inclusion-exclusion for dead end counting. For each fixed X, the count of dead ends equals the alternating sum over subsets T: #{N ≤ X : dead end} = ∑_{T ⊆ Finset.range b} (-1) ^ |T| · #{N ≤ X : N sf ∧ ∀d∈T, bN+d sf} This is the finite Bonferroni identity: for events A_d = "bN+d is squarefree", #{sf N : all A_d fail} = ∑_T (-1) ^ |T| #{sf N : ∀d∈T, A_d holds}. Mathlib has Finset.sum_powerset_neg_one_pow_card for this pattern.

theorem LeanPool.DeadEnds.alternating_sum_tendsto (b : ℕ) (_hb : 2 ≤ b) (h_tendsto : ∀ T ∈ (Finset.range b).powerset, Filter.Tendsto (fun (X : ℕ) => ↑(countJointSquarefree b T X) / ↑X) Filter.atTop (nhds (jointSquarefreeDensity b T))) : Filter.Tendsto (fun (X : ℕ) => ∑ T ∈ (Finset.range b).powerset, (-1) ^ T.card * (↑(countJointSquarefree b T X) / ↑X)) Filter.atTop (nhds (explicitDensityFormula b))

Tendsto of alternating sums given Tendsto of each term. If for each T ⊆ Finset.range b, the ratio (countJointSquarefree b T X)/X → α(b,T), then the alternating sum ∑_T (-1) ^ |T| · (countJointSquarefree b T X)/X converges to ∑_T (-1) ^ |T| · α(b,T) = explicitDensityFormula b. This uses that Filter.Tendsto is preserved under finite sums: Filter.Tendsto.sum : ∀ (hf : ∀ i ∈ s, Tendsto (f i) l (nhds (a i))), Tendsto (fun x => ∑ i ∈ s, f i x) l (nhds (∑ i ∈ s, a i))

theorem LeanPool.DeadEnds.sum_div_eq_div_sum (b X : ℕ) (_hX : 0 < X) : ∑ T ∈ (Finset.range b).powerset, (-1) ^ T.card * (↑(countJointSquarefree b T X) / ↑X) = (∑ T ∈ (Finset.range b).powerset, (-1) ^ T.card * ↑(countJointSquarefree b T X)) / ↑X

Rewriting the sum: factor out division by X. ∑_T (-1) ^ |T| · count(T,X) / X = (∑_T (-1) ^ |T| · count(T,X)) / X when X ≠ 0. Uses basic algebra: ∑_i (a_i / c) = (∑_i a_i) / c for c ≠ 0.

Main theorems

theorem LeanPool.DeadEnds.dead_end_tendsto_explicit_formula (b : ℕ) (hb : 2 ≤ b) : Filter.Tendsto (fun (X : ℕ) => ↑(countBaseBDeadEnds b X) / ↑X) Filter.atTop (nhds (explicitDensityFormula b))

The base-b dead-end counting ratios tend to the explicit inclusion-exclusion density.

theorem LeanPool.DeadEnds.baseBDeadEnd_density_exists (b : ℕ) (hb : 2 ≤ b) : ∃ (D : ℝ), HasAsymptoticDensity b D

theorem LeanPool.DeadEnds.baseBDeadEnd_density_unique (b : ℕ) (D₁ D₂ : ℝ) (h₁ : HasAsymptoticDensity b D₁) (h₂ : HasAsymptoticDensity b D₂) : D₁ = D₂

noncomputable def LeanPool.DeadEnds.baseBDeadEndDensity (b : ℕ) (hb : 2 ≤ b) : ℝ

The asymptotic density D_b of base-b dead ends, defined (when b ≥ 2) as the unique limit guaranteed by baseBDeadEnd_density_exists.

Equations

• LeanPool.DeadEnds.baseBDeadEndDensity b hb = Classical.choose ⋯

theorem LeanPool.DeadEnds.baseBDeadEndDensity_spec (b : ℕ) (hb : 2 ≤ b) : HasAsymptoticDensity b (baseBDeadEndDensity b hb)

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

theorem LeanPool.DeadEnds.jointSquarefreeDensity_is_asymptotic_density (b : ℕ) (hb : 2 ≤ b) (T : Finset ℕ) (hT : T ⊆ Finset.range b) : have countJoint := fun (X : ℕ) => {N ∈ Finset.Icc 1 X | Squarefree N ∧ ∀ d ∈ T, Squarefree (b * N + d)}.card; Filter.Tendsto (fun (X : ℕ) => ↑(countJoint X) / ↑X) Filter.atTop (nhds (jointSquarefreeDensity b T))

theorem LeanPool.DeadEnds.baseBDeadEnd_density_formula (b : ℕ) (hb : 2 ≤ b) : baseBDeadEndDensity b hb = explicitDensityFormula b

theorem LeanPool.DeadEnds.explicitDensityFormula_correct (b : ℕ) (hb : 2 ≤ b) : HasAsymptoticDensity b (explicitDensityFormula b)