OAI/Combinatorics/ContingencyTables/Dense/DenseDrawSemantics.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The bounded binary draw is exactly the analyzed Boolean sampler

  1. lemma OAI.ContingencyTables.DensePrograms.trialWidth_code line 15
  2. lemma OAI.ContingencyTables.DensePrograms.denseTrialBits_pos line 23
  3. def OAI.ContingencyTables.DensePrograms.drawInput line 31
  4. theorem OAI.ContingencyTables.DensePrograms.denseDrawCode_eq line 38

    Source documentation

    This identifies every output, including the all-rejections fallback, with the actual finite Boolean sampler whose total-variation bound is proved.

    theorem denseDrawCode_eq {m n d : ℕ}
    (R : Option (Fin m) → ℕ) (P : Option (Fin n) → ℕ)
    (hd : 14 ≤ d) (hR : ∀ i,d^12 ≤ R i) (hP : ∀ j,d^12 ≤ P j)
    (htotal : ∑ i,R i=∑ j,P j) (h : ℕ)
    (a : Grid (I := Fin (m*n)) (4*d^8)) (fallback : Table R P)
…

    Mentions: OAI.ContingencyTables.Table