First-entry row data

This file packages the row-wise data for the first-entry contribution to the normalization constant. It introduces the threshold selecting admissible first jumps from a parent state m, the resulting tail sum, and the pairwise weights used later in the fiberwise reindexing of B_x.

Main definitions

• entryThreshold
• firstEntryTail
• firstEntryPairWeight

def PrimitiveSetsAboveX.entryThreshold (x Y m : ℕ) : ℕ

The least threshold satisfying both q ≥ Y and x ≤ m * q.

Equations

• PrimitiveSetsAboveX.entryThreshold x Y m = max Y (x ⌈/⌉ m)

noncomputable def PrimitiveSetsAboveX.firstEntryTail (x Y m : ℕ) : ℝ

The first-entry tail sum starting from a parent state m.

Equations

• PrimitiveSetsAboveX.firstEntryTail x Y m = ∑' (q : ℕ), if PrimitiveSetsAboveX.entryThreshold x Y m ≤ q then ArithmeticFunction.vonMangoldt q / (↑q * Real.log ↑(m * q) ^ 2) else 0

noncomputable def PrimitiveSetsAboveX.firstEntryPairWeight (x Y : ℕ) (mq : ℕ × ℕ) : ℝ

The pairwise weight indexed by a parent state m and jump factor q for the first-entry contribution to B_x.

Equations

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

theorem PrimitiveSetsAboveX.entryThreshold_le_iff (x Y m q : ℕ) (hm : 0 < m) : entryThreshold x Y m ≤ q ↔ Y ≤ q ∧ x ≤ m * q

The lower-threshold condition is exactly the conjunction q ≥ Y and x ≤ m * q.

theorem PrimitiveSetsAboveX.firstEntryPairWeight_eq {x Y m q : ℕ} (hm1 : 1 ≤ m) (hmx : m < x) : firstEntryPairWeight x Y (m, q) = 1 / ↑m * if entryThreshold x Y m ≤ q then ArithmeticFunction.vonMangoldt q / (↑q * Real.log ↑(m * q) ^ 2) else 0

For a parent state already known to satisfy 1 ≤ m < x, the pairwise first-entry weight is the corresponding scaled tail summand.

theorem PrimitiveSetsAboveX.firstEntryPairWeight_row (x Y m : ℕ) : (fun (q : ℕ) => firstEntryPairWeight x Y (m, q)) = if 1 ≤ m ∧ m < x then fun (q : ℕ) => 1 / ↑m * if entryThreshold x Y m ≤ q then ArithmeticFunction.vonMangoldt q / (↑q * Real.log ↑(m * q) ^ 2) else 0 else fun (x : ℕ) => 0

For a fixed parent state m, the first-entry row is either the scaled tail summand row when 1 ≤ m < x, or identically zero otherwise.