OAI/NumberTheory/Ostmann/Arithmetic/MovingGiantPolynomial.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.PolynomialGiantRows.denominator_movingReverse line 13
2. theorem OAI.Ostmann.PolynomialGiantRows.usesOnly_movingReverse line 18
3. theorem OAI.Ostmann.PolynomialGiantRows.valueLE_movingReverse line 27
4. def OAI.Ostmann.movingPolynomialAncestors line 39
5. theorem OAI.Ostmann.movingPolynomialAncestors_denominator line 44
6. theorem OAI.Ostmann.movingPolynomialAncestors_det line 54
7. theorem OAI.Ostmann.movingPolynomialAncestors_degree line 70
8. theorem OAI.Ostmann.movingPolynomialAncestors_usesOnly line 84
9. theorem OAI.Ostmann.movingPolynomialAncestors_value line 95
10. def OAI.Ostmann.movingHistoryLine line 112
11. theorem OAI.Ostmann.movingHistoryLine_nonzero line 117

    Source documentation

    Nonvanishing needed before the current compensation prime is sampled.

    theorem movingHistoryLine_nonzero {σ K : Type*} [Field K]
        (steps : List (PolynomialReversal σ)) (v w : MvPolynomial σ ℤ)
        (φ : MvPolynomial σ ℤ →+* K)
        (h : ∀ s ∈ steps, φ s.v ≠ 0 ∧ φ s.w ≠ 0 ∧ φ s.u ≠ 0)
        (hv : φ v ≠ 0) (hw : φ w ≠ 0) :
        φ (movingHistoryLine steps v w).a ≠ 0 ∨ φ (movingHistoryLine steps v w).b ≠ 0 := by
    …

    Mentions: OAI.Ostmann.PolynomialReversal, OAI.Ostmann.movingHistoryLine

12. theorem OAI.Ostmann.movingHistoryLine_degree line 135

    Source documentation

    Concrete degree bound for the coefficient tests in the ancestor ordering.

    theorem movingHistoryLine_degree {σ : Type*}
        (steps : List (PolynomialReversal σ)) (v w : MvPolynomial σ ℤ)
        (d : ℕ) (hs : ∀ s ∈ steps,
          s.v.totalDegree ≤ d ∧ s.w.totalDegree ≤ d ∧ s.u.totalDegree ≤ d)
        (hv : v.totalDegree ≤ d) (hw : w.totalDegree ≤ d) :
        (movingHistoryLine steps v w).a.totalDegree ≤ (steps.length + 1) * d ∧
          (movingHistoryLine steps v w).b.totalDegree ≤ (steps.length + 1) * d := by
    …

    Mentions: OAI.Ostmann.PolynomialReversal, OAI.Ostmann.movingHistoryLine

13. theorem OAI.Ostmann.movingHistoryLine_value line 146
14. theorem OAI.Ostmann.movingHistoryLine_vars_subset line 160