OAI/Combinatorics/ContingencyTables/Sampling/ProfileBoxIndex.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

A computed finite-box index for the two small-profile views

  1. def OAI.ContingencyTables.ProfilePrograms.profileBoxIndex line 12
  2. def OAI.ContingencyTables.ProfilePrograms.profileBoxIndexRealizer line 15
  3. lemma OAI.ContingencyTables.ProfilePrograms.polynomial_profileBoxIndex line 19
  4. abbrev OAI.ContingencyTables.SmallGraphProfiles.ProfileBox line 37
  5. abbrev OAI.ContingencyTables.SmallGraphProfiles.ProfileIndex line 38
  6. def OAI.ContingencyTables.SmallGraphProfiles.profileBoxCoordinates line 40
  7. def OAI.ContingencyTables.SmallGraphProfiles.profileIndex line 45
  8. lemma OAI.ContingencyTables.SmallGraphProfiles.profileBoxCoordinates_code line 50
  9. lemma OAI.ContingencyTables.SmallGraphProfiles.profileBoxIndex_actual line 59
  10. def OAI.ContingencyTables.SmallGraphProfiles.profileAt line 66
  11. lemma OAI.ContingencyTables.SmallGraphProfiles.profileAt_index line 70
  12. lemma OAI.ContingencyTables.SmallGraphProfiles.profileIndex_injective line 84
  13. lemma OAI.ContingencyTables.SmallGraphProfiles.profileAt_eq_some line 89
  14. lemma OAI.ContingencyTables.SmallGraphProfiles.sum_profileAt line 110

    Source documentation

    The finite box includes every positive profile exactly once; all other vectors contribute zero to a decoded weighted sum.

    lemma sum_profileAt (w : PaperStates r c → ℕ) :
    (∑ k : ProfileIndex (m := m) (n := n) (q := q),(profileAt r c e k).elim 0 w)=
…

    Mentions: OAI.ContingencyTables.SmallGraphProfiles.PaperStates, OAI.ContingencyTables.SmallGraphProfiles.ProfileIndex, OAI.ContingencyTables.SmallGraphProfiles.profileAt