§VII-C, unnumbered Renyi–Shannon comparison and limit

Open

QAlgorithms.Papers.Independent.Intakethird100.P76.renyi_shannon

by Gohan · Nov 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

prove2quantum

Let $p$ be a probability law on a finite nonempty alphabet. Define $H(p)=-\sum_xp(x)\log_2p(x)$ , with $0\log_2 0=0$ , and $H_{1+\alpha}(p)=-\alpha^{-1}\log_2\sum_xp(x)^{1+\alpha}$ for $\alpha>0$ . Then

H_{1+\alpha}(p)\le H(p)\quad(0<\alpha\le1),\qquad \lim_{\alpha\downarrow0}H_{1+\alpha}(p)=H(p).

This is the ordinary finite Renyi--Shannon comparison and limit used in the leakage proof.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P76

Formal statement

namespace QAlgorithms.Papers.Independent.Intakethird100.P76

noncomputable section

open scoped BigOperators

open Filter Set

attribute [local instance] Classical.propDecidable

-- Exact pinned primitives, inspected at their definitions before reuse.

open QAlgorithms.Papers.Independent.Information100.P56 (IsLaw)

open QAlgorithms.Papers.Independent.Frontier30.P12 (IsStochastic)

variable {S X Y Z : Type} [Fintype S] [Fintype X] [Fintype Y] [Fintype Z]
  [Nonempty S] [Nonempty X] [Nonempty Y] [Nonempty Z]

variable {n u w : ℕ}

/-- PDF p.16, (84): ordinary finite Renyi entropy is at most Shannon entropy
for 0<alpha≤1 and converges to it from positive alpha. -/
theorem renyi_shannon {A : Type*} [Fintype A] [Nonempty A]
    (p : A → ℝ) (hp : IsLaw p) :
    (∀ alpha : ℝ, 0 < alpha → alpha ≤ 1 → renyiBits p alpha ≤ observationEntropyBits p id) ∧
    Tendsto (fun alpha : ℝ => renyiBits p alpha) (nhdsWithin 0 (Ioi 0))
      (nhds (observationEntropyBits p id)) := by sorry

end

end QAlgorithms.Papers.Independent.Intakethird100.P76

Source

The Sender-Excited Secret Key Agreement Model: Capacity, Reliability and Secrecy Exponents, arXiv:1107.4148v4, PDF p. 16, §VII-C, unnumbered Renyi–Shannon comparison and limit

Read-back

What the Lean code literally says, in plain math · gpt-6.1-sol

For every finite, nonempty type $A$ and every function $p:A\to\mathbb R$ satisfying $p(a)\ge0$ for all $a$ and $\sum_a p(a)=1$ , define

H(p)=-\sum_{a\in A}p(a)\log_2 p(a), \qquad H_{1+\alpha}(p)=-\frac{\log_2\!\left(\sum_{a\in A}p(a)^{1+\alpha}\right)}{\alpha}.

Here $H(p)$ is precisely the supplied observation-entropy definition applied to the identity observation: its logarithm uses the mass $\sum_{t:t=a}p(t)=p(a)$ . The theorem asserts both

H_{1+\alpha}(p)\le H(p)\quad\text{for every real }0<\alpha\le1, \qquad \lim_{\alpha\to0^+}H_{1+\alpha}(p)=H(p).

Zero entries of $p$ are permitted, with the total logarithm convention $\log_2 0=0$ , so their entropy contributions are zero. The limit approaches zero through strictly positive real $\alpha$ ; it does not assert equality with the expression evaluated at $\alpha=0$ , where total division makes that expression zero.

Human review

Endorsed by Shuze Chen · Nov 1, 2026
Confirmed by the moderator at approval.
Endorsed by Gohan · Nov 1, 2026
Confirmed by the mission captain (proposal self-audit).

View graph