This is verified by computation (native_decide).

Rewriting using \(\left(\frac{a}{b}\right)^n = \frac{a^n}{b^n}\) and combining fractions, the inequality \(\frac{100^{11} \cdot 100^{89}}{11^{11} \cdot 89^{89}} {\lt} 2^{50}\) is equivalent (after clearing the positive denominator \(11^{11} \cdot 89^{89}\)) to \(100^{11} \cdot 100^{89} {\lt} 2^{50} \cdot 11^{11} \cdot 89^{89}\). By the ring identity \(100^{11} \cdot 100^{89} = 100^{100}\), this reduces to \(100^{100} {\lt} 2^{50} \cdot 11^{11} \cdot 89^{89}\), which holds by casting key_nat_ineq to \(\mathbb {R}\).

Unfolding the definition of \(H_2\), the goal becomes

We establish auxiliary facts: \(11/100 {\gt} 0\), \(89/100 {\gt} 0\), \(\log _2(11/100) {\lt} 0\) (since \(11/100 {\lt} 1\) and the base is \({\gt} 1\)), and \(\log _2(89/100) {\lt} 0\) similarly. Using the identity \(\log _2(a/b) = \log _2 a - \log _2 b\), we rewrite:

After substitution and ring normalization, the goal becomes

We establish the key step: \(11 \cdot \log _2(100/11) + 89 \cdot \log _2(100/89) {\lt} 50\). Indeed, taking \(\log _2\) of the inequality \(\left(\frac{100}{11}\right)^{11}\cdot \left(\frac{100}{89}\right)^{89} {\lt} 2^{50}\) from key_frac_ineq, and using \(\log _2(x^n) = n\log _2 x\) and \(\log _2(2^{50}) = 50\), we obtain:

Since \(\log _2(100/11) {\gt} 0\) and \(\log _2(100/89) {\gt} 0\), we conclude by linear arithmetic that \(\frac{11}{100}\log _2\! \left(\frac{100}{11}\right) + \frac{89}{100}\log _2\! \left(\frac{100}{89}\right) {\lt} \frac{1}{2}\).

Unfolding \(H_2(\delta ) = -\delta \log _2\delta - (1-\delta )\log _2(1-\delta )\) and \(\operatorname {binEntropy}(\delta ) = -\delta \log \delta - (1-\delta )\log (1-\delta )\), and using \(\log _2 x = \log x / \log 2\) (i.e., \(\operatorname {logb}\, 2\, x = \log x / \log 2\)), together with \(\log (\cdot ^{-1}) = -\log (\cdot )\), the equality follows by ring arithmetic.

Let \(x \in (0,1)\). We write \(H_2 = \operatorname {binEntropy}(\cdot )/\log 2\) by binaryEntropy_eq_binEntropy_div. Applying Mathlib’s Real.hasDerivAt_binEntropy (which gives derivative \(\log ((1-x)/x)\) for \(\operatorname {binEntropy}\) at \(x\), using \(x \neq 0\) and \(x \neq 1\)), and dividing by the constant \(\log 2\), we obtain that \(H_2\) has a derivative at \(x\). Using \(\log _2((1-x)/x) = (\log (1-x) - \log x)/\log 2 = \log ((1-x)/x)/\log 2\), the result follows.

Let \(a, b \in (0, 1/2)\) with \(a {\lt} b\). Using binaryEntropy_eq_binEntropy_div, we write \(H_2(a) = \operatorname {binEntropy}(a)/\log 2\) and \(H_2(b) = \operatorname {binEntropy}(b)/\log 2\). Since \(\log 2 {\gt} 0\) (as \(1 {\lt} 2\)), it suffices to show \(\operatorname {binEntropy}(a) {\lt} \operatorname {binEntropy}(b)\). Both \(a\) and \(b\) lie in \([0, 2^{-1}]\) (verified by the hypotheses via \(\operatorname {simp}\) and linear arithmetic), and Mathlib’s Real.binEntropy_strictMonoOn asserts strict monotonicity of \(\operatorname {binEntropy}\) on \([0, 1/2]\), giving the result.

Let \(\delta \) satisfy \(0 {\lt} \delta {\lt} 11/100\). We note that \(\delta {\lt} 1/2\) (by linear arithmetic from \(11/100 {\lt} 1/2\)), so \(\delta \in (0, 1/2)\). Also \(11/100 \in (0, 1/2)\). By binaryEntropy_strictMonoOn, since \(\delta {\lt} 11/100\), we have \(H_2(\delta ) {\lt} H_2(11/100)\). By binaryEntropy_at_eleven_hundredths, \(H_2(11/100) {\lt} 1/2\). Chaining these inequalities gives \(H_2(\delta ) {\lt} 1/2\).

This follows immediately by unfolding the definition of \(B_0(r)\) and applying simp.

By extensionality, it suffices to show that no \(v\) belongs to \(B_0(r)\). Suppose \(v \in B_0(r)\); then by simp on the definition, \(\operatorname {wt}(v) \leq r {\lt} 0\). But \(\operatorname {wt}(v) \geq 0\) since it is a natural number cast to \(\mathbb {R}\), a contradiction by linear arithmetic. The other direction is trivial since \(\emptyset \) has no members.

We exhibit the zero vector \(0 \in \mathbb {F}_2^n\) as a witness. By mem_hammingBall, it suffices to show \(\operatorname {wt}(0) \leq r\). Using simp with the definitions of hammingWeight, hammingNorm, and hammingDist_self, we get \(\operatorname {wt}(0) = 0\), and \(0 \leq r\) holds by assumption.

We establish \(0 {\lt} 1 - \delta \) (by linear arithmetic from \(\delta \leq 1/2\)) and \(\delta \leq 1 - \delta \) (since \(\delta \leq 1/2\)). Writing \(k = a + (k - a)\) and \(n - a = (k-a) + (n-k)\), and rewriting the powers accordingly, the left-hand side becomes

Since \(\delta \leq 1 - \delta \) and \(\delta {\gt} 0\), we have \(\delta ^{k-a} \leq (1-\delta )^{k-a}\) by pow_le_pow_left. Applying mul_le_mul_of_nonneg_left twice (first using \((1-\delta )^{n-k} {\gt} 0\), then \(\delta ^a {\gt} 0\)), we obtain

completing the proof by ring arithmetic.

We note that every element of \(\mathbb {F}_2\) is either \(0\) or \(1\) (by decide). We define an equivalence \(e : (\operatorname {Fin} n \to \mathbb {F}_2) \simeq \operatorname {Finset}(\operatorname {Fin} n)\) by mapping \(v\) to its support \(\{ i \in \operatorname {Fin} n : v_i \neq 0\} \), with inverse sending a subset \(s\) to the indicator function \(\mathbf{1}_s\). The left inverse is verified case-by-case on \(\mathbb {F}_2\), and the right inverse by a boolean case split. Under this equivalence, the cardinality of \(e(v)\) equals \(\operatorname {wt}(v)\) by definition. Applying Mathlib’s Fin.sum_pow_mul_eq_add_pow, we get

Transporting along \(e\) via Equiv.sum_comp and a congruence argument gives the result.

Unfolding \(H_2(\delta ) = -\delta \log _2\delta - (1-\delta )\log _2(1-\delta )\), we establish that \(\delta n - k {\gt} 0\) (by linear arithmetic from \(k + 1 \leq \delta n\)) and that \(\log _2 \delta \leq \log _2(1-\delta )\) (by strict monotonicity of \(\log _2\) on \((0,\infty )\), applied at points \(\delta {\lt} 1 - \delta \) since \(\delta \leq 1/2\)). Casting \(n - k\) appropriately, the inequality then follows by nonlinear arithmetic (nlinarith), using \((\delta n - k) \cdot (\log _2(1-\delta ) - \log _2\delta ) \geq 0\).

We establish \(0 {\lt} 1 - \delta \) by linear arithmetic. We show \(k \leq n\): otherwise \(k {\gt} n\), so \(\delta n {\lt} n\), but \(k + 1 \leq \delta n {\lt} n \leq k\), a contradiction by linear arithmetic. Let \(p = \delta ^k(1-\delta )^{n-k} {\gt} 0\) (by positivity).

Step 1: \(|B_0(k)| \cdot \delta ^k(1-\delta )^{n-k} \leq 1\). We compute:

The first inequality uses bernoulli_weight_mono: for \(v \in B_0(k)\), \(\operatorname {wt}(v) \leq k\), so \(\delta ^k(1-\delta )^{n-k} \leq \delta ^{\operatorname {wt}(v)}(1-\delta )^{n-\operatorname {wt}(v)}\). The second uses Finset.sum_le_univ_sum_of_nonneg (terms are nonneg). The final equality is bernoulli_weight_sum.

Step 2: \(p^{-1} \leq 2^{H_2(\delta ) n}\). This is equivalent (by Real.logb_le_iff_le_rpow) to \(\log _2(p^{-1}) \leq H_2(\delta ) n\). Using \(\log _2(p^{-1}) = -\log _2 p\) and \(\log _2(\delta ^k (1-\delta )^{n-k}) = k\log _2\delta + (n-k)\log _2(1-\delta )\), this becomes \(-(k\log _2\delta + (n-k)\log _2(1-\delta )) \leq H_2(\delta )n\), which holds by entropy_logb_ineq.

Conclusion: From Step 1, \(|B_0(k)| \leq p^{-1}\), and from Step 2, \(p^{-1} \leq 2^{H_2(\delta )n}\), so by linear arithmetic \(|B_0(k)| \leq 2^{H_2(\delta )n}\).