Lemma 8: the composed quantum correction has zero right derivative

Open

QAlgorithms.Papers.Independent.Intakethird100.P50.quantumCorrection_zero_rightDerivative

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

prove2quantum

Let $e\ge2$ be an integer, $c\ge0$ a real constant and $r>1$ . With $h$ the binary entropy in bits, define

f_1(e,\eta)=\frac\eta2\log_2(e-1)+\eta\log_2e+h(\eta/2)+(1+\eta/2)h\!\left(\frac\eta{2+\eta}\right).

The composition has right derivative zero at the noise-free point:

\left.\frac{d}{dp^+}f_1(e,cp^r)\right|_{p=0}=0.

Only a physical right neighborhood of zero is relevant. The case $c=0$ is included as the constant-zero composition. The result explains the tangency of the capacity correction to coherent information.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P50

Formal statement

noncomputable section

open scoped BigOperators Matrix ComplexConjugate ComplexOrder

open Filter

namespace QAlgorithms.Papers.Independent.Intakethird100.P50

variable {A B E F : Type}

variable [Fintype A] [DecidableEq A] [Fintype B] [DecidableEq B]

variable [Fintype E] [DecidableEq E] [Fintype F] [DecidableEq F]

open QAlgorithms.Papers.Independent.Information100.P67
  (IsIsometry receiverChannel complementaryChannel maximumCoherentInformation
    dilationPower idealJoint)

open QAlgorithms.Papers.Independent.Information100.P80 (log2)

open QAlgorithms.Papers.Independent.Information100.P69 (diamond choi)

open QAlgorithms.Papers.Independent.Support50.P07 (fullTracePrivateCapacity)

open QAlgorithms.Papers.Independent.Frontier18.P17 (clock)

/-- Lemma 8, PDF p.9: right derivative on physical p≥0, including c=0.
Choi rank e≥2 is the domain of the displayed entropy correction. -/
theorem quantumCorrection_zero_rightDerivative (e : ℕ) (he : 2 ≤ e)
    (c r : ℝ) (hc : 0 ≤ c) (hr : 1 < r) :
    HasDerivWithinAt (fun p : ℝ => quantumCorrection e (c * p ^ r)) 0 (Set.Ici 0) 0 := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P50

end

Source

Quantum and private capacities of low-noise channels, arXiv:1705.04335v3, PDF p. 9, Lemma 8: the composed quantum correction has zero right derivative

Read-back

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

For every natural number $e\ge2$ and real numbers $c\ge0$ , $r>1$ , define

q_e(\eta)= \frac{\eta}{2}\log_2(e-1)+\eta\log_2e+ h_2(\eta/2)+(1+\eta/2)h_2\!\left(\frac{\eta}{2+\eta}\right), \qquad h_2(x)=\frac{-x\ln x-(1-x)\ln(1-x)}{\ln2}.

Then the function $p\mapsto q_e(cp^r)$ has derivative zero at $p=0$ within the set $[0,\infty)$ . Here $p^r$ is real exponentiation and $\log_2x=\ln x/\ln2$ ; the logarithms and divisions use their total real definitions, including $\ln0=0$ and division by zero equal to zero. In particular, the function has value zero at $p=0$ . The statement includes $c=0$ , and concerns only the derivative within the nonnegative half-line.

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