OAI/Combinatorics/ContingencyTables/Dense/DenseMatrixWalk.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Binary matrix propagation of the implemented dense walk

  1. abbrev OAI.ContingencyTables.DensePrograms.MatrixWalkData line 11
  2. def OAI.ContingencyTables.DensePrograms.initialEntry line 13
  3. def OAI.ContingencyTables.DensePrograms.initialEntryRealizer line 16
  4. lemma OAI.ContingencyTables.DensePrograms.polynomial_initialEntry line 19
  5. def OAI.ContingencyTables.DensePrograms.initialVector line 23
  6. def OAI.ContingencyTables.DensePrograms.initialVectorRealizer line 26
  7. lemma OAI.ContingencyTables.DensePrograms.polynomial_initialVector line 29
  8. def OAI.ContingencyTables.DensePrograms.matrixWalkInput line 33
  9. def OAI.ContingencyTables.DensePrograms.matrixWalkInputRealizer line 36
  10. lemma OAI.ContingencyTables.DensePrograms.polynomial_matrixWalkInput line 42
  11. def OAI.ContingencyTables.DensePrograms.matrixWalk line 51
  12. def OAI.ContingencyTables.DensePrograms.matrixWalkRealizer line 54
  13. theorem OAI.ContingencyTables.DensePrograms.polynomial_matrixWalk line 59

    Source documentation

    The number of matrix steps is supplied by a unary list. All entries and the propagated vector use binary integers.

    theorem polynomial_matrixWalk : PolynomialTime matrixWalkRealizer := by
…

    Mentions: OAI.ContingencyTables.DensePrograms.matrixWalkRealizer

  14. lemma OAI.ContingencyTables.DensePrograms.initialVector_actual line 70
  15. lemma OAI.ContingencyTables.DensePrograms.numerators_reindex line 93
  16. theorem OAI.ContingencyTables.DensePrograms.matrixWalk_actual line 106

    Source documentation

    The matrix is the count matrix of the actual Boolean walk, including all rejected proposals and unused proposal codes.

    theorem matrixWalk_actual {m n d N : ℕ} (R : Option (Fin m) → ℕ)
    (P : Option (Fin n) → ℕ) (hq : m*n≤d)
    (e : Fin N ≃ Grid (I := Fin (m*n)) (4*d^8))
…
  17. theorem OAI.ContingencyTables.DensePrograms.matrixWalk_mass line 123

    Source documentation

    A matrix-vector entry, normalized by its known dyadic denominator, is the mass of the implemented finite-bit walk.

    theorem matrixWalk_mass {m n d N : ℕ} (R : Option (Fin m) → ℕ)
    (P : Option (Fin n) → ℕ) (hq : m*n≤d)
    (e : Fin N ≃ Grid (I := Fin (m*n)) (4*d^8))
…