OAI/Combinatorics/ContingencyTables/Transport/CacheBoxBounds.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ContingencyTables.DensePrograms.completionBoxMeasure line 11
2. theorem OAI.ContingencyTables.DensePrograms.completionWeightMeasure_polynomial line 15
3. def OAI.ContingencyTables.ProfilePrograms.matrixEntryBox line 44
4. def OAI.ContingencyTables.ProfilePrograms.entryResidualParameters line 48
5. def OAI.ContingencyTables.ProfilePrograms.entryResidualRealizer line 51
6. lemma OAI.ContingencyTables.ProfilePrograms.polynomial_entryResidual line 57
7. theorem OAI.ContingencyTables.ProfilePrograms.matrixEntryBox_bound line 62

   Source documentation

   Separating binary preparation size from the four enumerated boxes.

   theorem matrixEntryBox_bound : ∃ p : Polynomial ℕ,∀ z,
       let r := entryResidualParameters z
   …

   Mentions: OAI.ContingencyTables.ProfilePrograms.entryResidualParameters

8. theorem OAI.ContingencyTables.ProfilePrograms.matrixEntryMeasure_polynomial line 93