OAI/Combinatorics/ContingencyTables/Machines/ResidualDenseProgram.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

A computed dense completion call from a retained small profile

  1. abbrev OAI.ContingencyTables.ProfilePrograms.ResidualParameters line 11
  2. abbrev OAI.ContingencyTables.ProfilePrograms.ResidualDrawData line 12
  3. def OAI.ContingencyTables.ProfilePrograms.residualParameters line 14
  4. def OAI.ContingencyTables.ProfilePrograms.residualParametersRealizer line 17
  5. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_residualParameters line 26
  6. def OAI.ContingencyTables.ProfilePrograms.residualDenseDraw line 33
  7. def OAI.ContingencyTables.ProfilePrograms.residualDenseDrawRealizer line 36
  8. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_residualDenseDraw line 42

    Source documentation

    The actual completion call computes the residual margins, selects their large rectangle, initializes it, and draws a dense matrix.

    theorem polynomial_residualDenseDraw : PolynomialTime residualDenseDrawRealizer :=
…

    Mentions: OAI.ContingencyTables.ProfilePrograms.residualDenseDrawRealizer