OAI/Combinatorics/ContingencyTables/Transport/RejectionLaw.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.ContingencyTables.FirstSuccess.variation_self line 16
2. theorem OAI.ContingencyTables.FirstSuccess.variation_triangle line 19
3. def OAI.ContingencyTables.FirstSuccess.pointLaw line 28
4. def OAI.ContingencyTables.FirstSuccess.retryStep line 33
5. def OAI.ContingencyTables.FirstSuccess.retryLaw line 36
6. def OAI.ContingencyTables.FirstSuccess.successMass line 40
7. def OAI.ContingencyTables.FirstSuccess.failureMass line 43
8. theorem OAI.ContingencyTables.FirstSuccess.success_failure_total line 46
9. theorem OAI.ContingencyTables.FirstSuccess.retryStep_mass line 57
10. theorem OAI.ContingencyTables.FirstSuccess.outputMass_succ line 77
11. theorem OAI.ContingencyTables.FirstSuccess.retryLaw_mass line 87

    Source documentation

    The law of finitely many independent trials, each of which can either return a value or fail, is the geometric first-success law.

    theorem retryLaw_mass (p : RationalLaw α) (f : α → Option β)
        (fallback z : β) (n : ℕ) :
        (retryLaw p f fallback n).mass z =
          outputMass (successMass p f) (failureMass p f) n fallback z := by
    …

    Mentions: OAI.ContingencyTables.FirstSuccess.retryLaw, OAI.ContingencyTables.FirstSuccess.outputMass, OAI.ContingencyTables.FirstSuccess.successMass, OAI.ContingencyTables.FirstSuccess.failureMass

12. theorem OAI.ContingencyTables.FirstSuccess.retryLaw_variation line 98

    Source documentation

    Approximate independent trials incur their error before the success test. Rejection never divides that error by a success probability.

    theorem retryLaw_variation (p q : RationalLaw α) (f : α → Option β)
        (fallback : β) (n : ℕ) :
        variation (retryLaw p f fallback n) (retryLaw q f fallback n) ≤
          (n : ℚ) * variation p q := by
    …

    Mentions: OAI.ContingencyTables.FirstSuccess.variation, OAI.ContingencyTables.FirstSuccess.retryLaw