Core definitions for the normalization constant

This file contains the shared decomposition of the entry weights and normalization constant into their small-prime and first-entry pieces, together with the structural reindexing lemmas used by the two separate estimate files.

Main definitions

• entryWeightFactor
• smallPrimeDivisorSum
• firstEntryDivisorSum
• normalizationSmallPrimePart
• normalizationFirstEntryPart

noncomputable def PrimitiveSetsAboveX.entryWeightFactor (n : ℕ) : ℝ

The common prefactor 1 / (n log^2 n) in the entry weights.

Equations

• PrimitiveSetsAboveX.entryWeightFactor n = 1 / (↑n * Real.log ↑n ^ 2)

noncomputable def PrimitiveSetsAboveX.smallPrimeDivisorSum (Y n : ℕ) : ℝ

The small-prime-power divisor sum appearing in b_x(n).

Equations

• PrimitiveSetsAboveX.smallPrimeDivisorSum Y n = ∑ q ∈ n.divisors with q < Y, ArithmeticFunction.vonMangoldt q

noncomputable def PrimitiveSetsAboveX.firstEntryDivisorSum (x Y n : ℕ) : ℝ

The first-entry divisor sum appearing in b_x(n).

Equations

• PrimitiveSetsAboveX.firstEntryDivisorSum x Y n = ∑ q ∈ n.divisors with Y ≤ q ∧ n / q < x, ArithmeticFunction.vonMangoldt q

noncomputable def PrimitiveSetsAboveX.smallPrimeEntryWeight (Y n : ℕ) : ℝ

The contribution to b_x(n) from divisors q < Y.

Equations

• PrimitiveSetsAboveX.smallPrimeEntryWeight Y n = PrimitiveSetsAboveX.entryWeightFactor n * PrimitiveSetsAboveX.smallPrimeDivisorSum Y n

noncomputable def PrimitiveSetsAboveX.firstEntryEntryWeight (x Y n : ℕ) : ℝ

The contribution to b_x(n) from divisors q ≥ Y with n / q < x.

Equations

• PrimitiveSetsAboveX.firstEntryEntryWeight x Y n = PrimitiveSetsAboveX.entryWeightFactor n * PrimitiveSetsAboveX.firstEntryDivisorSum x Y n

noncomputable def PrimitiveSetsAboveX.normalizationSmallPrimePart (x Y n : ℕ) : ℝ

The small-prime-power summand in the normalization constant B_x.

Equations

• PrimitiveSetsAboveX.normalizationSmallPrimePart x Y n = if x ≤ n then PrimitiveSetsAboveX.smallPrimeEntryWeight Y n else 0

noncomputable def PrimitiveSetsAboveX.normalizationFirstEntryPart (x Y n : ℕ) : ℝ

The first-entry summand in the normalization constant B_x.

Equations

• PrimitiveSetsAboveX.normalizationFirstEntryPart x Y n = if x ≤ n then PrimitiveSetsAboveX.firstEntryEntryWeight x Y n else 0

theorem PrimitiveSetsAboveX.entryWeight_eq_smallPrimeEntryWeight_add_firstEntryEntryWeight (x Y n : ℕ) : entryWeight x Y n = smallPrimeEntryWeight Y n + firstEntryEntryWeight x Y n

b_x(n) splits into the small-prime-power and first-entry contributions.

theorem PrimitiveSetsAboveX.entryWeight_add_filtered_vonMangoldt_eq_entryWeightFactor_sum_divisors (x Y n : ℕ) : (entryWeight x Y n + ∑ q ∈ n.divisors, if Y ≤ q ∧ x ≤ n / q then entryWeightFactor n * ArithmeticFunction.vonMangoldt q else 0) = entryWeightFactor n * ∑ q ∈ n.divisors, ArithmeticFunction.vonMangoldt q

Adding the remaining divisor contribution to b_x(n) recovers the full weighted divisor sum.

theorem PrimitiveSetsAboveX.smallPrimeEntryWeight_nonneg (Y n : ℕ) : 0 ≤ smallPrimeEntryWeight Y n

The small-prime contribution to b_x(n) is nonnegative.

theorem PrimitiveSetsAboveX.firstEntryEntryWeight_nonneg (x Y n : ℕ) : 0 ≤ firstEntryEntryWeight x Y n

The first-entry contribution to b_x(n) is nonnegative.

theorem PrimitiveSetsAboveX.le_mul_entryThreshold (x Y m : ℕ) (hm : 0 < m) : x ≤ m * entryThreshold x Y m

The first-entry threshold always lands in the admissible range x ≤ m * q, since it dominates the ceiling quotient x ⌈/⌉ m.

theorem PrimitiveSetsAboveX.firstEntryTailApproximation {Y : ℕ} (hY : 2 ≤ Y) : ∃ (C : ℝ), 0 < C ∧ ∀ {x m : ℕ}, 2 ≤ x → 1 ≤ m → m < x → |firstEntryTail x Y m - 1 / Real.log ↑x| ≤ C / Real.log ↑x ^ 2

For fixed Y ≥ 2, the first-entry tail at the faithful cutoff entryThreshold x Y m approximates 1 / log x with a uniform log⁻² x error, uniformly for all parent states 1 ≤ m < x.

theorem PrimitiveSetsAboveX.abs_sum_Icc_inv_sub_log_le_one (x : ℕ) (hx : 1 ≤ x) : |∑ m ∈ Finset.Icc 1 (x - 1), 1 / ↑m - Real.log ↑x| ≤ 1

Equivalently, the finite reciprocal sum ∑_{m < x} 1 / m is within 1 of log x.

theorem PrimitiveSetsAboveX.sum_range_normalizationSmallPrimePart_eq (N x Y : ℕ) : ∑ n ∈ Finset.range N, normalizationSmallPrimePart x Y n = ∑ q ∈ Finset.range N, ∑ m ∈ Finset.range N, if 0 < q ∧ 0 < m ∧ q * m < N ∧ q < Y ∧ x ⌈/⌉ q ≤ m then ArithmeticFunction.vonMangoldt q / ↑q * (1 / (↑m * Real.log ↑(m * q) ^ 2)) else 0

The finite prefix of the small-prime contribution reindexes as a sum over q < Y and inner m-tails, with the exact lower cutoff x ⌈/⌉ q.

theorem PrimitiveSetsAboveX.tsum_firstEntryPairWeight_fiber_prod {x Y n : ℕ} (hx : 1 ≤ x) : ∑' (p : ↑((fun (mq : ℕ × ℕ) => mq.1 * mq.2) ⁻¹' {n})), firstEntryPairWeight x Y ↑p = normalizationFirstEntryPart x Y n

Reindexing the product fiber of firstEntryPairWeight recovers the first-entry normalization summand, including the zero fiber.

theorem PrimitiveSetsAboveX.normalizationConstant_eq_tsum_parts (x Y : ℕ) : normalizationConstant x Y = ∑' (n : ℕ), (normalizationSmallPrimePart x Y n + normalizationFirstEntryPart x Y n)

The normalization constant B_x is exactly the sum of its small-prime and first-entry contributions.