OAI/Combinatorics/ContingencyTables/Dense/DenseAffine.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Free coordinates of a dense completion block

none denotes the pivot row or column. The free coordinates are the other cells. These are the manuscript's actual affine completion formulas; the row and column constraints hold identically, and feasible tables are uniquely determined by their free cells.

  1. def OAI.ContingencyTables.DenseAffine.table line 22
  2. theorem OAI.ContingencyTables.DenseAffine.table_rows line 29
  3. theorem OAI.ContingencyTables.DenseAffine.table_columns line 39
  4. theorem OAI.ContingencyTables.DenseAffine.table_unique line 50
  5. theorem OAI.ContingencyTables.DenseAffine.table_recover line 74

    Source documentation

    Recover an actual table from its scaled free coordinates.

    theorem table_recover (R : Option I → ℝ) (P : Option J → ℝ) (w : I → J → ℝ)
    (hw : ∀ i j, w i j ≠ 0) (X : Option I → Option J → ℝ)
    (hR : ∀ i, ∑ j, X i j = R i) (hP : ∀ j, ∑ i, X i j = P j) :
    table R P w (fun p => X (some p.1) (some p.2) / w p.1 p.2) = X := by
…

    Mentions: OAI.ContingencyTables.DenseAffine.table