OAI/Combinatorics/ContingencyTables/Sampling/SmallComplementProgram.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Binary execution of the complemented small column view

  1. def OAI.ContingencyTables.ProfilePrograms.complementValues line 11
  2. def OAI.ContingencyTables.ProfilePrograms.complementValuesRealizer line 13
  3. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_complementValues line 15
  4. lemma OAI.ContingencyTables.ProfilePrograms.complementValues_ofFn line 18
  5. theorem OAI.ContingencyTables.SmallGraphProfiles.lookupComplement_eq line 34

    Source documentation

    The arithmetic complement needs no underflow assumption: it agrees with the natural subtraction already present in the physical view.

    theorem lookupComplement_eq (B : Fin m → Fin n → ℕ) (z : SmallProfile small) (U : ℕ)
    (hU : ∀ a : Cells small,B a.val.1 a.val.2=U) (i : Fin m) (j : Fin n) :
    lookupView ((cellCatalog small e,complementValues (U,viewList small e z true)),(i.val,j.val))=
      smallQ small B z i j := by
…

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

  6. theorem OAI.ContingencyTables.SmallGraphProfiles.complementedColumnSum_eq line 47
  7. theorem OAI.ContingencyTables.SmallGraphProfiles.storedRowSum_eq line 65