OAI/Combinatorics/ContingencyTables/Sampling/FirstPaperInitialization.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Concrete initial state and completion fallbacks

  1. def OAI.ContingencyTables.GreedyFeasibleTable.reindexed line 14

    Source documentation

    Reindex the row/column recursion without changing its arithmetic.

    noncomputable def reindexed {I J : Type*} [Fintype I] [Fintype J]
    (r : I → ℕ) (c : J → ℕ) (h : (∑ i,r i)=∑ j,c j) : Table r c :=
…

    Mentions: OAI.ContingencyTables.Table

  2. def OAI.ContingencyTables.SmallGraphProfiles.initialJoint line 36

    Source documentation

    The image of a greedily filled original table is an actual positive small state with its own successful retained completion.

    def initialJoint (htotal : (∑ i,r i)=∑ j,c j) : PaperStateJoint r c :=
…

    Mentions: OAI.ContingencyTables.SmallGraphProfiles.PaperStateJoint

  3. lemma OAI.ContingencyTables.SmallGraphProfiles.initialJoint_success line 39
  4. def OAI.ContingencyTables.SmallGraphProfiles.greedyFibre line 48

    Source documentation

    A fallback is computed for the current residual margins, then moved back through the entry-preserving completion equivalence.

    def greedyFibre (z : PaperStates r c) : PaperFibre r c z :=
…

    Mentions: OAI.ContingencyTables.SmallGraphProfiles.PaperStates, OAI.ContingencyTables.SmallGraphProfiles.PaperFibre