ReferenceFiniteDraw.lean`

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

A finite Boolean draw of the actual state-dependent completion fibre

abbrev OAI.ContingencyTables.SmallGraphProfiles.paperReferenceEquiv line 30
abbrev OAI.ContingencyTables.SmallGraphProfiles.completionDrawBits line 34
def OAI.ContingencyTables.SmallGraphProfiles.completionBooleanDraw line 37
theorem OAI.ContingencyTables.SmallGraphProfiles.completionBooleanDraw_variation line 50
Source documentation
The output is a genuine completion of the current retained profile on every bit word; the distance bound is uniform in that state.
```
theorem completionBooleanDraw_variation
    (hPL : PublishedInputs.FiniteBoxPrekopaLeindler q)
    (hCheeger : PublishedInputs.FiniteCheeger (Grid (I := Fin q) (4*d^8)))
…
```
Mentions: OAI.ContingencyTables.PublishedInputs.FiniteBoxPrekopaLeindler, OAI.ContingencyTables.PublishedInputs.FiniteCheeger
lemma OAI.ContingencyTables.SmallGraphProfiles.completionDrawBits_le line 76
def OAI.ContingencyTables.SmallGraphProfiles.completionPaddedDraw line 89
Source documentation
One common reserved word works at every state, despite the different residual margins and quotient lengths.
```
def completionPaddedDraw (b h : ℕ) (hb : Nat.clog 2 (stateBound r c+2) ≤ b)
    (a : Grid (I := Fin q) (4*d^8)) (z : PaperStates r c) (fallback : PaperFibre r c z)
…
```
Mentions: OAI.ContingencyTables.SmallGraphProfiles.stateBound, OAI.ContingencyTables.SmallGraphProfiles.PaperStates, OAI.ContingencyTables.SmallGraphProfiles.PaperFibre
theorem OAI.ContingencyTables.SmallGraphProfiles.completionPaddedDraw_law line 95