Reference · Finite types, distributions and Markov chains

rainbow.math.finite.markov-hastings-flow

Finite types, distributions and Markov chainssrc/rainbow/math/finite/markov_hastings_flow.clj11 definitions, 27 theorems

General, division-free Hastings accepted-flow certificates. For a target mass pi and proposal kernel q, the accepted directed flow is min(pi(x) q(x,y), pi(y) q(y,x)). This quantity is symmetric without division, positivity side conditions, or a special case for zero proposal mass. A candidate Markov kernel realizes the Hastings flow when its target-weighted flow is the accepted flow plus an explicitly supplied correction. If that correction is symmetric, the realized kernel satisfies detailed balance; if its rows and the target are normalized, the target is stationary. The exact ratio acceptance min(forward,reverse)/forward realizes that accepted flow for every native nonnegative rational, including the zero-forward case without using an invalid inverse law at zero. For a normalized finite proposal row, the accepted row is bounded by one and its exact rejection mass is the quotient-safe distance from that total to one; accepted mass plus rejection mass is exactly one. A certified Boolean equality decision constructs the canonical diagonal rejection placement. When its finite carrier is exhaustive, the placement has exactly the computed rejection mass in every row, so the resulting canonical kernel is normalized, reversible, and stationary under the stated target and proposal normalization premises. This remains a theorem about mathematical kernels, not an executable sampler. Native, kernel-checked, and axiom-free on D63.

Depends onmath.rational.nnrat.minmaxmath.rational.nnrat.metric-separationmath.finite.markov-stationarity

mcmc/nnrat-hastings-accepted-flow.{u} :
  (S : Type u) (target : S → ℚ≥0) (proposal : S → S → ℚ≥0) (x₁ x₂ : S)
  → ℚ≥0

mcmc/nnrat-hastings-ratio-acceptance :
  (x₁ x₂ : ℚ≥0)
  → ℚ≥0

mcmc/nnrat-hastings-accepted-transition.{u} :
  (S : Type u) (target : S → ℚ≥0) (proposal : S → S → ℚ≥0) (x₁ x₂ : S)
  → ℚ≥0

mcmc/nnrat-hastings-rejection-mass.{u} :
  (S : Type u) (states : Finset S) (target : S → ℚ≥0) (proposal : S → S → ℚ≥0) (x₁ : S)
  → ℚ≥0

mcmc/nnrat-hastings-completed-kernel.{u} :
  (S : Type u) (states : Finset S) (target : S → ℚ≥0) (proposal placement : S → S → ℚ≥0)
  (x₁ x₂ : S)
  → ℚ≥0

mcmc/nnrat-hastings-rejection-correction.{u} :
  (S : Type u) (target : S → ℚ≥0) (placement : S → S → ℚ≥0) (x₁ x₂ : S)
  → ℚ≥0

mcmc/nnrat-off-diagonal-zero.{u} :
  (S : Type u) (placement : S → S → ℚ≥0)
  → Prop

mcmc/nnrat-hastings-diagonal-rejection-placement.{u} :
  (S : Type u) (states : Finset S) (target : S → ℚ≥0) (proposal : S → S → ℚ≥0)
  (decision : S → S → data/Bool) (x₁ x₂ : S)
  → ℚ≥0

mcmc/nnrat-hastings-canonical-kernel.{u} :
  (S : Type u) (states : Finset S) (target : S → ℚ≥0) (proposal : S → S → ℚ≥0)
  (decision : S → S → data/Bool) (x₁ x₂ : S)
  → ℚ≥0

mcmc/nnrat-symmetric-flow.{u} :
  (S : Type u) (flow : S → S → ℚ≥0)
  → Prop

mcmc/nnrat-hastings-kernel-realization.{u} :
  (S : Type u) (target : S → ℚ≥0) (proposal kernel correction : S → S → ℚ≥0)
  → Prop

nnrat/min-commutative :
  (left right : ℚ≥0)
  → minmax/min left right = minmax/min right left

mcmc/nnrat-hastings-accepted-flow-symmetric.{u} :
  (S : Type u) (target : S → ℚ≥0) (proposal : S → S → ℚ≥0) (left right : S)
  → flow left right = flow right left
  where flow := mcmc/nnrat-hastings-accepted-flow S target proposal

mcmc/nnrat-positive-hastings-ratio-realizes-accepted-flow :
  (numerator-predecessor denominator-predecessor : ℕ) (reverse : ℚ≥0)
  → make · mcmc/nnrat-hastings-ratio-acceptance (make) reverse = minmax/min (make) reverse
  where make := nnrat/make (data/succ numerator-predecessor) denominator-predecessor

mcmc/nnrat-zero-hastings-ratio-realizes-accepted-flow :
  (denominator-predecessor : ℕ) (reverse : ℚ≥0)
  → nnrat/make 0 denominator-predecessor · mcmc/nnrat-hastings-ratio-acceptance (nnrat/make 0 denominator-predecessor) reverse = minmax/min (nnrat/make 0 denominator-predecessor) reverse

mcmc/nnrat-made-hastings-ratio-realizes-accepted-flow :
  (numerator denominator-predecessor : ℕ) (reverse : ℚ≥0)
  → make · mcmc/nnrat-hastings-ratio-acceptance (make) reverse = minmax/min (make) reverse
  where make := nnrat/make numerator denominator-predecessor

mcmc/nnrat-hastings-ratio-realizes-accepted-flow :
  (forward reverse : ℚ≥0)
  → forward · mcmc/nnrat-hastings-ratio-acceptance forward reverse = minmax/min forward reverse

mcmc/nnrat-positive-hastings-ratio-acceptance-at-most-one :
  (numerator-predecessor denominator-predecessor : ℕ) (reverse : ℚ≥0)
  → mcmc/nnrat-hastings-ratio-acceptance (make) reverse ≤ 1
  where make := nnrat/make (data/succ numerator-predecessor) denominator-predecessor

mcmc/nnrat-zero-hastings-ratio-acceptance-at-most-one :
  (denominator-predecessor : ℕ) (reverse : ℚ≥0)
  → mcmc/nnrat-hastings-ratio-acceptance (nnrat/make 0 denominator-predecessor) reverse ≤ 1

mcmc/nnrat-made-hastings-ratio-acceptance-at-most-one :
  (numerator denominator-predecessor : ℕ) (reverse : ℚ≥0)
  → mcmc/nnrat-hastings-ratio-acceptance (make) reverse ≤ 1
  where make := nnrat/make numerator denominator-predecessor

mcmc/nnrat-hastings-ratio-acceptance-at-most-one :
  (forward reverse : ℚ≥0)
  → mcmc/nnrat-hastings-ratio-acceptance forward reverse ≤ 1

mcmc/nnrat-hastings-accepted-transition-at-most-proposal.{u} :
  (S : Type u) (target : S → ℚ≥0) (proposal : S → S → ℚ≥0) (left right : S)
  → mcmc/nnrat-hastings-accepted-transition S target proposal left right ≤ proposal left right

mcmc/nnrat-hastings-accepted-transition-realizes-flow.{u} :
  (S : Type u) (target : S → ℚ≥0) (proposal : S → S → ℚ≥0) (left right : S)
  → target left · mcmc/nnrat-hastings-accepted-transition S target proposal left right = mcmc/nnrat-hastings-accepted-flow S target proposal left right

mcmc/nnrat-hastings-accepted-row-at-most-proposal-row.{u} :
  (S : Type u) (states : Finset S) (target : S → ℚ≥0) (proposal : S → S → ℚ≥0)
  (left : S)
  → probability/nnrat-total-mass S states (fun right => transition right) ≤ probability/nnrat-total-mass S states (proposal left)
  where transition := mcmc/nnrat-hastings-accepted-transition S target proposal left

mcmc/nnrat-hastings-accepted-row-at-most-one.{u} :
  (S : Type u) (states : Finset S) (target : S → ℚ≥0) (proposal : S → S → ℚ≥0)
  (proposal-normalized : markov/nnrat-kernel-rows-normalized S states proposal)
  (left : S)
  → probability/nnrat-total-mass S states (fun right => transition right) ≤ 1
  where transition := mcmc/nnrat-hastings-accepted-transition S target proposal left

mcmc/nnrat-hastings-accepted-row-plus-rejection-is-one.{u} :
  (S : Type u) (states : Finset S) (target : S → ℚ≥0) (proposal : S → S → ℚ≥0)
  (proposal-normalized : markov/nnrat-kernel-rows-normalized S states proposal)
  (left : S)
  → probability/nnrat-total-mass S states (fun right => transition right) + mcmc/nnrat-hastings-rejection-mass S states target proposal left = 1
  where transition := mcmc/nnrat-hastings-accepted-transition S target proposal left

mcmc/nnrat-hastings-completed-kernel-rows-normalized.{u} :
  (S : Type u) (states : Finset S) (target : S → ℚ≥0) (proposal placement : S → S → ℚ≥0)
  (proposal-normalized : normalized proposal)
  (placement-has-rejection-mass : ∀ (left : S), probability/nnrat-total-mass S states (placement left) = mcmc/nnrat-hastings-rejection-mass S states target proposal left)
  → normalized (kernel)
  where kernel := mcmc/nnrat-hastings-completed-kernel S states target proposal placement
  where normalized := markov/nnrat-kernel-rows-normalized S states

mcmc/nnrat-hastings-completed-kernel-realization.{u} :
  (S : Type u) (states : Finset S) (target : S → ℚ≥0) (proposal placement : S → S → ℚ≥0)
  → mcmc/nnrat-hastings-kernel-realization S target proposal (kernel) (correction)
  where correction := mcmc/nnrat-hastings-rejection-correction S target placement
  where kernel := mcmc/nnrat-hastings-completed-kernel S states target proposal placement

mcmc/nnrat-hastings-rejection-correction-symmetric-of-off-diagonal-zero.{u} :
  (S : Type u) (target : S → ℚ≥0) (placement : S → S → ℚ≥0)
  (equality-decidable : ∀ (left : S), ∀ (right : S), proposition/disjunction (left = right) (left = right → proposition/falsity))
  (off-diagonal : mcmc/nnrat-off-diagonal-zero S placement)
  → mcmc/nnrat-symmetric-flow S (correction)
  where correction := mcmc/nnrat-hastings-rejection-correction S target placement

mcmc/nnrat-hastings-realization-detailed-balance.{u} :
  (S : Type u) (target : S → ℚ≥0) (proposal kernel correction : S → S → ℚ≥0)
  (realized : mcmc/nnrat-hastings-kernel-realization S target proposal kernel correction)
  (correction-symmetric : mcmc/nnrat-symmetric-flow S correction)
  → markov/nnrat-detailed-balance S target kernel

mcmc/nnrat-hastings-realization-stationary.{u} :
  (S : Type u) (states : Finset S) (target : S → ℚ≥0)
  (proposal kernel correction : S → S → ℚ≥0)
  (target-normalized : probability/nnrat-total-mass S states target = 1)
  (kernel-normalized : markov/nnrat-kernel-rows-normalized S states kernel)
  (realized : mcmc/nnrat-hastings-kernel-realization S target proposal kernel correction)
  (correction-symmetric : mcmc/nnrat-symmetric-flow S correction)
  → markov/nnrat-stationary S states kernel target

mcmc/nnrat-hastings-completed-kernel-detailed-balance.{u} :
  (S : Type u) (states : Finset S) (target : S → ℚ≥0) (proposal placement : S → S → ℚ≥0)
  (weighted-placement-symmetric : mcmc/nnrat-symmetric-flow S (correction))
  → markov/nnrat-detailed-balance S target (kernel)
  where correction := mcmc/nnrat-hastings-rejection-correction S target placement
  where kernel := mcmc/nnrat-hastings-completed-kernel S states target proposal placement

mcmc/nnrat-hastings-completed-kernel-stationary.{u} :
  (S : Type u) (states : Finset S) (target : S → ℚ≥0) (proposal placement : S → S → ℚ≥0)
  (target-normalized : probability/nnrat-total-mass S states target = 1)
  (proposal-normalized : markov/nnrat-kernel-rows-normalized S states proposal)
  (placement-has-rejection-mass : ∀ (left : S), probability/nnrat-total-mass S states (placement left) = mcmc/nnrat-hastings-rejection-mass S states target proposal left)
  (weighted-placement-symmetric : mcmc/nnrat-symmetric-flow S (correction))
  → markov/nnrat-stationary S states (kernel) target
  where correction := mcmc/nnrat-hastings-rejection-correction S target placement
  where kernel := mcmc/nnrat-hastings-completed-kernel S states target proposal placement

mcmc/nnrat-hastings-completed-kernel-stationary-of-off-diagonal-zero.{u} :
  (S : Type u) (states : Finset S) (target : S → ℚ≥0) (proposal placement : S → S → ℚ≥0)
  (equality-decidable : ∀ (left : S), ∀ (right : S), proposition/disjunction (left = right) (left = right → proposition/falsity))
  (off-diagonal : mcmc/nnrat-off-diagonal-zero S placement)
  (target-normalized : probability/nnrat-total-mass S states target = 1)
  (proposal-normalized : markov/nnrat-kernel-rows-normalized S states proposal)
  (placement-has-rejection-mass : ∀ (left : S), probability/nnrat-total-mass S states (placement left) = mcmc/nnrat-hastings-rejection-mass S states target proposal left)
  → markov/nnrat-stationary S states (kernel) target
  where kernel := mcmc/nnrat-hastings-completed-kernel S states target proposal placement

mcmc/nnrat-hastings-diagonal-rejection-placement-off-diagonal-zero.{u} :
  (S : Type u) (states : Finset S) (target : S → ℚ≥0) (proposal : S → S → ℚ≥0)
  (decision : S → S → data/Bool)
  (certified : finite/certified-equality-decision S decision)
  → mcmc/nnrat-off-diagonal-zero S (placement)
  where placement := mcmc/nnrat-hastings-diagonal-rejection-placement S states target proposal decision

mcmc/nnrat-hastings-diagonal-rejection-placement-has-rejection-mass.{u} :
  (S : Type u) (states : Finset S) (target : S → ℚ≥0) (proposal : S → S → ℚ≥0)
  (decision : S → S → data/Bool)
  (certified : finite/certified-equality-decision S decision)
  (carrier-covered : ∀ (state : S), list/membership S (finset-data/enumeration S states) state)
  (left : S)
  → probability/nnrat-total-mass S states (placement) = mcmc/nnrat-hastings-rejection-mass S states target proposal left
  where placement := mcmc/nnrat-hastings-diagonal-rejection-placement S states target proposal decision left

mcmc/nnrat-hastings-canonical-kernel-stationary.{u} :
  (S : Type u) (states : Finset S) (target : S → ℚ≥0) (proposal : S → S → ℚ≥0)
  (decision : S → S → data/Bool)
  (certified : finite/certified-equality-decision S decision)
  (carrier-covered : ∀ (state : S), list/membership S (finset-data/enumeration S states) state)
  (target-normalized : probability/nnrat-total-mass S states target = 1)
  (proposal-normalized : markov/nnrat-kernel-rows-normalized S states proposal)
  → markov/nnrat-stationary S states (kernel) target
  where kernel := mcmc/nnrat-hastings-canonical-kernel S states target proposal decision

mcmc/nnrat-hastings-canonical-kernel-stationary-of-exhaustive-carrier.{u} :
  (S : Type u) (states : Finset S) (target : S → ℚ≥0) (proposal : S → S → ℚ≥0)
  (decision : S → S → data/Bool)
  (exhaustive : finite/certified-exhaustive-carrier S states decision)
  (target-normalized : probability/nnrat-total-mass S states target = 1)
  (proposal-normalized : markov/nnrat-kernel-rows-normalized S states proposal)
  → markov/nnrat-stationary S states (kernel) target
  where kernel := mcmc/nnrat-hastings-canonical-kernel S states target proposal decision