OAI/NumberTheory/Ostmann/Arithmetic/ClearedHistoryPivot.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.Ostmann.ClearedHistoryValue line 12
2. def OAI.Ostmann.ClearedHistoryValue.ofVariable line 21
3. def OAI.Ostmann.ClearedHistoryValue.constant line 23
4. def OAI.Ostmann.ClearedHistoryValue.prod line 25
5. def OAI.Ostmann.ClearedHistoryValue.pivot line 32

   Source documentation

   This is exactly (v * right - w * left) / s, with integer clearing of all previously inserted denominators.

   noncomputable def pivot (left right : ClearedHistoryValue σ) (v w s : ℤ) (hs : s ≠ 0) :
       ClearedHistoryValue σ :=
   …

   Mentions: OAI.Ostmann.ClearedHistoryValue

6. def OAI.Ostmann.ClearedHistoryValue.eval line 39
7. theorem OAI.Ostmann.ClearedHistoryValue.eval_variable line 42
8. theorem OAI.Ostmann.ClearedHistoryValue.eval_constant line 45
9. theorem OAI.Ostmann.ClearedHistoryValue.eval_prod line 49
10. theorem OAI.Ostmann.ClearedHistoryValue.eval_pivot line 55
11. theorem OAI.Ostmann.ClearedHistoryValue.degree_prod line 65
12. theorem OAI.Ostmann.ClearedHistoryValue.degree_pivot line 69
13. theorem OAI.Ostmann.ClearedHistoryValue.denominator_pivot_unit line 83

    Source documentation

    A prime absent from the small-frequency denominator remains absent after the next substitution.

    theorem denominator_pivot_unit (left right : ClearedHistoryValue σ)
        (v w s : ℤ) (hs : s ≠ 0) (p : ℕ) (hp : p.Prime)
        (hL : ¬p ∣ left.denominator.natAbs) (hR : ¬p ∣ right.denominator.natAbs)
        (hS : ¬p ∣ s.natAbs) : ¬p ∣ (pivot left right v w s hs).denominator.natAbs := by
    …

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

14. theorem OAI.Ostmann.ClearedHistoryValue.integer_value_cleared line 91

    Source documentation

    Polynomial evaluation at an integer assignment is the numerator of the actual rational value. The equality is useful on the integrality support.

    theorem integer_value_cleared (F : ClearedHistoryValue σ) (x : σ → ℤ) (y : ℤ)
        (hy : F.eval (fun i => (x i : ℚ)) = y) :
        MvPolynomial.eval₂Hom (RingHom.id ℤ) x F.numerator = F.denominator * y := by
    …

    Mentions: OAI.Ostmann.ClearedHistoryValue

15. theorem OAI.Ostmann.ClearedHistoryValue.prime_coprime_integer_value line 104