OAI/NumberTheory/Ostmann/Construction/HistoryFormula.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

The actual product-and-pivot formulas of a fixed arithmetic history

  1. inductive OAI.Ostmann.HistoryFormula line 9
  2. def OAI.Ostmann.HistoryFormula.cleared line 19
  3. def OAI.Ostmann.HistoryFormula.cost line 25
  4. def OAI.Ostmann.HistoryFormula.frequencies line 31
  5. def OAI.Ostmann.HistoryFormula.InputsBounded line 37
  6. theorem OAI.Ostmann.HistoryFormula.degree_le_cost line 44
  7. theorem OAI.Ostmann.HistoryFormula.denominator_eq_frequency_product line 58
  8. theorem OAI.Ostmann.HistoryFormula.frequency_count_le_cost line 71
  9. theorem OAI.Ostmann.HistoryFormula.bounded line 82

    Source documentation

    The same bound applies after any subset of independent variables is set to zero; its proof uses only their absolute upper bounds.

    theorem bounded (F : HistoryFormula σ) (x : σ → ℝ) (R : ℝ) (hR : 3 ≤ R)
    (hx : ∀ i, |x i| ≤ R) (hF : F.InputsBounded R) :
    F.cleared.Bounded x (R ^ F.cost) := by
…

    Mentions: OAI.Ostmann.HistoryFormula

  10. theorem OAI.Ostmann.HistoryFormula.zero_variable_bound line 115
  11. theorem OAI.Ostmann.integer_list_product_dvd_power line 130
  12. theorem OAI.Ostmann.HistoryFormula.denominator_test_period line 139