PolynomialValueBounds.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Size of the cleared arithmetic tests at actual prime values

A uniform bound on the slot values gives an explicit bound on every cleared coefficient and denominator. This avoids any assumed bound on the height of newly constructed polynomials.

def OAI.Ostmann.PolynomialGiantRows.ValueLE line 19
theorem OAI.Ostmann.PolynomialGiantRows.valueLE_identity line 23
theorem OAI.Ostmann.PolynomialGiantRows.valueLE_reverse line 27

theorem OAI.Ostmann.PolynomialGiantRows.minor_value_le line 54

Source documentation

A minor of two bounded coefficient rows has the stated elementary size.

theorem minor_value_le (φ : MvPolynomial σ ℤ →+* ℝ) (a b c d : MvPolynomial σ ℤ)
    (H : ℝ) (hH : 0 ≤ H) (ha : |φ a| ≤ H) (hb : |φ b| ≤ H)
    (hc : |φ c| ≤ H) (hd : |φ d| ≤ H) : |φ (a * d - b * c)| ≤ 2 * H ^ 2 := by
…

theorem OAI.Ostmann.polynomialAncestorRows_value line 68
theorem OAI.Ostmann.log_abs_le_of_power_bound line 87
Source documentation
Convert the concrete multiplicative size bound to the logarithmic budget used when counting accidental prime divisors.
```
theorem log_abs_le_of_power_bound (x H : ℝ) (n : ℕ) (hx : x ≠ 0)
    (hbound : |x| ≤ H ^ n) : Real.log |x| ≤ (n : ℝ) * Real.log H := by
…
```