OAI/Combinatorics/ContingencyTables/Counting/CompanionHistorySize.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Polynomial stored size throughout the adaptive history fold

  1. lemma OAI.ContingencyTables.CompanionOuterHistoryProgram.getD_property line 10
  2. lemma OAI.ContingencyTables.CompanionOuterHistoryProgram.old_property line 17
  3. lemma OAI.ContingencyTables.CompanionOuterHistoryProgram.default_height line 25
  4. lemma OAI.ContingencyTables.CompanionOuterHistoryProgram.default_shape line 32
  5. lemma OAI.ContingencyTables.CompanionOuterHistoryProgram.fold_length line 35
  6. lemma OAI.ContingencyTables.CompanionOuterHistoryProgram.fold_fixed line 46
  7. lemma OAI.ContingencyTables.CompanionOuterHistoryProgram.fold_bounds line 52
  8. theorem OAI.ContingencyTables.CompanionOuterHistoryProgram.polynomial_historyFold line 103

    Source documentation

    The loop's live representation has a fixed polynomial bound even on malformed inputs; the only changing numeric values are additive-height fractions.

    theorem polynomial_historyFold : PolynomialTime (fold advanceRealizer) := by
…

    Mentions: OAI.ContingencyTables.CompanionOuterHistoryProgram.advanceRealizer

  9. lemma OAI.ContingencyTables.CompanionOuterHistoryProgram.polynomial_run line 174
  10. lemma OAI.ContingencyTables.CompanionOuterHistoryProgram.polynomial_storedHistory line 178
  11. lemma OAI.ContingencyTables.CompanionOuterHistoryProgram.polynomial_output line 181