Hit mass and final reductions

This file develops the ENNReal mass-flow layer behind the Markov-chain argument. It defines exact-step arrival mass, surviving mass before the first hit of a set A, and the total first-hit mass of A.

The central estimate is a telescope: if the restricted initial mass is at most 1 and each row of the transition kernel has total mass at most 1, then the total first-hit mass of A is at most 1. For primitive A, this is the visit-mass inequality used in the final argument, because finite paths in the multiplicative chain can meet A at most once.

Main definitions

• initialMass
• transitionKernel
• arrivalMass
• survivingArrivalMass
• firstHitMassAtStep
• visitMass

Main statements

• MarkovLayer.kernelRowBound
• tsum_initialMass_eq_one
• visitMass_le_of_bounds
• PrimitiveSet.summable_indicator_visitProbability_and_tsum_le_one_of_visitMass_le_one

noncomputable def PrimitiveSetsAboveX.initialMass (x Y n : ℕ) : ENNReal

The normalized initial mass restricted to the state space n ≥ x.

Equations

• PrimitiveSetsAboveX.initialMass x Y n = ENNReal.ofReal (if x ≤ n then PrimitiveSetsAboveX.initialDistribution x Y n else 0)

noncomputable def PrimitiveSetsAboveX.transitionKernel (x Y m n : ℕ) : ENNReal

The transition kernel on states n ≥ x, viewed as an ENNReal-valued mass function.

The state m can send mass to n only when m ≥ x, m ∣ n, and the quotient n / m is a valid jump factor q ≥ Y.

Equations

• PrimitiveSetsAboveX.transitionKernel x Y m n = if x ≤ m ∧ m ∣ n ∧ Y ≤ n / m then ENNReal.ofReal (PrimitiveSetsAboveX.transitionWeight Y m (n / m)) else 0

noncomputable def PrimitiveSetsAboveX.arrivalMass {x Y : ℕ} (chain : MarkovLayer x Y) : ℕ → ℕ → ENNReal

Exact-step arrival mass at state n after k steps in the multiplicative chain.

Equations

• PrimitiveSetsAboveX.arrivalMass chain 0 x✝ = PrimitiveSetsAboveX.initialMass x Y x✝
• PrimitiveSetsAboveX.arrivalMass chain k.succ x✝ = ∑' (m : ℕ), PrimitiveSetsAboveX.arrivalMass chain k m * PrimitiveSetsAboveX.transitionKernel x Y m x✝

noncomputable def PrimitiveSetsAboveX.survivingArrivalMass {x Y : ℕ} (chain : MarkovLayer x Y) (A : Set ℕ) : ℕ → ℕ → ENNReal

The surviving mass at state n after k steps, obtained by discarding every path that has already hit A.

Equations

• One or more equations did not get rendered due to their size.
• PrimitiveSetsAboveX.survivingArrivalMass chain A 0 x✝ = Aᶜ.indicator (PrimitiveSetsAboveX.initialMass x Y) x✝

noncomputable def PrimitiveSetsAboveX.firstHitMassAtStep {x Y : ℕ} (chain : MarkovLayer x Y) (A : Set ℕ) : ℕ → ENNReal

The mass that first hits A exactly at step k.

For k = 0 this is the initial mass already inside A, and for k + 1 it is the mass propagated from the surviving mass at step k into A.

Equations

• One or more equations did not get rendered due to their size.
• PrimitiveSetsAboveX.firstHitMassAtStep chain A 0 = ∑' (n : ℕ), A.indicator (PrimitiveSetsAboveX.initialMass x Y) n

noncomputable def PrimitiveSetsAboveX.visitMass {x Y : ℕ} (chain : MarkovLayer x Y) (A : Set ℕ) : ENNReal

The total visit mass of A, counted by the first hit of A along each path. For primitive sets, this agrees with the usual total mass of visits because finite multiplicative paths meet A at most once.

Equations

• PrimitiveSetsAboveX.visitMass chain A = ∑' (k : ℕ), PrimitiveSetsAboveX.firstHitMassAtStep chain A k

theorem PrimitiveSetsAboveX.MarkovLayer.kernelRowBound {x Y : ℕ} (chain : MarkovLayer x Y) ⦃m : ℕ⦄ : x ≤ m → ∑' (n : ℕ), transitionKernel x Y m n ≤ 1

The real row-sum bound ∑_{q ≥ Y} p(m, mq) ≤ 1 transfers directly to the ENNReal kernel transitionKernel, which is the form needed in the first-hit mass argument.

theorem PrimitiveSetsAboveX.tsum_initialMass_eq_one {x Y : ℕ} (hB : 0 < normalizationConstant x Y) : ∑' (n : ℕ), initialMass x Y n = 1

Once B_x > 0, the restricted initial mass has total mass exactly 1.

theorem PrimitiveSetsAboveX.PrimitiveSet.summable_indicator_visitProbability_and_tsum_le_one_of_visitMass_le_one {x Y : ℕ} (chain : MarkovLayer x Y) {A : Set ℕ} (hA : PrimitiveSet A) (hAx : A ⊆ Set.Ici x) (hx : 2 ≤ x) (hY : 2 ≤ Y) (hB : 0 < normalizationConstant x Y) (hVisitMass : visitMass chain A ≤ 1) : Summable (A.indicator chain.visitProbability) ∧ ∑' (n : ℕ), A.indicator chain.visitProbability n ≤ 1

If the first-hit mass budget of a primitive set A is at most 1, then the real indicator series of visit probabilities is summable and its total mass is at most 1.

theorem PrimitiveSetsAboveX.visitMass_le_of_bounds {x Y : ℕ} (chain : MarkovLayer x Y) (A : Set ℕ) (hx : 0 < x) (hY : 1 ≤ Y) (hinit : ∑' (n : ℕ), initialMass x Y n ≤ 1) (hkernel : ∀ ⦃m : ℕ⦄, x ≤ m → ∑' (n : ℕ), transitionKernel x Y m n ≤ 1) : visitMass chain A ≤ 1

If the initial mass is at most 1 and every kernel row is sub-Markov, then the total first-hit mass is at most 1.