Reference · Finite types, distributions and Markov chains

rainbow.math.finite.markov-hastings-positive

Finite types, distributions and Markov chainssrc/rainbow/math/finite/markov_hastings_positive.clj0 definitions, 5 theorems

Strict-positivity certificates for division-free Hastings transitions. If both directed target-proposal products are positive, then their minimum (the accepted flow) is positive. The same hypotheses make the ratio acceptance positive; multiplying by the positive forward proposal therefore makes the accepted transition positive. These are the mathematical bridge from full-support target/proposal data to one-step reachability. Native, kernel-checked, and axiom-free on D63.

Depends onmath.finite.markov-hastings-flowmath.rational.nnrat.positive

mcmc/nnrat-hastings-ratio-acceptance-positive :
  (forward reverse : ℚ≥0) (forward-positive : nnrat/positive forward)
  (reverse-positive : nnrat/positive reverse)
  → nnrat/positive (mcmc/nnrat-hastings-ratio-acceptance forward reverse)

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

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

mcmc/nnrat-hastings-completed-kernel-positive.{u} :
  (S : Type u) (states : Finset S) (target : S → ℚ≥0) (proposal placement : S → S → ℚ≥0)
  (left right : S) (target-left-positive : nnrat/positive (target left))
  (proposal-forward-positive : nnrat/positive (proposal left right))
  (target-right-positive : nnrat/positive (target right))
  (proposal-reverse-positive : nnrat/positive (proposal right left))
  → nnrat/positive (mcmc/nnrat-hastings-completed-kernel S states target proposal placement left right)

mcmc/nnrat-hastings-canonical-kernel-positive.{u} :
  (S : Type u) (states : Finset S) (target : S → ℚ≥0) (proposal : S → S → ℚ≥0)
  (decision : S → S → data/Bool) (left right : S)
  (target-left-positive : nnrat/positive (target left))
  (proposal-forward-positive : nnrat/positive (proposal left right))
  (target-right-positive : nnrat/positive (target right))
  (proposal-reverse-positive : nnrat/positive (proposal right left))
  → nnrat/positive (mcmc/nnrat-hastings-canonical-kernel S states target proposal decision left right)