Documentation
LeanPool
.
NairTenenbaum
.
Contributions
.
ShortIntervalCongruenceUpper
Search
return to top
source
Imports
Init
LeanPool.NairTenenbaum.Arithmetic.CongruenceCount
LeanPool.NairTenenbaum.Contributions.ShortIntervalCardinality
Imported by
NairTenenbaum
.
shortInterval_polynomial_congruence_count_le
Upper congruence counts with the rounding error retained
#
source
theorem
NairTenenbaum
.
shortInterval_polynomial_congruence_count_le
(
Q
:
Polynomial
ℤ
)
{
x
y
:
ℝ
}
(
hx
:
0
≤
x
)
(
hy
:
0
≤
y
)
{
q
:
ℕ
}
(
hq
:
0
<
q
)
:
↑
{
n
∈
shortInterval
x
y
|
q
∣
(
Polynomial.eval
(↑
n
)
Q
)
.
natAbs
}
.
card
≤
(
y
+
1
)
*
↑
(
rootCount
Q
q
)
/
↑
q
+
↑
(
rootCount
Q
q
)