OAI/Combinatorics/ContingencyTables/Sampling/FirstPaperBoundedLaw.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The bounded finite sampling law reaches the requested accuracy

  1. theorem OAI.ContingencyTables.SmallGraphProfiles.boundedOuterLaw_variation line 27

    Source documentation

    The concrete completion draw, literal small transition and repeated success test have the full error guarantee on nonempty large rectangles. The physical machine and empty-rectangle branch are separate constructions.

    theorem boundedOuterLaw_variation (b k : ℕ)
    (hb : Nat.clog 2 (stateBound r c+2) ≤ b) (hdb : d ≤ b) (hk : 1 ≤ k)
    (hC : stateBound r c+1 ≤ 2^b)
    (a : GridBoundary.Grid (I := Fin q) (4*d^8))
…

    Mentions: OAI.ContingencyTables.SmallGraphProfiles.stateBound, OAI.ContingencyTables.GridBoundary.Grid