OAI/Combinatorics/ContingencyTables/Sampling/ExactIntegerChoice.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ContingencyTables.ExactIntegerChoice.totalWeight line 15
2. def OAI.ContingencyTables.ExactIntegerChoice.normalized line 17
3. def OAI.ContingencyTables.ExactIntegerChoice.prefixWeight line 19
4. lemma OAI.ContingencyTables.ExactIntegerChoice.normalized_nonnegative line 21
5. lemma OAI.ContingencyTables.ExactIntegerChoice.normalized_total line 25
6. lemma OAI.ContingencyTables.ExactIntegerChoice.cumulative_normalized line 29
7. lemma OAI.ContingencyTables.ExactIntegerChoice.grid_scaled_cumulative line 36
8. theorem OAI.ContingencyTables.ExactIntegerChoice.integer_choice_exact line 43

   Source documentation

   On the integer grid with size equal to the total weight, the cumulative selector has exactly the desired rational law, with no approximation.

   theorem integer_choice_exact (h : 0<totalWeight w) (i : Fin r) :
       outputLaw (normalized w) (normalized_total w h) h i=normalized w i := by
   …

   Mentions: OAI.ContingencyTables.ExactIntegerChoice.totalWeight, OAI.ContingencyTables.ExactIntegerChoice.normalized, OAI.ContingencyTables.ExactIntegerChoice.normalized_total

9. def OAI.ContingencyTables.ExactIntegerChoice.intervalTrial line 58

   Source documentation

   One bounded trial rejects only the unused terminal indices.

   def intervalTrial {V Q : ℕ} (_h : V≤Q) (j : Fin Q) : Option (Fin V) :=
   …

10. lemma OAI.ContingencyTables.ExactIntegerChoice.intervalTrial_eq_some line 61
11. lemma OAI.ContingencyTables.ExactIntegerChoice.intervalTrial_mass line 71
12. def OAI.ContingencyTables.ExactIntegerChoice.weightedTrial line 79

    Source documentation

    A rational choice with integer weights, after a single binary rejection trial. The sum of these masses is totalWeight / 2^k.

    def weightedTrial (h : 0<totalWeight w) {Q : ℕ} (hQ : totalWeight w≤Q)
        (j : Fin Q) : Option (Fin r) :=
    …

    Mentions: OAI.ContingencyTables.ExactIntegerChoice.totalWeight

13. lemma OAI.ContingencyTables.ExactIntegerChoice.weightedTrial_mass line 83