FirstPaperFiniteSampler.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

abbrev OAI.ContingencyTables.SmallGraphProfiles.finiteSamplerBits line 30
Source documentation
The exact number of independent input bits used by the initialized finite experiment. The physical simulation has additional operation cost.
```
abbrev finiteSamplerBits (k : ℕ) : ℕ :=
…
```
def OAI.ContingencyTables.SmallGraphProfiles.initializedFiniteDraw line 38
Source documentation
Greedy arithmetic supplies all feasible fallbacks and the starting state. Each word returns a member of the original margin fibre.
```
def initializedFiniteDraw (k : ℕ) (htotal : (∑ i,r i)=∑ j,c j)
    (a : GridBoundary.Grid (I := Fin q) (4*d^8))
…
```
Mentions: OAI.ContingencyTables.GridBoundary.Grid
theorem OAI.ContingencyTables.SmallGraphProfiles.initializedFiniteDraw_variation line 47
Source documentation
Conditional accuracy of the entire actual finite-word experiment, with no assumed sampler, starting state, or completion fallback.
```
theorem initializedFiniteDraw_variation (k : ℕ) (hk : 1 ≤ k)
    (htotal : (∑ i,r i)=∑ j,c j)
    (a : GridBoundary.Grid (I := Fin q) (4*d^8))
…
```
Mentions: OAI.ContingencyTables.GridBoundary.Grid