OAI/Combinatorics/ContingencyTables/Transport/UniformPartialRejection.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Rejecting a uniform finite object through an explicit successful bijection

  1. def OAI.ContingencyTables.FirstSuccess.partialEquivDraw line 18
  2. lemma OAI.ContingencyTables.FirstSuccess.partialEquivDraw_eq_some line 22
  3. lemma OAI.ContingencyTables.FirstSuccess.partialEquiv_success_mass line 35
  4. lemma OAI.ContingencyTables.FirstSuccess.partialEquiv_failure_mass line 42
  5. theorem OAI.ContingencyTables.FirstSuccess.uniform_partial_retry_variation line 53

    Source documentation

    The bound applies before any approximate law is introduced, so later TV errors can be accumulated without conditioning on success.

    theorem uniform_partial_retry_variation (fallback : A) (n : ℕ) :
    variation (retryLaw (uniformLaw (α := S)) (partialEquivDraw p e) fallback n)
…

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

  6. theorem OAI.ContingencyTables.FirstSuccess.uniform_partial_retry_exp line 76

    Source documentation

    A lower success bound gives the usual exponential failure tail.

    theorem uniform_partial_retry_exp (fallback : A) (n : ℕ) (K : ℝ)
    (hs : 1/K ≤ (Fintype.card A:ℝ)/(Fintype.card S:ℝ)) :
    (variation (retryLaw (uniformLaw (α := S)) (partialEquivDraw p e) fallback n)
…

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