Reference · Finite types, distributions and Markov chains
rainbow.math.finite.markov-geometric-decay
Geometric decay of total variation along kernel iterates. Brick 2 of the convergence half, built against the LANDED contraction inhabitant rather than an abstract premise: under normalized rows and a certified Dobrushin bound rho, the total variation between the n-th iterates of two equal-total-mass distributions is at most rho^n times the initial total variation. The induction step collapses one iterate through the total-variation congruence, applies the inhabitant at the iterated masses (equal total mass rides along by preservation), and folds the factor into the exact rational power. Native and axiom-free on D63.
markov/nnrat-kernel-iterate-total-variation-decay
markov/nnrat-kernel-iterate-total-variation-decay.{u} :
(S : Type u) (states : Finset S) (kernel : S → S → ℚ≥0) (rho : ℚ≥0)
(normalized : markov/nnrat-kernel-rows-normalized S states kernel)
(coefficient-bound : markov/signed-kernel-dobrushin-coefficient S states kernel ≤ signed/from-nnrat rho)
(left right : S → ℚ≥0)
(equal-total-mass : probability/nnrat-total-mass S states left = probability/nnrat-total-mass S states right)
(steps : ℕ)
→ markov/nnrat-total-variation S states (iterate₁) (iterate) ≤ nnrat/power rho steps · markov/nnrat-total-variation S states left right
where iterate := markov/nnrat-kernel-iterate S states kernel steps right
where iterate₁ := markov/nnrat-kernel-iterate S states kernel steps left= = nnrat/equivalent: equality of rational valuesFinset = finset-data/Finset· = nnrat/multiplyℕ = data/Natℚ≥0 = nnrat/NonnegativeRational≤ = nnrat/at-most