Basic definitions for primitive sets above x

This file introduces the core objects used throughout the development: the arithmetic sums appearing in the analytic estimates, the entry weights and normalization data b_x, B_x, and μ_x, and the abstract Markov-layer interface used for the visit-probability argument.

Main definitions

• PrimitiveSet
• mertensPartialSum
• tailSum
• ry
• entryWeight
• normalizationConstant
• initialDistribution
• MarkovLayer

def PrimitiveSetsAboveX.PrimitiveSet (A : Set ℕ) : Prop

The primitive-set predicate used throughout the local development.

Equations

• PrimitiveSetsAboveX.PrimitiveSet A = ∀ ⦃m n : ℕ⦄, m ∈ A → n ∈ A → m ∣ n → m = n

noncomputable def PrimitiveSetsAboveX.mertensPartialSum (t : ℕ) : ℝ

Partial sums of Λ(q) / q.

Equations

• PrimitiveSetsAboveX.mertensPartialSum t = ∑ q ∈ Finset.Icc 1 t, ArithmeticFunction.vonMangoldt q / ↑q

noncomputable def PrimitiveSetsAboveX.tailSum (m y : ℕ) : ℝ

The logarithmic tail sum T(m, y) used in the normalization estimates.

Equations

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

noncomputable def PrimitiveSetsAboveX.ry (Y m : ℕ) : ℝ

The quantity R_Y(m) introduced in the proof of the main theorem.

Equations

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

noncomputable def PrimitiveSetsAboveX.transitionWeight (Y m q : ℕ) : ℝ

The transition weight p(m, mq) of the sub-Markov chain.

Equations

• PrimitiveSetsAboveX.transitionWeight Y m q = if Y ≤ q then Real.log ↑m / Real.log ↑(m * q) ^ 2 * (ArithmeticFunction.vonMangoldt q / ↑q) else 0

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

The entry weight b_x(n) used to define the initial distribution of the chain.

Equations

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

noncomputable def PrimitiveSetsAboveX.normalizationConstant (x Y : ℕ) : ℝ

The normalizing constant B_x.

Equations

• PrimitiveSetsAboveX.normalizationConstant x Y = ∑' (n : ℕ), if x ≤ n then PrimitiveSetsAboveX.entryWeight x Y n else 0

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

The normalized initial distribution μ_x(n) = b_x(n) / B_x.

Equations

• PrimitiveSetsAboveX.initialDistribution x Y n = PrimitiveSetsAboveX.entryWeight x Y n / PrimitiveSetsAboveX.normalizationConstant x Y

structure PrimitiveSetsAboveX.MarkovLayer (x Y : ℕ) : Type

An abstract sub-Markov layer on the state space n ≥ x, together with a candidate visit-probability function satisfying the last-jump recurrence.

• transitionSubMarkov ⦃m : ℕ⦄ : x ≤ m → ∑' (q : ℕ), transitionWeight Y m q ≤ 1

  The transition weights satisfy the required sub-Markov row-sum bound.

• visitProbability : ℕ → ℝ

  The probability that the chain ever visits n when started from μ_x.

• visitProbabilityRecurrence ⦃n : ℕ⦄ : x ≤ n → self.visitProbability n = initialDistribution x Y n + ∑' (q : ℕ), if Y ≤ q ∧ q ∣ n ∧ x ≤ n / q then self.visitProbability (n / q) * transitionWeight Y (n / q) q else 0

  The last-jump recurrence for the visiting probabilities.