Fano's inequality

TheoremFano's inequality, general form#✓fully proved

Let \(\alpha\) and \(\beta\) be finite nonempty sets with \(|\alpha| \ge 2\), let \(p : \alpha \times \beta \to \mathbb{R}\) satisfy \(p(a, b) > 0\) for all \(a, b\) and \(\sum_{a, b} p(a, b) = 1\), and let \(g : \beta \to \alpha\). Put \(p_Y(b) = \sum_a p(a, b)\), let \(P_e = \sum_b \sum_{a \ne g(b)} p(a, b)\) be the probability that \(g\) guesses wrong, and let \(H(X \mid Y) = -\sum_{a, b} p(a, b) \log (p(a, b) / p_Y(b))\), where \(\log\) is the natural logarithm. Then

\[H(X \mid Y) \le -P_e \log P_e - (1 - P_e) \log (1 - P_e) + P_e \log (|\alpha| - 1).\]

This version does not assume decidable equality on \(\beta\).

theorem fano_inequality_general
    {α β : Type*} [Fintype α] [Fintype β] [Nonempty α] [Nonempty β]
    [DecidableEq α]
    (p : α → β → ℝ)
    (hp_pos : ∀ a b, 0 < p a b)
    (hp_sum : ∑ a : α, ∑ b : β, p a b = 1)
    (g : β → α)
    (hcard : 2 ≤ Fintype.card α) :
    let pY : β → ℝ := fun y => ∑ a : α, p a y
    let Pe : ℝ := ∑ b : β, ∑ a : α, if g b ≠ a then p a b else 0
    let HXY : ℝ := -(∑ a : α, ∑ b : β, p a b * Real.log (p a b / pY b))
    HXY ≤ -Pe * Real.log Pe - (1 - Pe) * Real.log (1 - Pe)
      + Pe * Real.log ((Fintype.card α - 1 : ℕ) : ℝ)

Uses 1 · Used by 1

Proof usesLog-sum inequality

Used byFano's inequality

TheoremFano's inequality#✓fully proved

Let \(\alpha\) and \(\beta\) be finite nonempty sets with \(|\alpha| \ge 2\), let \(p : \alpha \times \beta \to \mathbb{R}\) satisfy \(p(a, b) > 0\) for all \(a, b\) and \(\sum_{a, b} p(a, b) = 1\), and let \(g : \beta \to \alpha\) be an estimator. Put \(p_Y(b) = \sum_a p(a, b)\), let \(P_e = \sum_b \sum_{a \ne g(b)} p(a, b)\) be the probability that \(g\) guesses wrong, and let \(H(X \mid Y) = -\sum_{a, b} p(a, b) \log (p(a, b) / p_Y(b))\), where \(\log\) is the natural logarithm. Then

\[H(X \mid Y) \le -P_e \log P_e - (1 - P_e) \log (1 - P_e) + P_e \log (|\alpha| - 1).\]

theorem fano_inequality
    {α β : Type*} [Fintype α] [Fintype β] [Nonempty α] [Nonempty β]
    [DecidableEq α] [DecidableEq β]
    (p : α → β → ℝ)
    (hp_pos : ∀ a b, 0 < p a b)
    (hp_sum : ∑ a : α, ∑ b : β, p a b = 1)
    (g : β → α)
    (hcard : 2 ≤ Fintype.card α) :
    let pY : β → ℝ := fun y => ∑ a : α, p a y
    let Pe : ℝ := ∑ b : β, ∑ a : α, if g b ≠ a then p a b else 0
    let HXY : ℝ := -(∑ a : α, ∑ b : β, p a b * Real.log (p a b / pY b))
    HXY ≤ -Pe * Real.log Pe - (1 - Pe) * Real.log (1 - Pe)
      + Pe * Real.log ((Fintype.card α - 1 : ℕ) : ℝ)

Sources

• R. M. Fano, Transmission of Information, MIT Press (1961). It follows from fano_inequality_general; the unused [DecidableEq β] keeps the source's shape.

Uses 1

Proof usesFano's inequality, general form

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.