OAI/Combinatorics/ContingencyTables/Transport/TabulationMeasureBounds.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ContingencyTables.MeasuredMap.listMeasure_le line 13
2. lemma OAI.ContingencyTables.MeasuredMap.listMeasure_mono line 23
3. lemma OAI.ContingencyTables.ProfilePrograms.list_weight_bound line 40
4. lemma OAI.ContingencyTables.ProfilePrograms.profileMatrixMeasure_le line 46

   Source documentation

   The two loops over the profile box cost a polynomial in its cardinality and the uniform measure of a single transition entry.

   lemma profileMatrixMeasure_le (z : MatrixParameters) (W M : ℕ)
       (hz : weight z ≤ W)
       (hv : ∀ v∈profileBoxViews (matrixData z),weight v ≤ W)
       (he : ∀ u∈profileBoxViews (matrixData z),∀ v∈profileBoxViews (matrixData z),
         matrixEntryMeasure (z,(u,v)) ≤ M) :
       let N := gridStateCount (profileEnumerationData (matrixData z))
   …

   Mentions: OAI.ContingencyTables.ProfilePrograms.MatrixParameters, OAI.ContingencyTables.ProfilePrograms.profileBoxViews, OAI.ContingencyTables.ProfilePrograms.matrixData, OAI.ContingencyTables.ProfilePrograms.matrixEntryMeasure, OAI.ContingencyTables.ProfilePrograms.profileEnumerationData

5. lemma OAI.ContingencyTables.ProfilePrograms.unitMatrixMeasure_le line 94