OAI/Combinatorics/ContingencyTables/Sampling/ExactMatrixLookup.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Feasibility of every decoded candidate in the exact branch

  1. lemma OAI.ContingencyTables.ExactMatrixTrial.lookup_index line 15
  2. lemma OAI.ContingencyTables.ExactMatrixTrial.lookup_feasible line 24

    Source documentation

    Even a malformed index returns the fixed feasible fallback.

    lemma lookup_feasible (fallback : Table r c) (i : ℕ) :
    ∃ X : Table r c,
      lookup ((originalCandidates (List.ofFn r,List.ofFn c),matrixCode fallback.val),i)=
        matrixCode X.val := by
…

    Mentions: OAI.ContingencyTables.Table, OAI.ContingencyTables.ExactMatrixTrial.lookup