OAI/Combinatorics/ContingencyTables/Sampling/ExactIntegerProgram.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Binary execution of an exact integer-weighted rejection trial

  1. def OAI.ContingencyTables.ExactIntegerPrograms.weightsCode line 13

    Source documentation

    Fractions share the total integer weight before canonical reduction.

    def weightsCode (xs : List ℕ) : List TreeFraction.Fraction :=
…
  2. def OAI.ContingencyTables.ExactIntegerPrograms.weightsCodeRealizer line 15
  3. lemma OAI.ContingencyTables.ExactIntegerPrograms.polynomial_weightsCode line 21
  4. abbrev OAI.ContingencyTables.ExactIntegerPrograms.Input line 26
  5. def OAI.ContingencyTables.ExactIntegerPrograms.choiceInput line 28
  6. def OAI.ContingencyTables.ExactIntegerPrograms.choiceInputRealizer line 30
  7. lemma OAI.ContingencyTables.ExactIntegerPrograms.polynomial_choiceInput line 34
  8. def OAI.ContingencyTables.ExactIntegerPrograms.weightedIndex line 41

    Source documentation

    One trial returns an index or requests another independent word. All integers are processed in binary; no weight is expanded into copies.

    def weightedIndex (z : Input) : Option ℕ :=
…

    Mentions: OAI.ContingencyTables.ExactIntegerPrograms.Input

  9. def OAI.ContingencyTables.ExactIntegerPrograms.weightedIndexRealizer line 44
  10. lemma OAI.ContingencyTables.ExactIntegerPrograms.polynomial_weightedIndex line 51
  11. lemma OAI.ContingencyTables.ExactIntegerPrograms.weightsCode_ofFn line 66
  12. lemma OAI.ContingencyTables.ExactIntegerPrograms.weightedIndex_ofFn line 72

    Source documentation

    The compiled binary trial is exactly the integer-grid experiment.

    lemma weightedIndex_ofFn {r k : ℕ} (w : Fin r → ℕ) (h : 0<totalWeight w)
    (hQ : totalWeight w≤2^k) (bits : Fin k → Bool) :
    weightedIndex (List.ofFn w,List.ofFn bits)=
      (weightedTrial w h hQ (FairBits.binaryWordEquiv k bits)).map Fin.val := by
…

    Mentions: OAI.ContingencyTables.ExactIntegerPrograms.weightedIndex, OAI.ContingencyTables.FairBits.binaryWordEquiv