OAI/Combinatorics/ContingencyTables/Dense/DenseBoundedTrial.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ContingencyTables.GridBoundary.offsetCoordinateEquiv line 19
2. def OAI.ContingencyTables.GridBoundary.boundedOffsetLaw line 23
3. def OAI.ContingencyTables.GridBoundary.uniformOffsetLaw line 28
4. theorem OAI.ContingencyTables.GridBoundary.uniformOffsetLaw_mass line 32
5. theorem OAI.ContingencyTables.GridBoundary.boundedOffsetLaw_variation line 41
6. def OAI.ContingencyTables.GridBoundary.boundedTrialLaw line 48
7. theorem OAI.ContingencyTables.GridBoundary.stationaryTrialLaw_eq line 55
8. theorem OAI.ContingencyTables.GridBoundary.inverse_two_pow_cast line 71
9. theorem OAI.ContingencyTables.GridBoundary.boundedTrialLaw_variation line 79

   Source documentation

   A complete finite dense trial has bin-mixing error plus the bounded offset error, with the manuscript's actual walk and offset schedules.

   theorem boundedTrialLaw_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