OAI/Combinatorics/ContingencyTables/Sampling/SmallGraphProfiles.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ContingencyTables.SmallGraphProfiles.Balanced line 19
2. def OAI.ContingencyTables.SmallGraphProfiles.SingleDefect line 22
3. def OAI.ContingencyTables.SmallGraphProfiles.Pattern line 26
4. abbrev OAI.ContingencyTables.SmallGraphProfiles.Profiles line 29
5. lemma OAI.ContingencyTables.SmallGraphProfiles.balanced_not_defect line 32
6. lemma OAI.ContingencyTables.SmallGraphProfiles.assemble_injective line 39
7. lemma OAI.ContingencyTables.SmallGraphProfiles.assemble_removeOne line 48

   Source documentation

   Fixing a prefix and reindexing preserves every actual unit removal.

   lemma assemble_removeOne (small : I → J → Bool) (s : I×J) (hs : small s.1 s.2=true)
       (σ : I×J → ℕ) (U : ℕ) {n : ℕ} (e : Fin n ≃ Later small s)
       (v : Coordinates Bool (widths (fun _ : Fin n => U)) → ℕ)
       (i : Coordinates Bool (widths (fun _ : Fin n => U))) :
       assemble small s hs σ U e (removeOne v i)=
         removeOne (assemble small s hs σ U e v) (contextEquiv small s hs e U (.inr i)) := by
   …

8. theorem OAI.ContingencyTables.SmallGraphProfiles.assemble_exchange_adjacent line 66

   Source documentation

   Every contextual transport edge is an actual doubled-small-coordinate unit exchange, with no move involving the retained prefix.

   theorem assemble_exchange_adjacent (small : I → J → Bool) (s : I×J)
       (hs : small s.1 s.2=true) (σ : I×J → ℕ) (U : ℕ) {n : ℕ}
       (e : Fin n ≃ Later small s)
       (X Y : Coordinates Bool (widths (fun _ : Fin n => U)) → ℕ)
       (hxy : IntegerExchangeAdjacent X Y) :
       IntegerExchangeAdjacent (assemble small s hs σ U e X) (assemble small s hs σ U e Y) := by
   …