Numeric inequalities for Tran–Vu’s covering induction (L = 1000).

noncomputable def KahnKalai.kmin (ℓ : ℕ) : ℕ

Least integer strictly larger than 0.9 ℓ.

Equations

• KahnKalai.kmin ℓ = ⌊9 / 10 * ↑ℓ⌋₊ + 1

theorem KahnKalai.kmin_pos (ℓ : ℕ) : 1 ≤ kmin ℓ

theorem KahnKalai.kmin_gt (ℓ : ℕ) : 9 / 10 * ↑ℓ < ↑(kmin ℓ)

theorem KahnKalai.kmin_le_add_one (ℓ : ℕ) : ↑(kmin ℓ) ≤ 9 / 10 * ↑ℓ + 1

theorem KahnKalai.kmin_le (ℓ : ℕ) (hℓ : 1 ≤ ℓ) : kmin ℓ ≤ ℓ

theorem KahnKalai.eleven_mul_kmin_le (ℓ : ℕ) (hℓ : 1 ≤ ℓ) : 11 * kmin ℓ ≤ 10 * (ℓ + 1)

theorem KahnKalai.two_rpow_one_div_ten_le : 2 ^ (1 / 10) ≤ 11 / 10

theorem KahnKalai.fifty_pow_le_hundred_rpow : 50 ≤ 100 ^ (9 / 10)

theorem KahnKalai.fifty_pow_le_hundred_kmin (ℓ : ℕ) : 50 ^ ℓ ≤ 100 ^ kmin ℓ

theorem KahnKalai.fortyfour_eight_le_three_fifty (ℓ : ℕ) (hℓ : 2 ≤ ℓ) : 44 * 8 ^ ℓ ≤ 3 * 50 ^ ℓ

theorem KahnKalai.eleven_two_pow_le_twelve_fifty (ℓ : ℕ) (hℓ : 2 ≤ ℓ) : 11 * 2 ^ (3 * ℓ + 4) ≤ 12 * 50 ^ ℓ

theorem KahnKalai.eleven_two_pow_le_twelve_hundred (ℓ : ℕ) (hℓ : 2 ≤ ℓ) : 11 * 2 ^ (3 * ℓ + 4) ≤ 12 * 100 ^ kmin ℓ

theorem KahnKalai.choose_geom_tail_le (ℓ : ℕ) : ∑ k ∈ Finset.Icc (kmin ℓ) ℓ, (1 / 100) ^ k * ↑(ℓ.choose k) ≤ (1 / 100) ^ kmin ℓ * 2 ^ ℓ

theorem KahnKalai.bad_frac_le_of_two (ℓ : ℕ) (hℓ : 2 ≤ ℓ) : (1 / 100) ^ kmin ℓ * 2 ^ ℓ * 2 ^ (ℓ + 2) ≤ 12 / 11 * (1 / 2 ^ (ℓ + 2))

theorem KahnKalai.bad_frac_le_one : 1 / 100 * 2 ^ (1 + 2) ≤ 12 / 11 * (1 / 2 ^ (1 + 2))

theorem KahnKalai.frac_gap (ℓ : ℕ) (hℓ : 1 ≤ ℓ) : 1 / 2 ^ (ℓ + 2) ≤ 1 / 2 ^ (kmin ℓ - 1 + 2) - 1 / 2 ^ (ℓ + 2)

theorem KahnKalai.two_div_three_add_le : 2 / 3 + 1 / 2 ^ (0 + 2) ≤ 11 / 12

theorem KahnKalai.occupation_mul_le (ℓ : ℕ) (hℓ : 1 ≤ ℓ) {β : ℝ} (hβ : β ≤ 12 / 11 * (1 / 2 ^ (ℓ + 2))) : 2 / 3 + 1 / 2 ^ (ℓ + 2) ≤ (2 / 3 + 1 / 2 ^ (kmin ℓ - 1 + 2)) * (1 - β)