OAI/NumberTheory/Ostmann/Arithmetic/ClearedHistoryBounds.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Degree and value control survives clearing every history denominator

  1. def OAI.Ostmann.ClearedHistoryValue.Bounded line 13
  2. theorem OAI.Ostmann.ClearedHistoryValue.bounded_variable line 16
  3. theorem OAI.Ostmann.ClearedHistoryValue.bounded_constant line 21
  4. theorem OAI.Ostmann.ClearedHistoryValue.bounded_prod line 26
  5. theorem OAI.Ostmann.ClearedHistoryValue.bounded_pivot line 40

    Source documentation

    No coefficient-height estimate is assumed. The exact two products in the substitution give a value bound that is valid at every real assignment.

    theorem bounded_pivot (left right : ClearedHistoryValue σ) (v w s : ℤ) (hs : s ≠ 0)
    (x : σ → ℝ) (HL HR : ℝ) (hL : left.Bounded x HL) (hR : right.Bounded x HR) :
    (pivot left right v w s hs).Bounded x
      ((|(v : ℝ)| + |(w : ℝ)| + |(s : ℝ)|) * HL * HR) := by
…

    Mentions: OAI.Ostmann.ClearedHistoryValue, OAI.Ostmann.ClearedHistoryValue.pivot, OAI.Ostmann.ClearedHistoryValue.Bounded

  6. theorem OAI.Ostmann.ClearedHistoryValue.zero_variable_value_bound line 72