OAI/Combinatorics/ContingencyTables/Sampling/OriginalResidualVector.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Explicit integer correction weights on the original-table box

  1. abbrev OAI.ContingencyTables.ProfilePrograms.ResidualVectorCache line 14

    Source documentation

    Candidate matrices, ordinary numerators, denominator/branch size, and table count.

    abbrev ResidualVectorCache := (List (Option MatrixCode)×List ℕ)×((ℕ×ℕ)×ℕ)
  2. def OAI.ContingencyTables.ProfilePrograms.residualVectorEntry line 16
  3. def OAI.ContingencyTables.ProfilePrograms.residualVectorEntryRealizer line 20
  4. lemma OAI.ContingencyTables.ProfilePrograms.polynomial_residualVectorEntry line 32
  5. def OAI.ContingencyTables.ProfilePrograms.residualVectorIndices line 47
  6. def OAI.ContingencyTables.ProfilePrograms.residualVectorIndicesRealizer line 49
  7. lemma OAI.ContingencyTables.ProfilePrograms.polynomial_residualVectorIndices line 52
  8. def OAI.ContingencyTables.ProfilePrograms.residualVector line 59
  9. def OAI.ContingencyTables.ProfilePrograms.residualVectorRealizer line 62
  10. lemma OAI.ContingencyTables.ProfilePrograms.polynomial_residualVector line 65
  11. lemma OAI.ContingencyTables.ProfilePrograms.residualVector_ofFn line 75
  12. lemma OAI.ContingencyTables.OriginalBoxLaw.index_injective line 98
  13. lemma OAI.ContingencyTables.OriginalBoxLaw.residualVector_actual line 104

    Source documentation

    Invalid candidates carry zero; every feasible candidate carries exactly its signed residual numerator after the proved nonnegative truncation.

    lemma residualVector_actual (p : IntegerLaw (Table r c) Q) (fallback : Table r c)
    (T : ℕ) (hT : 0<T) :
    let _ : Nonempty (Table r c) := ⟨fallback⟩
…

    Mentions: OAI.ContingencyTables.IntegerLaw, OAI.ContingencyTables.Table