OAI/NumberTheory/Ostmann/Construction/HistorySubstitution.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Substitution constructs the actual rational expressions of a reversed history

  1. def OAI.Ostmann.HistoryFormula.value line 11
  2. def OAI.Ostmann.HistoryFormula.bind line 13
  3. theorem OAI.Ostmann.HistoryFormula.value_prime line 19
  4. theorem OAI.Ostmann.HistoryFormula.value_external line 22
  5. theorem OAI.Ostmann.HistoryFormula.value_product line 25
  6. theorem OAI.Ostmann.HistoryFormula.value_solve line 30
  7. theorem OAI.Ostmann.HistoryFormula.value_bind line 34
  8. theorem OAI.Ostmann.HistoryFormula.cost_bind_le line 44

    Source documentation

    A fixed number of substitutions multiplies the expression-size bound; for fixed transfer depth this remains a polynomial in the word length.

    theorem cost_bind_le (F : HistoryFormula σ) (f : σ → HistoryFormula τ)
    (C : ℕ) (hC : 1 ≤ C) (hf : ∀ i, (f i).cost ≤ C) :
    (F.bind f).cost ≤ C * F.cost := by
…

    Mentions: OAI.Ostmann.HistoryFormula, OAI.Ostmann.HistoryFormula.cost

  9. theorem OAI.Ostmann.HistoryFormula.inputsBounded_bind line 57
  10. def OAI.Ostmann.HistoryFormula.listProduct line 66
  11. theorem OAI.Ostmann.HistoryFormula.value_listProduct line 70
  12. theorem OAI.Ostmann.HistoryFormula.cost_listProduct line 76
  13. def OAI.Ostmann.HistoryFormula.replace line 82
  14. theorem OAI.Ostmann.HistoryFormula.value_replace line 86