OAI/Combinatorics/ContingencyTables/Transport/FiniteRepairDegree.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.ContingencyTables.IntegerWeightedTransport.outgoing_repair_card_le line 16

   Source documentation

   If the source encoding is injective there is at most one outgoing repair at a fixed state.

   theorem outgoing_repair_card_le (x y : D → X) (hx : Function.Injective x) (v : X) :
       ((Finset.univ.filter (fun d => x d=v)).image y).card ≤ 1 := by
   …

2. theorem OAI.ContingencyTables.IntegerWeightedTransport.incoming_repair_card_le line 26

   Source documentation

   The ordered defect type and repaired profile identify the source. Consequently a fixed target has at most one inverse repair of each type.

   theorem incoming_repair_card_le (x y : D → X) (label : D → T)
       (h : Function.Injective (fun d => (label d,y d))) (v : X) :
       ((Finset.univ.filter (fun d => y d=v)).image x).card ≤ Fintype.card T := by
   …

3. def OAI.ContingencyTables.IntegerWeightedTransport.repairNeighbors line 40
4. lemma OAI.ContingencyTables.IntegerWeightedTransport.mem_repairNeighbors_forward line 45
5. lemma OAI.ContingencyTables.IntegerWeightedTransport.mem_repairNeighbors_reverse line 52
6. theorem OAI.ContingencyTables.IntegerWeightedTransport.repairNeighbors_card_le line 58