OAI/Combinatorics/ContingencyTables/Transport/BalancedJointConstruction.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ContingencyTables.SmallGraphProfiles.tableWord line 17
2. lemma OAI.ContingencyTables.SmallGraphProfiles.tableWord_false line 22
3. lemma OAI.ContingencyTables.SmallGraphProfiles.tableWord_true line 29
4. def OAI.ContingencyTables.SmallGraphProfiles.jointOfTable line 38

   Source documentation

   Residual feasibility and the literal small-cell bound suffice to construct the balanced profile together with every retained large entry.

   noncomputable def jointOfTable (small : I → J → Bool) (B : I → J → ℕ)
       (r : I → ℕ) (c : J → ℕ) (L U : ℕ)
       (hB : ∀ i j,small i j=true → B i j=U)
       (Y : Table (fun i => r i+rowLargeCount small i*L) (fun j => c j+columnLargeCount small j*L))
       (hY : ∀ i j,small i j=true → Y.val i j ≤ U)
       (hR : ∀ i,smallRow small Y.val i ≤ r i)
       (hC : ∀ j,smallColumnView small Y.val j ≤ c j)
       (hlarge : ∀ i j,small i j=false → Y.val i j ≤ B i j) : BalancedJoint small B r c L U :=
   …

   Mentions: OAI.ContingencyTables.Table, OAI.ContingencyTables.smallColumnView, OAI.ContingencyTables.SmallGraphProfiles.BalancedJoint

5. lemma OAI.ContingencyTables.SmallGraphProfiles.jointOfTable_projection line 54