OAI/NumberTheory/Ostmann/Characters/IntegerPolynomialBounds.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.integerPolynomial_rational_eval line 13
2. theorem OAI.Ostmann.integerPolynomial_rational_zero_iff line 22
3. theorem OAI.Ostmann.integerPolynomial_rational_degree line 33
4. theorem OAI.Ostmann.int_prime_divisor_card_le line 41

   Source documentation

   A bound on an actual integer test gives the required independent-prime cardinality bound without a separate polynomial-height hypothesis.

   theorem int_prime_divisor_card_le (P : Finset ℕ) (z : ℤ) (hz : z ≠ 0)
       (hprime : ∀ p ∈ P, p.Prime) (B H : ℝ) (hB : 0 < B)
       (hsize : ∀ p ∈ P, B ≤ Real.log (p : ℝ)) (hvalue : |(z : ℝ)| ≤ H) :
       ((P.filter fun p => p ∣ z.natAbs).card : ℝ) ≤ Real.log H / B := by
   …

5. theorem OAI.Ostmann.int_prime_divisor_card_le_power line 55

   Source documentation

   The common-denominator recurrence yields the logarithmic budget for any nonzero cleared coefficient with the established power bound.

   theorem int_prime_divisor_card_le_power (P : Finset ℕ) (z : ℤ) (hz : z ≠ 0)
       (hprime : ∀ p ∈ P, p.Prime) (B H : ℝ) (n : ℕ) (hB : 0 < B)
       (hsize : ∀ p ∈ P, B ≤ Real.log (p : ℝ)) (hvalue : |(z : ℝ)| ≤ H ^ n) :
       ((P.filter fun p => p ∣ z.natAbs).card : ℝ) ≤ (n : ℝ) * Real.log H / B := by
   …