Definition 17: Binary Entropy Function

The binary entropy function H₂ : ℝ → ℝ defined by H₂(δ) = -δ log₂(δ) - (1 - δ) log₂(1 - δ).

Main Results

• binaryEntropy: the binary entropy function
• binaryEntropy_lt_half: H₂(δ) < 1/2 for δ ∈ (0, 11/100)
• hammingBall: the Hamming ball of radius r
• hammingBallBound: |B₀(⌊δn - 1⌋)| ≤ 2^{H₂(δ) · n}

Binary Entropy Function

def binaryEntropy (δ : ℝ) : ℝ

The binary entropy function H₂ : ℝ → ℝ defined by H₂(δ) = -δ log₂(δ) - (1 - δ) log₂(1 - δ). For δ ∈ (0, 1), this gives the Shannon entropy of a Bernoulli(δ) distribution measured in bits. Outside (0, 1), the function extends by continuity (with log₂(0) = 0 in Mathlib's convention).

Equations

• binaryEntropy δ = -δ * Real.logb 2 δ - (1 - δ) * Real.logb 2 (1 - δ)

Key numerical inequality: H₂(11/100) < 1/2

The proof strategy converts the entropy inequality to a product inequality via exponentiation, then verifies the resulting natural number inequality.

theorem key_nat_ineq : 100 ^ 100 < 2 ^ 50 * 11 ^ 11 * 89 ^ 89

The key Nat inequality: 100^100 < 2^50 * 11^11 * 89^89. This is the exponential form of H₂(11/100) < 1/2.

theorem key_frac_ineq : (100 / 11) ^ 11 * (100 / 89) ^ 89 < 2 ^ 50

(100/11)^11 * (100/89)^89 < 2^50 in ℝ.

theorem binaryEntropy_at_eleven_hundredths : binaryEntropy (11 / 100) < 1 / 2

H₂(11/100) < 1/2: the binary entropy function at 11/100 is less than 1/2. The proof converts to the product form using logb, then applies key_frac_ineq.

Derivative and monotonicity of binary entropy

theorem binaryEntropy_eq_binEntropy_div (δ : ℝ) : binaryEntropy δ = Real.binEntropy δ / Real.log 2

binaryEntropy equals Mathlib's binEntropy divided by log 2.

theorem hasDerivAt_binaryEntropy {x : ℝ} (hx0 : 0 < x) (hx1 : x < 1) : HasDerivAt binaryEntropy (Real.logb 2 ((1 - x) / x)) x

theorem binaryEntropy_strictMonoOn : StrictMonoOn binaryEntropy (Set.Ioo 0 (1 / 2))

H₂ is strictly increasing on (0, 1/2): for 0 < a < b < 1/2, H₂(a) < H₂(b). This follows from H₂'(x) = logb 2 ((1-x)/x) > 0 for x < 1/2.

theorem binaryEntropy_lt_half {δ : ℝ} (hδ0 : 0 < δ) (hδ1 : δ < 11 / 100) : binaryEntropy δ < 1 / 2

H₂(δ) < 1/2 for δ ∈ (0, 11/100). Since H₂ is strictly increasing on (0, 1/2) and 11/100 < 1/2, we have H₂(δ) < H₂(11/100) < 1/2 for δ < 11/100.

Hamming Ball

def hammingBall (n : ℕ) (r : ℝ) : Finset (Fin n → 𝔽₂)

The Hamming ball of radius r centered at the origin in 𝔽₂^n: B₀(r) = {v ∈ 𝔽₂^n : wt(v) ≤ r}, where wt is the Hamming weight. This is defined as a Finset of vectors. When r < 0, the ball is empty.

Equations

• hammingBall n r = {v : Fin n → 𝔽₂ | ↑(hammingWeight v) ≤ r}

theorem mem_hammingBall {n : ℕ} {r : ℝ} {v : Fin n → 𝔽₂} : v ∈ hammingBall n r ↔ ↑(hammingWeight v) ≤ r

Membership in the Hamming ball: v ∈ B₀(r) iff wt(v) ≤ r.

theorem hammingBall_empty_of_neg {n : ℕ} {r : ℝ} (hr : r < 0) : hammingBall n r = ∅

The Hamming ball is empty when r < 0.

theorem hammingBall_nonempty {n : ℕ} {r : ℝ} (hr : 0 ≤ r) : (hammingBall n r).Nonempty

The Hamming ball is non-empty when r ≥ 0: the zero vector has weight 0.

Hamming Ball Bound helpers

theorem bernoulli_weight_mono {n : ℕ} {δ : ℝ} (hδ0 : 0 < δ) (hδ1 : δ ≤ 1 / 2) {a k : ℕ} (hak : a ≤ k) (hkn : k ≤ n) : δ ^ k * (1 - δ) ^ (n - k) ≤ δ ^ a * (1 - δ) ^ (n - a)

Helper: for 0 < δ ≤ 1/2 and a ≤ k ≤ n, we have δ^a · (1-δ)^(n-a) ≥ δ^k · (1-δ)^(n-k). This is because δ ≤ 1-δ, so replacing a by k (moving weight from 1-δ to δ exponent) decreases the product.

theorem bernoulli_weight_sum {n : ℕ} {δ : ℝ} (hδ0 : 0 < δ) (hδ1 : δ ≤ 1 / 2) : ∑ v : Fin n → 𝔽₂, δ ^ hammingWeight v * (1 - δ) ^ (n - hammingWeight v) = 1

The total Bernoulli weight over all vectors equals 1: ∑_{v : Fin n → 𝔽₂} δ^(wt v) · (1-δ)^(n - wt v) = 1. This is a consequence of the binomial theorem (δ + (1-δ))^n = 1^n = 1.

Hamming Ball Bound

theorem entropy_logb_ineq {n : ℕ} {δ : ℝ} (hδ0 : 0 < δ) (hδ1 : δ ≤ 1 / 2) {k : ℕ} (hkn : k ≤ n) (hk : ↑k + 1 ≤ δ * ↑n) : -(↑k * Real.logb 2 δ + ↑(n - k) * Real.logb 2 (1 - δ)) ≤ binaryEntropy δ * ↑n

The Hamming ball bound: for positive n and δ ∈ (0, 1/2], the number of binary vectors of length n with Hamming weight at most k satisfies |B₀(k)| ≤ 2^{H₂(δ) · n} whenever k + 1 ≤ δ · n. The proof shows |B₀(k)| · δ^k · (1-δ)^{n-k} ≤ 1 by summing Bernoulli weights, then converts to the entropy form.

theorem hammingBallBound {n : ℕ} (hn : 0 < n) {δ : ℝ} (hδ0 : 0 < δ) (hδ1 : δ ≤ 1 / 2) {k : ℕ} (hk : ↑k + 1 ≤ δ * ↑n) : ↑(hammingBall n ↑k).card ≤ 2 ^ (binaryEntropy δ * ↑n)