OAI/Combinatorics/ContingencyTables/Dense/DenseExponentListSemantics.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The binary list exponent equals the geometric dense exponent

  1. def OAI.ContingencyTables.DensePrograms.exponentDataCode line 13
  2. lemma OAI.ContingencyTables.DensePrograms.optionIndex_lt line 17
  3. lemma OAI.ContingencyTables.DensePrograms.exists_optionIndex line 22
  4. lemma OAI.ContingencyTables.DensePrograms.exponentCell_code line 28
  5. lemma OAI.ContingencyTables.DensePrograms.mem_exponentCells_code line 37
  6. theorem OAI.ContingencyTables.DensePrograms.fullExponent_code line 46

    Source documentation

    The list maximum contains every cell once; its initial zero accounts for the extra zero component in the nonnegative rational penalty.

    theorem fullExponent_code {q K : ℕ} (R : Option (Fin m) → ℕ)
    (P : Option (Fin n) → ℕ) (d : ℕ) (e : Fin m×Fin n ≃ Fin q)
    (a : Grid (I := Fin q) K) :
…