OAI/Combinatorics/ContingencyTables/Dense/DenseExponentProgram.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Binary execution of one dense exponent component

  1. abbrev OAI.ContingencyTables.DensePrograms.ComponentData line 11
  2. def OAI.ContingencyTables.DensePrograms.eighthPower line 13
  3. lemma OAI.ContingencyTables.DensePrograms.polynomial_eighthPower line 19
  4. def OAI.ContingencyTables.DensePrograms.componentValue line 22
  5. def OAI.ContingencyTables.DensePrograms.componentRealizer line 25
  6. theorem OAI.ContingencyTables.DensePrograms.polynomial_component line 42

    Source documentation

    Cost is polynomial in the binary data, even when the represented margin values and the quotient are large.

    theorem polynomial_component : PolynomialTime componentRealizer := by
…

    Mentions: OAI.ContingencyTables.DensePrograms.componentRealizer

  7. theorem OAI.ContingencyTables.DensePrograms.componentValue_eq_floor line 69