OAI/Combinatorics/ContingencyTables/Dense/DenseMetropolisSemantics.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The binary dense program realizes the exact finite transition

  1. theorem OAI.ContingencyTables.DensePrograms.flatMetropolisStep_pair line 14
  2. lemma OAI.ContingencyTables.DensePrograms.ofFn_split_take line 38
  3. lemma OAI.ContingencyTables.DensePrograms.ofFn_split_drop line 46
  4. theorem OAI.ContingencyTables.DensePrograms.flatWordStep_code line 59

    Source documentation

    Exact pointwise agreement, hence every finite-word law and mixing bound for denseBitStep applies to the polynomial list implementation.

    theorem flatWordStep_code {m n d : ℕ}
    (R : Option (Fin m) → ℕ) (P : Option (Fin n) → ℕ)
    (a : Grid (I := Fin (m*n)) (4*d^8)) (bits : Fin (denseStepBits d) → Bool) :
…