OAI/Combinatorics/ContingencyTables/Sampling/InverseSmallRepair.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Explicit arithmetic inverse of each labelled repair

  1. def OAI.ContingencyTables.SmallGraphProfiles.inverseRepairRow line 18

    Source documentation

    Undo the row transfer, using only additions, subtractions and tests against the two specified cells.

    def inverseRepairRow (small : I → J → Bool) (v : SmallProfile small) (s t : I×J)
    (i : I) (j : J) : ℕ :=
…
  2. def OAI.ContingencyTables.SmallGraphProfiles.inverseRepairProfile line 22
  3. lemma OAI.ContingencyTables.SmallGraphProfiles.inverseRepairRow_repaired line 28
  4. theorem OAI.ContingencyTables.SmallGraphProfiles.inverseRepairProfile_repaired line 43

    Source documentation

    The inverse is evaluated once per ordered defect label; no search through bounded profiles is needed to recover a predecessor.

    theorem inverseRepairProfile_repaired (small : I → J → Bool) (B : I → J → ℕ)
    (z : SmallProfile small) (s t : I×J)
    (hz : ∀ a,z a ≤ B a.1.val.1 a.1.val.2)
    (hd : IsDefect (smallView small z false) (smallQ small B z) s t) :
    inverseRepairProfile small B (repairedProfile small B z s t) s t=z := by
…

    Mentions: OAI.ContingencyTables.IsDefect, OAI.ContingencyTables.SmallGraphProfiles.inverseRepairProfile, OAI.ContingencyTables.SmallGraphProfiles.repairedProfile