OAI/Combinatorics/ContingencyTables/Transport/ExcessPairCoordinates.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ContingencyTables.IntegerWeightedTransport.coordinateEquiv_symm_root_succ line 13
2. lemma OAI.ContingencyTables.IntegerWeightedTransport.coordinateEquiv_symm_zero line 17
3. lemma OAI.ContingencyTables.IntegerWeightedTransport.coordinateEquiv_symm_succ line 20
4. lemma OAI.ContingencyTables.IntegerWeightedTransport.embedding_root line 25
5. lemma OAI.ContingencyTables.IntegerWeightedTransport.embedding_pair_total line 32
6. def OAI.ContingencyTables.IntegerWeightedTransport.excessIndex line 46
7. lemma OAI.ContingencyTables.IntegerWeightedTransport.excessEmbedding_root line 51
8. lemma OAI.ContingencyTables.IntegerWeightedTransport.excessEmbedding_pair_total line 69

   Source documentation

   The raw finite profile recovers the distinguished position by its pair total; all other pairs have their original total.

   lemma excessEmbedding_pair_total {S : Type*} {n : ℕ} (M : Fin n → ℕ) (z : S → ℕ)
       (q : ExcessAssignments (widths M)) (i : Fin n) :
       excessEmbedding (widths M) z q ((coordinateEquiv S M).symm (.inr (i,false)))+
         excessEmbedding (widths M) z q ((coordinateEquiv S M).symm (.inr (i,true)))=
         M i+if i=excessIndex M q then 1 else 0 := by
   …

   Mentions: OAI.ContingencyTables.IntegerWeightedTransport.ExcessAssignments, OAI.ContingencyTables.IntegerWeightedTransport.excessEmbedding, OAI.ContingencyTables.IntegerWeightedTransport.excessIndex