OAI/Combinatorics/ContingencyTables/Dense/DenseBooleanDraw.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ContingencyTables.GridBoundary.denseDrawBits line 20
2. def OAI.ContingencyTables.GridBoundary.denseBooleanDraw line 24
3. def OAI.ContingencyTables.GridBoundary.denseBooleanDrawLaw line 32
4. theorem OAI.ContingencyTables.GridBoundary.denseBooleanDrawLaw_eq line 39
5. theorem OAI.ContingencyTables.GridBoundary.denseBooleanDraw_variation line 62

   Source documentation

   The actual finite Boolean draw always has codomain the feasible tables and its law satisfies the desired dense approximation guarantee.

   theorem denseBooleanDraw_variation (R : Option I → ℕ) (P : Option J → ℕ)
       (d : ℕ) (hd : 14 ≤ d) (hR : ∀ i, d ^ 12 ≤ R i) (hP : ∀ j, d ^ 12 ≤ P j)
       (hRmax : ∀ i, R (some i) ≤ R none) (hPmax : ∀ j, P (some j) ≤ P none)
       (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

6. theorem OAI.ContingencyTables.GridBoundary.denseDrawBits_polynomial line 81

   Source documentation

   The full Boolean source has polynomial length in the declared dense parameters.

   theorem denseDrawBits_polynomial (R : Option I → ℕ) (P : Option J → ℕ)
       (d C b h : ℕ) (e : I × J ≃ Fin q) (hq : q ≤ d)
       (hwidth : ∀ p, integerWidth R P d p ≤ C) (hb : Nat.clog 2 (C + 2) ≤ b) :
       denseDrawBits R P d e h ≤ 25 * (d + b + h + 1) ^ 62 := by
   …

   Mentions: OAI.ContingencyTables.GridBoundary.integerWidth, OAI.ContingencyTables.GridBoundary.denseDrawBits