Markov-chain lemmas for primitive sets above x

This file proves the main analytic estimates for the Markov-chain construction: the asymptotic control of R_Y(m), the eventual sub-Markov bound on the transition rows, the eventual estimate for the normalization constant B_x, and the explicit closed formula for the visiting probabilities.

Main statements

• subMarkovRowSumBound
• normalizationEstimate
• visitProbabilityFormula

theorem PrimitiveSetsAboveX.tsum_eq_sum_divisors_of_nondivisors_zero {α : Type u_1} [AddCommMonoid α] [TopologicalSpace α] {n : ℕ} (hn : 0 < n) (f : ℕ → α) (hf : ∀ (q : ℕ), ¬q ∣ n → f q = 0) : ∑' (q : ℕ), f q = n.divisors.sum f

If a summand vanishes off the divisors of n, its infinite sum is the finite sum over n.divisors.

theorem PrimitiveSetsAboveX.tsum_eq_sum_divisors_of_dvd_and {α : Type u_1} [AddCommMonoid α] [TopologicalSpace α] {n : ℕ} (hn : 0 < n) (P : ℕ → Prop) [DecidablePred P] (f : ℕ → α) : (∑' (q : ℕ), if q ∣ n ∧ P q then f q else 0) = ∑ q ∈ n.divisors, if P q then f q else 0

If a divisor condition is bundled into the summand, the tsum reduces to the finite divisor sum with that condition removed.

theorem PrimitiveSetsAboveX.subMarkovRowSumBound : ∃ (C : ℝ), 0 < C ∧ ∀ ⦃Y : ℕ⦄, Real.exp (2 * C) < ↑Y → ∃ (x₀ : ℕ), Y ≤ x₀ ∧ ∀ ⦃m : ℕ⦄, x₀ ≤ m → ∑' (q : ℕ), transitionWeight Y m q ≤ 1

Choosing the cutoff Y large enough makes every sufficiently late transition row sum at most 1, so the outgoing weights define an eventual sub-Markov chain.

theorem PrimitiveSetsAboveX.normalizationEstimate {Y : ℕ} (hY : 2 ≤ Y) : ∃ (C : ℝ), 0 < C ∧ ∃ (x₀ : ℕ), ∀ ⦃x : ℕ⦄, x₀ ≤ x → |normalizationConstant x Y - 1| ≤ C / Real.log ↑x

For each fixed Y ≥ 2, the normalizing constants satisfy the asymptotic estimate B_x = 1 + O(1 / log x).

theorem PrimitiveSetsAboveX.visitProbabilityRecurrence_sum_parents {x Y : ℕ} (chain : MarkovLayer x Y) {n : ℕ} (hxn : x ≤ n) (hn : 0 < n) : chain.visitProbability n = initialDistribution x Y n + ∑ m ∈ n.divisors, if x ≤ m ∧ Y ≤ n / m then chain.visitProbability m * transitionWeight Y m (n / m) else 0

Reindexing the last-jump recurrence by the parent state shows that only divisors m ∣ n can contribute to the probability of visiting n.

theorem PrimitiveSetsAboveX.lastJumpContribution_eq_of_formula {x Y : ℕ} (hx : 2 ≤ x) {n q : ℕ} (hq : q ∈ n.divisors) (hqx : Y ≤ q ∧ x ≤ n / q) {v : ℝ} (hvisit : v = 1 / (normalizationConstant x Y * (↑n / ↑q) * Real.log (↑n / ↑q))) : v * transitionWeight Y (n / q) q = 1 / normalizationConstant x Y * (1 / (↑n * Real.log ↑n ^ 2) * ArithmeticFunction.vonMangoldt q)

For a proper parent n / q, any last-jump term with the explicit parent value simplifies to the common factor (1 / B_x) * (Λ(q) / (n log^2 n)).

theorem PrimitiveSetsAboveX.formula_eq_initialDistribution_add_filteredVonMangoldt {x Y n : ℕ} : 1 / (normalizationConstant x Y * ↑n * Real.log ↑n) = initialDistribution x Y n + 1 / normalizationConstant x Y * ∑ q ∈ n.divisors, if Y ≤ q ∧ x ≤ n / q then 1 / (↑n * Real.log ↑n ^ 2) * ArithmeticFunction.vonMangoldt q else 0

The divisor decomposition of log n rewrites the explicit target formula as the normalized initial mass plus the filtered von Mangoldt divisor sum.

theorem PrimitiveSetsAboveX.explicitFormula_eq_recurrence_rhs {x Y n : ℕ} (hx : 2 ≤ x) (hn : x ≤ n) {f : ℕ → ℝ} (hvisit : ∀ ⦃q : ℕ⦄, q ∈ n.divisors → Y ≤ q ∧ x ≤ n / q → q ≠ 1 → f (n / q) = 1 / (normalizationConstant x Y * (↑n / ↑q) * Real.log (↑n / ↑q))) : 1 / (normalizationConstant x Y * ↑n * Real.log ↑n) = initialDistribution x Y n + ∑' (q : ℕ), if Y ≤ q ∧ q ∣ n ∧ x ≤ n / q then f (n / q) * transitionWeight Y (n / q) q else 0

If every last-jump parent already has the explicit value 1 / (B_x n log n), then the recurrence right-hand side collapses to the closed formula for the visit probability at n.

theorem PrimitiveSetsAboveX.visitProbabilityFormula {x Y : ℕ} (chain : MarkovLayer x Y) (hx : 2 ≤ x) {n : ℕ} (hn : x ≤ n) : chain.visitProbability n = 1 / (normalizationConstant x Y * ↑n * Real.log ↑n)

The Markov layer visits each state n ≥ x with the explicit probability 1 / (B_x n log n). The lower bound 2 ≤ x guarantees that the logarithms in this formula are positive.

theorem PrimitiveSetsAboveX.visitProbability_nonneg {x Y : ℕ} (chain : MarkovLayer x Y) (hx : 2 ≤ x) (hB : 0 < normalizationConstant x Y) {n : ℕ} (hn : x ≤ n) : 0 ≤ chain.visitProbability n

Under the standing hypotheses 2 ≤ x and B_x > 0, the visiting probabilities are nonnegative on the state space n ≥ x.