Scaled ternary bound for the Sylvester-Schur large residual estimate

3 fully proved

Algebraic reductions

LemmaSquare root bound on a linear range#✓fully proved

Let \(n\) and \(N\) be natural numbers with \(900 \le n\) and \(N \le 4n\). Then \(\lfloor \sqrt{N} \rfloor \le \lfloor n/15 \rfloor\).

lemma sqrt_le_div_fifteen_of_le_four_mul {n N : ℕ} (hn : 900 ≤ n)
    (hNhi : N ≤ 4 * n) :
    Nat.sqrt N ≤ n / 15

Used by 2

Used byScaled ternary bound for the first residual estimate · Central-offset residual bound

LemmaCube root times logarithm on a linear range#✓fully proved

Let \(n\) and \(N\) be natural numbers with \(945 \le n\) and \(N \le 4n\). Then \(\lfloor N^{1/3} \rfloor \cdot \lfloor \log_2 N \rfloor \le \lfloor n/5 \rfloor\), where \(\lfloor \log_2 N \rfloor\) is read as \(0\) when \(N = 0\).

lemma nthRoot_three_mul_log_le_one_fifth_of_le_four_mul {n N : ℕ}
    (hn : 945 ≤ n) (hNhi : N ≤ 4 * n) :
    Nat.nthRoot 3 N * Nat.log 2 N ≤ n / 5

Used by 2

Used byScaled ternary bound for the first residual estimate · Central-offset residual bound

Range dispatch

LemmaScaled ternary bound for the first residual estimate#✓fully proved

Let \(n\) and \(N\) be natural numbers with \(945 \le n\) and \(3n \le N \le n^2 + n\). Then

\[ n \cdot 2^{n} \cdot (3n)^{n} \cdot 4^{n + \lfloor \sqrt{N} \rfloor + \lfloor N^{1/3} \rfloor \lfloor \log_2 N \rfloor} < 3^{n} \cdot 4^{n} \cdot N^{n}. \]

lemma first_residual_large_scaled_ternary_bound {n N : ℕ}
    (hn : 945 ≤ n) (hNlo : 3 * n ≤ N) (hNhi : N ≤ n ^ 2 + n) :
    n * (2 ^ n * ((3 * n) ^ n *
      4 ^ (n + Nat.sqrt N + Nat.nthRoot 3 N * Nat.log 2 N))) <
      3 ^ n * 4 ^ n * N ^ n

Uses 4 · Used by 1

Proof usesCube root times logarithm on a linear range · A linear bound by a power of four · Square root bound on a linear range · Powers of two against powers of three

Used byErdős key lemma

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.