OAI/Combinatorics/ContingencyTables/Rooted/RootedPhysicalTables.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Feasible physical tables retain unit mass for the selected roots

  1. theorem OAI.ContingencyTables.RootedPhysicalTables.feasible_weight_one line 17
  2. theorem OAI.ContingencyTables.RootedPhysicalTables.table_count_le_mass line 25

    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) (R : RootedCompletion.Selection A.T) (alpha : ℝ) :
    (Fintype.card (BoundedTable (fun i => (A.r i).toNat) (fun j => (A.c j).toNat) A.b):ℝ) ≤
      RootedPhysicalNormalizer.physicalMass A R alpha := by
…

    Mentions: OAI.ContingencyTables.RootedCompletion.Selection, OAI.ContingencyTables.BoundedTable, OAI.ContingencyTables.RootedPhysicalNormalizer.physicalMass