OAI/Combinatorics/ContingencyTables/Sampling/ExactIntegerRetry.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.ContingencyTables.ExactIntegerChoice.trialLaw line 17
2. def OAI.ContingencyTables.ExactIntegerChoice.failure line 20
3. lemma OAI.ContingencyTables.ExactIntegerChoice.trialLaw_none line 22
4. lemma OAI.ContingencyTables.ExactIntegerChoice.lifted_success line 31
5. lemma OAI.ContingencyTables.ExactIntegerChoice.lifted_no_success line 35
6. lemma OAI.ContingencyTables.ExactIntegerChoice.lifted_failure line 39
7. def OAI.ContingencyTables.ExactIntegerChoice.retryIntegerLaw line 45

   Source documentation

   none records that all supplied independent trials rejected; it is not a fallback table. This is the finite prefix law of exact rejection.

   def retryIntegerLaw (N : ℕ) : RationalLaw (Option (Fin r)) :=
   …

8. lemma OAI.ContingencyTables.ExactIntegerChoice.retryIntegerLaw_none line 48
9. lemma OAI.ContingencyTables.ExactIntegerChoice.retryIntegerLaw_some line 53
10. lemma OAI.ContingencyTables.ExactIntegerChoice.failure_nonnegative line 71
11. lemma OAI.ContingencyTables.ExactIntegerChoice.failure_lt_half line 76
12. lemma OAI.ContingencyTables.ExactIntegerChoice.retryIntegerLaw_failure_bound line 85
13. lemma OAI.ContingencyTables.ExactIntegerChoice.retryIntegerLaw_limit line 90
14. lemma OAI.ContingencyTables.ExactIntegerChoice.retryIntegerLaw_expected_attempts line 109

    Source documentation

    The expected number of independent integer proposals is less than two.

    lemma retryIntegerLaw_expected_attempts (hshort : Q<2*totalWeight w) :
        Summable (fun N => ((retryIntegerLaw w h hQ N).mass none:ℝ)) ∧
          (∑' N,((retryIntegerLaw w h hQ N).mass none:ℝ))<2 := by
    …

    Mentions: OAI.ContingencyTables.ExactIntegerChoice.totalWeight, OAI.ContingencyTables.ExactIntegerChoice.retryIntegerLaw

15. lemma OAI.ContingencyTables.ExactIntegerChoice.clog_power_lt_twice line 124