OAI/Combinatorics/ContingencyTables/Sampling/SmallViewLookupProgram.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Polynomial lookup of the sparse small-cell view

  1. abbrev OAI.ContingencyTables.ProfilePrograms.ViewLookupInput line 10
  2. def OAI.ContingencyTables.ProfilePrograms.lookupView line 12
  3. def OAI.ContingencyTables.ProfilePrograms.lookupViewRealizer line 15
  4. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_lookupView line 19
  5. theorem OAI.ContingencyTables.SmallGraphProfiles.lookupView_eq line 35

    Source documentation

    Missing large cells yield zero, exactly as required by smallView.

    theorem lookupView_eq (z : SmallProfile small) (b : Bool) (i : Fin m) (j : Fin n) :
    lookupView ((cellCatalog small e,viewList small e z b),(i.val,j.val))=
      smallView small z b i j := by
…

    Mentions: OAI.ContingencyTables.SmallGraphProfiles.cellCatalog, OAI.ContingencyTables.SmallGraphProfiles.viewList