OAI/Combinatorics/ContingencyTables/Transport/ResidualEnumerationBounds.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ContingencyTables.ProfilePrograms.completionEnumeration_count line 12
2. lemma OAI.ContingencyTables.ProfilePrograms.completionEnumeration_count_le line 18
3. lemma OAI.ContingencyTables.ProfilePrograms.swapZeroList_length line 27
4. lemma OAI.ContingencyTables.ProfilePrograms.swapZeroList_sum_le line 31
5. lemma OAI.ContingencyTables.ProfilePrograms.normalizedCompletion_count_le line 40
6. lemma OAI.ContingencyTables.ProfilePrograms.canonicalCompletion_count_le line 48
7. def OAI.ContingencyTables.ProfilePrograms.profilePaddingData line 53
8. lemma OAI.ContingencyTables.ProfilePrograms.profilePaddedMargins_length line 58
9. lemma OAI.ContingencyTables.ProfilePrograms.profilePaddedMargins_sum line 63
10. lemma OAI.ContingencyTables.ProfilePrograms.profilePaddedMargins_sum_ofFn line 70
11. lemma OAI.ContingencyTables.ProfilePrograms.profileCompletion_count line 79

    Source documentation

    This bound is independent of the values in the two proposed small views. In particular it applies before the validity test accepts them.

    lemma profileCompletion_count (z : ProfileCheckData×ℕ) :
        gridStateCount (completionEnumerationData
          (profilePaddedMargins true z,profilePaddedMargins false z)) ≤
          (z.1.1.2.1.length*(z.1.1.2.1.sum+z.1.1.2.2.length*z.2)+1)^
            (z.1.1.2.1.length*z.1.1.2.2.length) := by
    …

    Mentions: OAI.ContingencyTables.ProfilePrograms.ProfileCheckData, OAI.ContingencyTables.ProfilePrograms.profilePaddedMargins

12. lemma OAI.ContingencyTables.SmallGraphProfiles.padded_base_bound line 98
13. lemma OAI.ContingencyTables.SmallGraphProfiles.arbitrary_profile_margin_sum line 120

    Source documentation

    All profile proposals have a singly exponential completion box, including proposals rejected by the chain's validity test.

    lemma arbitrary_profile_margin_sum {m n : ℕ} (r : Fin m → ℕ) (c : Fin n → ℕ)
        (v : ProfileCheckData)
        (hr : v.1.2.1=List.ofFn r) (hc : v.1.2.2=List.ofFn c) :
        let dim := dimensionAllowance (I := Fin m) (J := Fin n)
    …

14. lemma OAI.ContingencyTables.SmallGraphProfiles.arbitrary_profile_completion_count line 143