OAI/Combinatorics/ContingencyTables/Counting/CompanionPhysicalTables.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ContingencyTables.CompanionPhysicalTables.physicalTable line 16
2. def OAI.ContingencyTables.CompanionPhysicalTables.Feasible line 19
3. abbrev OAI.ContingencyTables.CompanionPhysicalTables.PhysicalTables line 24
4. lemma OAI.ContingencyTables.CompanionPhysicalTables.row_nonnegative line 26
5. lemma OAI.ContingencyTables.CompanionPhysicalTables.column_nonnegative line 30
6. lemma OAI.ContingencyTables.CompanionPhysicalTables.physicalTable_assignment line 34
7. lemma OAI.ContingencyTables.CompanionPhysicalTables.assignment_physicalTable line 43
8. def OAI.ContingencyTables.CompanionPhysicalTables.toBounded line 50
9. def OAI.ContingencyTables.CompanionPhysicalTables.fromBounded line 70
10. lemma OAI.ContingencyTables.CompanionPhysicalTables.toBounded_integer line 92
11. lemma OAI.ContingencyTables.CompanionPhysicalTables.fromBounded_table line 97
12. lemma OAI.ContingencyTables.CompanionPhysicalTables.physicalTable_injective line 103
13. def OAI.ContingencyTables.CompanionPhysicalTables.tablesEquiv line 113

    Source documentation

    The terminal feasible-profile count is the original bounded-table count, with the instance's necessarily nonnegative margins.

    noncomputable def tablesEquiv (A : Instance I J) :
        PhysicalTables A ≃ BoundedTable (fun i => (A.r i).toNat) (fun j => (A.c j).toNat) A.b where
    …

    Mentions: OAI.ContingencyTables.CompanionPhysicalTables.PhysicalTables, OAI.ContingencyTables.BoundedTable

14. theorem OAI.ContingencyTables.CompanionPhysicalTables.cardinality_eq line 132
15. theorem OAI.ContingencyTables.CompanionPhysicalTables.feasible_weight_one line 137
16. theorem OAI.ContingencyTables.CompanionPhysicalTables.table_count_le_mass line 146

    Source documentation

    Every original bounded table contributes exactly one unit, so the actual normalizer always dominates the table count.

    theorem table_count_le_mass (A : Instance I J) (alpha : ℝ) :
        (Fintype.card (BoundedTable (fun i => (A.r i).toNat) (fun j => (A.c j).toNat) A.b):ℝ) ≤
          CompanionPhysicalNormalizer.physicalMass A alpha := by
    …

    Mentions: OAI.ContingencyTables.BoundedTable, OAI.ContingencyTables.CompanionPhysicalNormalizer.physicalMass