Browkin and Brzeziński's 1994 result

def BB94.C (k j : ℕ) : ℕ

The coefficient of x^j in the paper's f_k(x). This is OEIS A111125.

Equations

• BB94.C k j = (k + j).choose (2 * j) + 2 * (k + j).choose (2 * j + 1)

theorem BB94.C_eq_zero_iff {k j : ℕ} : C k j = 0 ↔ k < j

theorem BB94.C_pos_iff {k j : ℕ} : 0 < C k j ↔ j ≤ k

theorem BB94.C_eq_zero_of_lt {k j : ℕ} : k < j → C k j = 0

Alias of the reverse direction of BB94.C_eq_zero_iff.

@[simp]

theorem BB94.C_zero {k : ℕ} : C k 0 = 2 * k + 1

@[simp]

theorem BB94.C_self {k : ℕ} : C k k = 1

theorem BB94.C_add_two_add_one {k j : ℕ} : C (k + 2) (j + 1) = 2 * C (k + 1) (j + 1) + C (k + 1) j - C k (j + 1)

theorem BB94.C_mono_right {j : ℕ} : Monotone fun (x : ℕ) => C x j

theorem BB94.C_le {k j : ℕ} : C k (j + 1) ≤ 2 * C (k + 1) (j + 1) + C (k + 1) j

theorem BB94.sum_range_C_mul {k : ℕ} (x y : ℤ) : x ^ (2 * k + 1) + y ^ (2 * k + 1) = ∑ j ∈ Finset.range (k + 1), ↑(C k j) * (x + y) ^ (2 * j + 1) * (-x * y) ^ (k - j)

def BB94.tup (n k : ℕ) (i : Fin (n + 3)) : ℤ

The sequence of n+3-tuples providing a lower bound of 2n+1 on the quality (i.e. 2n-5 for n-tuples where n ≥ 3). k moves between tuples and i is the tuple index.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem BB94.tup_last {n k : ℕ} : tup n k (Fin.last (n + 2)) = 1

@[simp]

theorem BB94.tup_second_last {n k : ℕ} : tup n k (Fin.last (n + 1)).castSucc = -(2 ^ k) ^ (2 * n + 1)

@[simp]

theorem BB94.tup_except_last_two {n k : ℕ} {i : Fin (n + 1)} : tup n k i.castSucc.castSucc = ↑(C n ↑i) * (2 ^ k - 1) ^ (2 * ↑i + 1) * (2 ^ k) ^ (n - ↑i)

theorem BB94.injective_tup {n : ℕ} : Function.Injective (tup n)

theorem BB94.sum_tup {n k : ℕ} : ∑ i : Fin (n + 3), tup n k i = 0

theorem BB94.gcd_tup {n k : ℕ} : Finset.univ.gcd (tup n k) = 1

theorem BB94.tup_sign {n k : ℕ} {i : Fin (n + 3)} (hk : k ≠ 0) : 0 < tup n k i ↔ i ≠ (Fin.last (n + 1)).castSucc

theorem BB94.SSC_tup {n k : ℕ} (hk : k ≠ 0) : SSC (tup n k)

theorem BB94.tup_mem_nConjectureTuples {n k : ℕ} (hk : k ≠ 0) : tup n k ∈ nConjectureTuples (n + 3)

theorem BB94.maxAbs_tup {n k : ℕ} : maxAbs (tup n k) = (2 ^ k) ^ (2 * n + 1)

theorem BB94.radical_prod_tup_dvd {n k : ℕ} : UniqueFactorizationMonoid.radical (∏ i : Fin (n + 3), tup n k i) ∣ ↑(∏ j ∈ Finset.range (n + 1), C n j) * (2 ^ k - 1) * 2

theorem BB94.one_lt_radical_prod_tup {n k : ℕ} (hk : k ≠ 0) : 1 < UniqueFactorizationMonoid.radical (∏ i : Fin (n + 3), tup n k i)

theorem BB94.log_radical_prod_tup_le {n k : ℕ} (hk : k ≠ 0) : Real.log ↑(UniqueFactorizationMonoid.radical (∏ i : Fin (n + 3), tup n k i)) ≤ Real.log (2 * ↑(∏ j ∈ Finset.range (n + 1), C n j)) + ↑k * Real.log 2

theorem BB94.le_tupleQuality {n k : ℕ} (hk : k ≠ 0) : ENNReal.ofReal ((2 * ↑n + 1) * (↑k * Real.log 2) / (Real.log (2 * ↑(∏ j ∈ Finset.range (n + 1), C n j)) + ↑k * Real.log 2)) ≤ tupleQuality (tup n k)

theorem BB94.liminf_tupleQuality_tup {n : ℕ} : ↑(2 * n + 1) ≤ Filter.liminf (tupleQuality ∘ tup n) Filter.atTop

theorem le_quality_nConjectureTuples {n : ℕ} (hn : 3 ≤ n) : ↑(2 * n - 5) ≤ quality (nConjectureTuples n)

Theorem 1.3 in the paper, Browkin and Brzeziński (1994).