Dyadic fractions in ℝ≥0∞

A count c out of 2 ^ n equally likely strings is a probability c / 2 ^ n. Bounded-error acceptance thresholds compare it with 2 / 3; this file turns that comparison into one between natural numbers.

Main results

• ENNReal.two_div_three_le_natCast_div_two_pow_iff: 2 / 3 ≤ c / 2 ^ n ↔ 2 * 2 ^ n ≤ 3 * c.

theorem ENNReal.two_div_three_le_natCast_div_two_pow_iff {c n : ℕ} : 2 / 3 ≤ ↑c / 2 ^ n ↔ 2 * 2 ^ n ≤ 3 * c

A dyadic fraction c / 2 ^ n is at least two thirds exactly when 2 * 2 ^ n ≤ 3 * c.