OAI/Combinatorics/ContingencyTables/Rooted/LargeMarginSemantics.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Exact indexing of the computed large residual margins

  1. lemma OAI.ContingencyTables.SmallGraphProfiles.largeIndices_ofFn_mem line 17
  2. def OAI.ContingencyTables.SmallGraphProfiles.largeMemberEquiv line 23
  3. def OAI.ContingencyTables.SmallGraphProfiles.largeIndexEquiv line 35

    Source documentation

    Increasing list order gives a fixed, computed indexing of every large row. The same construction is used for columns.

    def largeIndexEquiv (r : Fin m → ℕ) (U : ℕ) :
    Fin (largeIndices (U,List.ofFn r)).length ≃ LargeRows r U :=
…

    Mentions: OAI.ContingencyTables.SmallGraphProfiles.LargeRows

  4. lemma OAI.ContingencyTables.SmallGraphProfiles.largeIndexEquiv_val line 39
  5. lemma OAI.ContingencyTables.SmallGraphProfiles.largePaddedMargins_ofFn line 43
  6. theorem OAI.ContingencyTables.SmallGraphProfiles.largePaddedRows_code line 50
  7. theorem OAI.ContingencyTables.SmallGraphProfiles.largePaddedColumns_code line 66