DenseMaximalReindex.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Dense draws with arbitrary choices of the reference row and column

lemma OAI.ContingencyTables.GridBoundary.maximal_index_exists line 19
def OAI.ContingencyTables.GridBoundary.maximalIndex line 23
def OAI.ContingencyTables.GridBoundary.maximalReindex line 25
abbrev OAI.ContingencyTables.GridBoundary.maximalMargin line 28
lemma OAI.ContingencyTables.GridBoundary.maximalMargin_max line 30
lemma OAI.ContingencyTables.GridBoundary.maximalMargin_lower line 36
lemma OAI.ContingencyTables.GridBoundary.maximalMargin_total line 39
abbrev OAI.ContingencyTables.GridBoundary.reindexedDrawBits line 44
def OAI.ContingencyTables.GridBoundary.reindexedBooleanDraw line 50
Source documentation
Move a largest row and column to the distinguished indices inside the sampler, then transport the output back to the fixed original indices.
```
def reindexedBooleanDraw (R : Option I → ℕ) (P : Option J → ℕ) (d : ℕ)
    (hd : 14 ≤ d) (hR : ∀ i,d^12 ≤ R i) (hP : ∀ j,d^12 ≤ P j)
    (e : I×J ≃ Fin q) (htotal : ∑ i,R i=∑ j,P j) (h : ℕ)
    (a : Grid (I := Fin q) (4*d^8)) (fallback : Table R P)
…
```
Mentions: OAI.ContingencyTables.GridBoundary.Grid, OAI.ContingencyTables.Table
def OAI.ContingencyTables.GridBoundary.reindexedBooleanDrawLaw line 61

theorem OAI.ContingencyTables.GridBoundary.reindexedBooleanDraw_variation line 70

Source documentation

The fixed reference used by the outer chain need not maximize either residual margin. The actual Boolean draw retains the same TV guarantee.

theorem reindexedBooleanDraw_variation (R : Option I → ℕ) (P : Option J → ℕ)
    (d : ℕ) (hd : 14 ≤ d) (hR : ∀ i,d^12 ≤ R i) (hP : ∀ j,d^12 ≤ P j)
    (hdimR : Fintype.card (Option I) ≤ d) (hdimP : Fintype.card (Option J) ≤ d)
    (hfree : Fintype.card (I×J) ≤ d) (htotal : ∑ i,R i=∑ j,P j)
    (e : I×J ≃ Fin q) (hPL : PublishedInputs.FiniteBoxPrekopaLeindler q)
    (hCheeger : PublishedInputs.FiniteCheeger (Grid (I := Fin q) (4*d^8)))
…

Mentions: OAI.ContingencyTables.PublishedInputs.FiniteBoxPrekopaLeindler, OAI.ContingencyTables.PublishedInputs.FiniteCheeger, OAI.ContingencyTables.GridBoundary.Grid

theorem OAI.ContingencyTables.GridBoundary.reindexedDrawBits_polynomial line 101
Source documentation
Relabeling preserves the polynomial Boolean-source bound. A bound on row margins already bounds every integer quotient width.
```
theorem reindexedDrawBits_polynomial (R : Option I → ℕ) (P : Option J → ℕ)
    (d C b h : ℕ) (e : I×J ≃ Fin q) (hq : q ≤ d)
    (hR : ∀ i,R i ≤ C) (hb : Nat.clog 2 (C+2) ≤ b) :
    reindexedDrawBits R P d e h ≤ 25*(d+b+h+1)^62 := by
…
```
Mentions: OAI.ContingencyTables.GridBoundary.reindexedDrawBits