LeanPool.DeadEnds.InclusionExclusion

Helper lemmas for inclusion-exclusion #

source

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

Instances For

source

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

Instances For

source

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

source

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

source

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)

source

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)

source

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

source

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

source

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.

source

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))

source

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.