OAI/Combinatorics/ContingencyTables/Transport/FinitePartialDraw.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

One Boolean word per listed proposal, with unused words giving a hold

  1. def OAI.ContingencyTables.FairBits.injectionDraw line 20

    Source documentation

    A code with no preimage is an explicit hold.

    def injectionDraw {k : ℕ} (e : X ↪ Fin (2^k)) (b : Fin (2^k)) : Option X :=
…
  2. lemma OAI.ContingencyTables.FairBits.injectionDraw_eq_some line 23
  3. theorem OAI.ContingencyTables.FairBits.injectionDraw_mass line 40

    Source documentation

    Every listed proposal gets exactly one equally likely bit string.

    theorem injectionDraw_mass {k : ℕ} (e : X ↪ Fin (2^k)) (x : X) :
    (mapLaw (uniformLaw (α := Fin (2^k))) (injectionDraw e)).mass (some x)=1/(2:ℚ)^k := by
…

    Mentions: OAI.ContingencyTables.FairBits.injectionDraw

  4. def OAI.ContingencyTables.FairBits.proposalEmbedding line 45
  5. def OAI.ContingencyTables.FairBits.partialBitDraw line 48
  6. theorem OAI.ContingencyTables.FairBits.partialBitDraw_mass line 51
  7. lemma OAI.ContingencyTables.FairBits.optionMap_mass_injective line 59
  8. lemma OAI.ContingencyTables.FairBits.optionMap_mass_outside line 66
  9. def OAI.ContingencyTables.FairBits.subsetBitDraw line 71
  10. theorem OAI.ContingencyTables.FairBits.subsetBitDraw_mass line 76

    Source documentation

    Distinct listed outcomes each have the advertised dyadic mass.

    theorem subsetBitDraw_mass (p : X → Prop) (k : ℕ)
    (h : Fintype.card {x // p x} ≤ 2^k) (x : X) :
    (mapLaw (uniformLaw (α := Fin k → Bool)) (subsetBitDraw p k h)).mass (some x)=
…

    Mentions: OAI.ContingencyTables.FairBits.subsetBitDraw