Rewriting the primitive weight using visit probabilities

This file records the exact algebraic bridge from the explicit visit-probability formula v_x(n) = 1 / (B_x n log n) to the weighted series identity f(A) = B_x * ∑_{n ∈ A} v_x(n), and packages the final deterministic reduction from a summable hit series to the logarithmic-series bound.

Main statements

• summable_indicatorLogSeries_and_tsum_le_of_hitMass

theorem PrimitiveSetsAboveX.summable_indicatorLogSeries_and_tsum_le_of_hitMass {x Y : ℕ} (chain : MarkovLayer x Y) (hx : 2 ≤ x) {A : Set ℕ} (hA : A ⊆ Set.Ici x) (hB : 0 < normalizationConstant x Y) (hHitSummable : Summable (A.indicator chain.visitProbability)) (hHit : ∑' (n : ℕ), A.indicator chain.visitProbability n ≤ 1) {C : ℝ} (hNorm : |normalizationConstant x Y - 1| ≤ C / Real.log ↑x) : Summable (A.indicator fun (m : ℕ) => 1 / (↑m * Real.log ↑m)) ∧ ∑' (m : ℕ), A.indicator (fun (k : ℕ) => 1 / (↑k * Real.log ↑k)) m ≤ 1 + C / Real.log ↑x

If the visit-probability series on A is summable and has total mass at most 1, then the logarithmic series on A is summable as well, and the normalization estimate converts this into the final upper bound for ∑_{n ∈ A} 1 / (n log n).