Power bounds for large residual Sylvester-Schur estimates

LemmaA linear bound by a power of four#✓fully proved

For every natural number \(n \ge 512\), \(n \le 4^{\lfloor n/128 \rfloor + 1}\).

lemma self_le_four_pow_div_one_twenty_eight_add_one {n : ℕ} (hn : 512 ≤ n) :
    n ≤ 4 ^ (n / 128 + 1)

Used by 2

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

LemmaPowers of two against powers of three#✓fully proved

For every natural number \(n\), \(2^{19 \lfloor n/12 \rfloor} \le 3^{n}\).

lemma two_pow_nineteen_mul_div_twelve_le_three_pow (n : ℕ) :
    2 ^ (19 * (n / 12)) ≤ 3 ^ n

Used by 2

Used byA power comparison for the central-offset estimate · Scaled ternary bound for the first residual estimate

LemmaA power comparison for the central-offset estimate#✓fully proved

Let \(D\), \(E\), \(i\), \(n\) be natural numbers with \(2D + i + 2E < 19 \lfloor i/12 \rfloor + 2n\). Then \(4^{D} \cdot 2^{i} \cdot 4^{E} < 3^{i} \cdot 4^{n}\).

lemma four_pow_mul_two_pow_mul_four_pow_lt_three_pow_mul_four_pow
    {D E i n : ℕ} (hexp : 2 * D + i + 2 * E < 19 * (i / 12) + 2 * n) :
    4 ^ D * (2 ^ i * 4 ^ E) < 3 ^ i * 4 ^ n

Uses 1 · Used by 1

Proof usesPowers of two against powers of three

Used byCentral-offset residual bound

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.