Reference · Finite types, distributions and Markov chains

rainbow.math.finite.markov-kernel-minimum

Finite types, distributions and Markov chainssrc/rainbow/math/finite/markov_kernel_minimum.clj3 definitions, 5 theorems

A certified global minimum entry of a finite exact-rational kernel. Nested finite argmins first select a minimum target in each source row, then select a source whose row minimum is globally smallest. Explicit anchor states make the construction total; when those anchors belong to the finite carrier, both selected indices belong as well. Subsequent theorems expose positivity and the global lower-bound property for Markov minorization. Native, kernel-checked, and axiom-free on D63.

Depends onmath.finite.rational-argminmath.rational.nnrat.positive

markov/nnrat-kernel-row-argmin.{u} :
  (S : Type u) (states : Finset S) (kernel : S → S → ℚ≥0) (initial-target x₁ : S)
  → S

markov/nnrat-kernel-argmin-source.{u} :
  (S : Type u) (states : Finset S) (kernel : S → S → ℚ≥0) (x₁ x₂ : S)
  → S

markov/nnrat-kernel-minimum.{u} :
  (S : Type u) (states : Finset S) (kernel : S → S → ℚ≥0) (x₁ x₂ : S)
  → ℚ≥0

markov/nnrat-kernel-row-argmin-member.{u} :
  (S : Type u) (states : Finset S) (kernel : S → S → ℚ≥0) (initial-target : S)
  (initial-target-member : membership initial-target) (source : S)
  → membership (argmin)
  where argmin := markov/nnrat-kernel-row-argmin S states kernel initial-target source
  where membership := list/membership S (finset-data/enumeration S states)

markov/nnrat-kernel-argmin-source-member.{u} :
  (S : Type u) (states : Finset S) (kernel : S → S → ℚ≥0)
  (initial-source initial-target : S)
  (initial-source-member : membership initial-source)
  → membership (source)
  where membership := list/membership S (finset-data/enumeration S states)
  where source := markov/nnrat-kernel-argmin-source S states kernel initial-source initial-target

markov/nnrat-kernel-minimum-positive.{u} :
  (S : Type u) (states : Finset S) (kernel : S → S → ℚ≥0)
  (initial-source initial-target : S)
  (initial-source-member : membership initial-source)
  (initial-target-member : membership initial-target)
  (listed-positive : ∀ (source : S), ∀ (target : S), ∀ (source-in-carrier : membership source), ∀ (target-in-carrier : membership target), nnrat/positive (kernel source target))
  → nnrat/positive (markov/nnrat-kernel-minimum S states kernel initial-source initial-target)
  where membership := list/membership S (finset-data/enumeration S states)

markov/nnrat-kernel-minimum-bounds-entry.{u} :
  (S : Type u) (states : Finset S) (kernel : S → S → ℚ≥0)
  (initial-source initial-target source target : S)
  (source-in-carrier : membership source) (target-in-carrier : membership target)
  → markov/nnrat-kernel-minimum S states kernel initial-source initial-target ≤ kernel source target
  where membership := list/membership S (finset-data/enumeration S states)

markov/nnrat-kernel-minimum-positive-lower-bound.{u} :
  (S : Type u) (states : Finset S) (kernel : S → S → ℚ≥0)
  (initial-source initial-target : S)
  (initial-source-member : membership initial-source)
  (initial-target-member : membership initial-target)
  (listed-positive : ∀ (source : S), ∀ (target : S), ∀ (source-in-carrier : membership source), ∀ (target-in-carrier : membership target), nnrat/positive (kernel source target))
  → proposition/conjunction (nnrat/positive (minimum)) (∀ (source : S), ∀ (target : S), ∀ (source-in-carrier : membership source), ∀ (target-in-carrier : membership target), minimum ≤ kernel source target)
  where membership := list/membership S (finset-data/enumeration S states)
  where minimum := markov/nnrat-kernel-minimum S states kernel initial-source initial-target