Pith. sign in

REVIEW 2 major objections 6 minor 1 cited by

Lean-QIT: Towards a Formal Infrastructure for Quantum Information Theory

T0 review · 2 major / 6 minor · reviewed 2026-07-13 · grok-4.5

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read A Lean 4 library defines quantum codes and rates first, then proves the classic Shannon theorems as equalities between those objects and entropy formulae.

desk verdict A real, reusable Lean operational layer that machine-checks Schumacher, HSW, and EA capacity (with strong converse) while keeping codes and rates independent of the analytic formulae. read the letter →

arxiv 2607.09632 v1 pith:YKA7F36C submitted 2026-07-10 quant-ph cs.AI

Chengkai Zhu , Ziao Tang , Guocheng Zhen , Yimeng Cao , Yusheng Zhao , Ranyiliu Chen , Xuanqiang Zhao , Lei Zhang
show 1 more author
Xin Wang
This is my paper · ORCID
classification quant-phcs.AI MSC 81P4568V1594A15 PACS 03.67.-a03.67.Hk
keywords quantuminformationtheoryShannonformalverificationLean4SchumachercompressionHSWtheorementanglement-assistedcapacitystrongconverse
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

This paper builds Lean-QIT, a machine-checked library for finite-dimensional quantum information theory. Its design choice is to define source codes, channel codes, error criteria, achievable rates, and capacities as independent operational objects, then prove that those rates equal the usual entropy and mutual-information formulae. With that spine the authors formalize Schumacher’s quantum source-coding theorem, the Holevo–Schumacher–Westmoreland classical capacity theorem, and the entanglement-assisted classical capacity theorem (including its strong converse). The point is that a capacity statement becomes a kernel-checked theorem relating two separately specified things, not a definition that already assumes the answer. A sympathetic reader cares because the same reusable interfaces—states, channels, hypothesis testing, one-shot quantities, and asymptotic bridges—can now support further coding theorems and give both humans and proof agents a typed place to audit assumptions and compose arguments.

What carries the argument

The operational coding spine: typed definitions of source and channel codes, finite-block performance predicates, achievable-rate sets, and capacities (via sSup/sInf), kept independent of entropy formulae and later linked by named direct, converse, and asymptotic lemmas.

What would settle it

Open the public repository snapshot and attempt to check the three named capacity endpoints (Schumacher rate equality, classicalCapacity equals regularized Holevo information, and both EA capacity and strong-converse capacity equal channel mutual information); a failed kernel check or a missing proof obligation would falsify the claim that those equalities are fully formalized.

Watch

Extended reading notes

Core claim

By separating operational definitions of codes, error criteria, and capacities from their analytic characterizations, Lean-QIT turns the central equalities of quantum Shannon theory into kernel-checked theorems that relate independently defined objects. The library realizes this architecture by fully formalizing Schumacher source coding, the HSW classical capacity, and the entanglement-assisted classical capacity with its strong converse.

Load-bearing premise

Every system is finite-dimensional; the whole library and the three proved theorems rest on finite index types and matrix representations.

Editorial extensions

If this is right

  • Capacity equalities become auditable theorems rather than definitional identities, so suppressed side conditions can be inspected.
  • The same state, channel, testing, and asymptotic APIs can be reused for quantum, private, and resource-assisted capacities without rewriting the operational layer.
  • Direct and converse proof routes stay named and composable, so later theorems can cite packing, expurgation, or Rényi bounds as modular interfaces.
  • Typed objects and explicit side conditions supply a machine-readable substrate for retrieval, proof completion, and assumption auditing by humans or agents.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • If the operational-first pattern holds for further theorems, formal QIT libraries may converge on a shared capacity API rather than theorem-specific scripts.
  • The finite-dimensional restriction suggests a natural next stress test: whether continuous-variable or infinite-dimensional coding can reuse the same rate predicates once a different state model is supplied.
  • Exposing one-shot and strong-converse layers as first-class endpoints may lower the cost of formalizing finite-blocklength refinements that currently sit outside textbook asymptotic statements.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

2 major / 6 minor

Summary. The manuscript introduces Lean-QIT, a Lean 4 library for finite-dimensional quantum information theory organized into object, analytic, and operational layers. Its central design choice is to define codes, error criteria, achievable rates, and capacities independently of the entropic formulae that later characterize them, so that capacity equalities become theorems relating separately specified objects. Using this infrastructure, the authors formalize three classical quantum Shannon theory endpoints: Schumacher source coding (R_Sch(ρ)=S(ρ)), the HSW classical capacity (C(N)=lim (1/n)χ(N^⊗n)), and the entanglement-assisted classical capacity together with its strong converse (C_EA(N)=C̃_EA(N)=I(N)). The paper documents typed state/channel APIs, subsystem and measurement calculus, state geometry, mutual information and sandwiched Rényi data processing, hypothesis-testing interfaces, smooth-entropy/AEP bridges, and the direct/converse/limit assembly for each coding theorem, with public endpoint wrappers collected in Appendix A.

Significance. If the kernel-checked claims hold as stated, this is a substantial contribution to formal quantum information theory. Prior Lean developments have emphasized operator/entropy foundations or specialized tasks; Lean-QIT targets the underdeveloped operational coding layer that connects finite-block protocols to asymptotic capacities. Shipping machine-checked Schumacher, HSW, and EA (with strong converse) theorems, with operational rates defined before analytic characterizations and with named reusable direct/converse components, is a genuine advance. The finite-dimensional restriction is stated up front and does not undermine the three equalities inside that regime. The library’s size metrics, public repository, and explicit separation of operational predicates from Holevo/mutual-information formulae make the work a useful substrate for both human formalization and AI-assisted proof search.

major comments (2)
  1. The central claim is that the three capacity equalities are proved public endpoints checked by the Lean kernel (§2 terminology; Theorems 4.2, 4.7, 4.11 and the corresponding Lean declarations in §§4.1–4.3). The manuscript cites a “July 9, 2026 snapshot” and github.com/QuAIR/Lean-QIT but does not pin a commit hash, release tag, or lake lockfile, nor does it state whether the critical path for these three endpoints is free of sorry and of non-Mathlib axioms. For a formalization paper whose load-bearing claim is kernel-checked completeness, a short reproducibility subsection (pinned commit + axiom/sorry inventory for the Schumacher, HSW, and EA public endpoints) is needed so that referees and readers can verify the claim as stated.
  2. §4.2–4.3 present packing/expurgation, Hayashi–Nagaoka, position-based coding, sequential decoding/quantum union bound, Petz and sandwiched Rényi limits, and cb-norm bridges as named witnesses consumed by the capacity squeezes. The paper is careful that operational definitions do not bake in analytic formulae, but it is not fully explicit which of these intermediate analytic ingredients are fully formalized in Lean-QIT versus imported as trusted lemmas or reduced to Mathlib. A brief table or paragraph mapping each named witness in Figure 3 to “fully proved / reduced to Mathlib / remaining obligation” would make the formalization depth of the HSW and EA spines auditable without changing the architectural claim.
minor comments (6)
  1. Figure 1 caption: typo “libaray” → “library”.
  2. Abstract and title use both “LeanQIT” and “Lean-QIT”; standardize on one spelling throughout (including the GitHub URL branding).
  3. Notation section defines R̄ = R ∪ {−∞,+∞} but later code listings use EReal; a one-line cross-reference would help readers map Lean types to the mathematical extended reals.
  4. §3.4’s discussion of concurrent Lean-Quantum is useful; a short sentence clarifying non-overlap (basis-independent operator layer vs operational coding spine) would reduce ambiguity for readers who only skim the introduction.
  5. Appendix A wrappers are thin by design; consider adding the fully-qualified Lean declaration names (module paths) next to each wrapper so that documentation and the paper stay synchronized as the library evolves.
  6. In Definition 4.1 / Eq. (21), the joint purification error e_jp is used but only briefly glossed; a one-line definition matching the SchumacherCompressionCode interface would improve self-containment.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity: operational rates are defined independently of entropic formulae, and capacity equalities are proved as kernel-checked theorems relating separately specified objects.

full rationale

Lean-QIT is a formalization infrastructure paper, not a predictive or fitted-model paper. Operational objects (IsAchievableSchumacherRate / schumacherCompressionRate; IsAchievableClassicalRate / classicalCapacity; IsAchievableEntanglementAssistedClassicalRate / entanglementAssistedClassicalCapacity and the strong-converse dual) are defined by quantifiers over codes, error criteria, and asymptotic rate predicates before any Holevo, mutual-information, or Rényi formula appears. The analytic characterizations (von Neumann entropy, regularized Holevo information, channel mutual information) are introduced as separate interfaces; the three capacity equalities are then assembled from named direct, converse, and limit lemmas (typical-subspace coding + AFW continuity; packing/expurgation + Holevo converse; Petz one-shot lower bounds + sandwiched-Rényi meta-converse). No free parameters are fitted to data, no uniqueness theorem is imported from overlapping authors to forbid alternatives, and self-citations point to the library repository or concurrent independent Lean work rather than load-bearing unverified premises. The finite-dimensional restriction is an explicit scope assumption, not a circular reduction. The derivation chain is therefore self-contained: known QST theorems are restated with independent operational and analytic sides and machine-checked as equalities, which is the opposite of definitional circularity.

Assumptions & free parameters 0 free parameters · 3 assumptions · 1 invented entities

The paper formalizes known finite-dimensional theorems; it introduces no new physical postulates or fitted constants. All load-bearing background is either standard mathematics (finite types, positive-semidefinite operators, CPTP maps, order-theoretic sInf/sSup) or textbook QIT (von Neumann entropy, relative entropy, Rényi divergences, AFW continuity, fully quantum AEP). The sole domain restriction is finite dimensionality, stated explicitly.

assumptions (3)
  • domain assumption All Hilbert spaces are finite-dimensional (Fintype index types).
    Stated in Notation and conventions; every State/Channel declaration carries the assumption. Required for the matrix and tensor-power interfaces used throughout.
  • standard math Standard definitions of CPTP maps, von Neumann entropy, quantum relative entropy, sandwiched and Petz–Rényi divergences, purified distance, and hypothesis-testing relative entropy.
    Imported from the QIT literature (Wilde, Tomamichel, etc.) and realized as Lean definitions; no novel axiomatization.
  • standard math Lean/Mathlib foundations for real analysis, matrices, and order theory (sInf/sSup, extended reals).
    Trusted computing base of the formalization; not re-proved in the paper.
invented entities (1)
  • Lean-QIT operational coding spine (SchumacherCompressionCode, HSWClassicalCode, EntanglementAssistedClassicalCode, IsAchievable*Rate predicates, capacity as sSup/sInf) independent evidence
    purpose: Provide typed, formula-independent definitions of codes, errors, rates and capacities so that capacity equalities become theorems rather than definitions.
    The central design contribution; independent evidence is the public Lean repository that type-checks the endpoints.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Lean-QIT: Towards a Formal Infrastructure for Quantum Information Theory." pith.science (2026). https://pith.science/paper/YKA7F36C

@misc{pith2026260709632,
  author       = {Pith},
  title        = {Pith review of: Lean-QIT: Towards a Formal Infrastructure for Quantum Information Theory},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/YKA7F36C}},
  note         = {Machine review of arXiv:2607.09632}
}
read the original abstract

Quantum information theory (QIT) characterizes the capabilities and fundamental limits of quantum information processing, underpinning quantum communication, computation, and error correction. Formalizing its coding theorems requires connecting finite-block protocols, analytic inequalities, and asymptotic limits within a unified machine-checked framework. Existing developments, however, lack a reusable operational layer that defines codes, error criteria, achievable rates, and capacities independently of their information-theoretic characterizations. In this work, we present LeanQIT, a Lean 4 library for finite-dimensional QIT. It provides composable, kernel-checked interfaces for quantum states and channels, source and channel codes, finite-block performance criteria, hypothesis testing, one-shot quantities, and asymptotic rate constructions. Using this infrastructure, we formalize Schumacher's quantum source-coding theorem, the Holevo--Schumacher--Westmoreland classical-capacity theorem, and the entanglement-assisted classical-capacity theorem together with its strong converse. By separating operational definitions from analytic characterizations and exposing reusable achievability, converse, and asymptotic components, Lean-QIT provides a machine-readable foundation for formal QIT and a compositional knowledge substrate for emerging AI-assisted formalization, automated proof search, and agentic reasoning in quantum information and computation.

Figures

Figures reproduced from arXiv: 2607.09632 by the authors.

Figure 1
Figure 1. Global architecture of Lean-QIT. The libaray is built on the trusted Lean/Mathlib foundation, finite-dimensional QIT substrate, shared proof interfaces, operational QST coding surfaces, and broader QIT modules. The QST spine consumes the shared interfaces to state and prove Schumacher source coding, HSW classical communication, and entanglement-assisted classical communication endpoints. 3 Finite-Dimensional QIT Bui… view at source ↗
Figure 2
Figure 2. Layered proof stack for the reusable finite-dimensional QIT building blocks in [PITH_FULL_IMAGE:figures/full_fig_p005_2.png] view at source ↗
Figure 3
Figure 3. Architecture of the coding spine developed in Section [PITH_FULL_IMAGE:figures/full_fig_p013_3.png] view at source ↗

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

  1. Analytic Qubit Separation between POVMs and Projective Measurements

    quant-ph 2026-08 conditional novelty 8.0 of 10

    First fully analytic Bell-functional separation between qubit POVMs and all qubit-projective strategies over arbitrary two-qubit states, plus an exact dimension-unrestricted optimality certificate.

Reference graph

Works this paper leans on

48 extracted references · cited by 1 Pith paper

  1. [1]

    Quantum coding.Physical Review A, 51(4):2738–2747, 1995

    Benjamin Schumacher. Quantum coding.Physical Review A, 51(4):2738–2747, 1995

    1995

  2. [2]

    Alexander S. Holevo. The capacity of the quantum channel with general signal states.IEEE Transactions on Information Theory, 44(1):269–273, 1998

    1998

  3. [3]

    Westmoreland

    Benjamin Schumacher and Michael D. Westmoreland. Sending classical information via noisy quantum channels.Physical Review A, 56(1):131–138, 1997

    1997

  4. [4]

    Capacity of the noisy quantum channel.Physical Review A, 55(3):1613–1622, 1997

    Seth Lloyd. Capacity of the noisy quantum channel.Physical Review A, 55(3):1613–1622, 1997

    1997

  5. [5]

    The private classical capacity and quantum capacity of a quantum channel.IEEE Transactions on Information Theory, 51(1):44–55, 2005

    Igor Devetak. The private classical capacity and quantum capacity of a quantum channel.IEEE Transactions on Information Theory, 51(1):44–55, 2005

    2005

  6. [6]

    Bennett, Gilles Brassard, Sandu Popescu, Benjamin Schumacher, John A

    Charles H. Bennett, Gilles Brassard, Sandu Popescu, Benjamin Schumacher, John A. Smolin, and William K. Wootters. Purification of noisy entanglement and faithful teleportation via noisy channels. Physical Review Letters, 76(5):722–725, 1996

    1996

  7. [7]

    Bennett, David P

    Charles H. Bennett, David P. DiVincenzo, John A. Smolin, and William K. Wootters. Mixed-state entanglement and quantum error correction.Physical Review A, 54(5):3824–3851, 1996

    1996

  8. [8]

    Bennett, Peter W

    Charles H. Bennett, Peter W. Shor, John A. Smolin, and Ashish V. Thapliyal. Entanglement-assisted classical capacity of noisy quantum channels.Physical Review Letters, 83(15):3081–3084, 1999

    1999

Show all 48 references
  1. [9]

    Bennett, Peter W

    Charles H. Bennett, Peter W. Shor, John A. Smolin, and Ashish V. Thapliyal. Entanglement-assisted capacity of a quantum channel and the reverse Shannon theorem.IEEE Transactions on Information Theory, 48(10):2637–2655, 2002

    2002

  2. [10]

    Bennett, Igor Devetak, Aram W

    Charles H. Bennett, Igor Devetak, Aram W. Harrow, Peter W. Shor, and Andreas Winter. The quantum reverse Shannon theorem and resource tradeoffs for simulating quantum channels.IEEE Transactions on Information Theory, 60(5):2926–2959, 2014

    2014

  3. [11]

    The quantum reverse Shannon theorem based on one-shot information theory.Communications in Mathematical Physics, 306(3):579–615, 2011

    Mario Berta, Matthias Christandl, and Renato Renner. The quantum reverse Shannon theorem based on one-shot information theory.Communications in Mathematical Physics, 306(3):579–615, 2011

    2011

  4. [12]

    PhD thesis, ETH Zurich, 2005

    Renato Renner.Security of Quantum Key Distribution. PhD thesis, ETH Zurich, 2005

    2005

  5. [13]

    Springer, 2015

    Marco Tomamichel.Quantum Information Processing with Finite Resources: Mathematical Foundations, volume 5 ofSpringerBriefs in Mathematical Physics. Springer, 2015

    2015

  6. [14]

    The mother of all protocols: Restructuring quantum information’s family tree.Proceedings of the Royal Society A, 465(2108):2537–2563, 2009

    Anura Abeyesinghe, Igor Devetak, Patrick Hayden, and Andreas Winter. The mother of all protocols: Restructuring quantum information’s family tree.Proceedings of the Royal Society A, 465(2108):2537–2563, 2009

    2009

  7. [15]

    Wilde.Quantum Information Theory

    Mark M. Wilde.Quantum Information Theory. Cambridge University Press, 2nd edition, 2017

    2017

  8. [16]

    Sumeet Khatri, Ludovico Lami, and Mark M. Wilde. Principles of quantum communication theory: A modern approach, 2025. Book in progress, latest version dated November 5, 2025. Available at https://www.markwilde.com/PQCT-khatri-lami-wilde.pdf

    2025

  9. [17]

    Mario Berta, Fernando G. S. L. Brandão, Gilad Gour, Ludovico Lami, Martin B. Plenio, Bartosz Regula, and Marco Tomamichel. On a gap in the proof of the generalised quantum Stein’s lemma and its consequences for the reversibility of quantum resources.Quantum, 7:1103, 2023

    2023

  10. [18]

    Formal mathematical reasoning: A new frontier in AI, 2024

    Kaiyu Yang, Gabriel Poesia, Jingxuan He, Wenda Li, Kristin Lauter, Swarat Chaudhuri, and Dawn Song. Formal mathematical reasoning: A new frontier in AI, 2024

    2024

  11. [19]

    AXLE: A cloud infrastructure for Lean 4 theorem proving utilities, 2026

    Jimmy Xin, Alex Schneidman, Chris Cummins, Karun Ram, Srihari Ganesh, and Jannis Limperg. AXLE: A cloud infrastructure for Lean 4 theorem proving utilities, 2026

    2026

  12. [20]

    The Lean theorem prover

    Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer. The Lean theorem prover. InAutomated Deduction — CADE-25, pages 378–388. Springer, 2015

    2015

  13. [21]

    The Lean 4 theorem prover and programming language

    Leonardo de Moura and Sebastian Ullrich. The Lean 4 theorem prover and programming language. In Automated Deduction — CADE 28, pages 625–635. Springer, 2021. 27 Lean-QIT QudeLeap Research

    2021

  14. [22]

    The Lean mathematical library

    The mathlib Community. The Lean mathematical library. InProceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2020), pages 367–381. ACM, 2020

    2020

  15. [23]

    CSLib: The Lean computer science library, 2026

    Clark Barrett, Swarat Chaudhuri, Fabrizio Montesi, Jim Grundy, Pushmeet Kohli, Leonardo de Moura, Alexandre Rademaker, and Sorrachai Yingchareonthawornchai. CSLib: The Lean computer science library, 2026

    2026

  16. [24]

    Physlib: The Lean physics library, 2024

    The Physlib community. Physlib: The Lean physics library, 2024. Repository snapshot accessed 2026-07-03

    2024

  17. [25]

    Formalization of physics index notation in Lean 4, 2024

    Joseph Tooby-Smith. Formalization of physics index notation in Lean 4, 2024

    2024

  18. [26]

    Certified quantum computation in Isabelle/HOL.Journal of Automated Reasoning, 65(5):691–709, 2020

    Anthony Bordg, Hanna Lachnitt, and Yijun He. Certified quantum computation in Isabelle/HOL.Journal of Automated Reasoning, 65(5):691–709, 2020

    2020

  19. [27]

    A formally certified end-to-end implementation of Shor’s factorization algorithm.Proceedings of the National Academy of Sciences, 120(21):e2218775120, 2023

    Yuxiang Peng, Kesha Hietala, Runzhou Tao, Liyi Li, Robert Rand, Michael Hicks, and Xiaodi Wu. A formally certified end-to-end implementation of Shor’s factorization algorithm.Proceedings of the National Academy of Sciences, 120(21):e2218775120, 2023

    2023

  20. [28]

    Lessa, and Rodolfo R

    Alex Meiburg, Leonardo A. Lessa, and Rodolfo R. Soldati. A formalization of the generalized quantum Stein’s lemma in Lean, 2025

    2025

  21. [29]

    End-to-end formalization of quantum error correction, 2026

    Mattias Ehatamm, Yi Lee, Xiaodi Wu, and Runzhou Tao. End-to-end formalization of quantum error correction, 2026

    2026

  22. [30]

    A machine-verified proof of a quantum- optimization conjecture, 2026

    Uri Kol, Maor Ben-Shahar, Kfir Sulimany, and Dirk Englund. A machine-verified proof of a quantum- optimization conjecture, 2026

    2026

  23. [31]

    Lean repositories for quantum mechanics, quantum information, and quantum computing,

    Alex Meiburg. Lean repositories for quantum mechanics, quantum information, and quantum computing,

  24. [32]

    Lean-QIT.https://github.com/QuAIR/Lean-QIT, 2026

    Chengkai Zhu, Ziao Tang, Guocheng Zhen, Yimeng Cao, Ranyiliu Chen, Xuanqiang Zhao, Lei Zhang, and Xin Wang. Lean-QIT.https://github.com/QuAIR/Lean-QIT, 2026

    2026

  25. [33]

    Lean-Quantum: Toward AI-assisted formalization of quantum information, 2026

    Kazumi Kasaura, Kei Tsukamoto, Kento Mori, Risa Mizuno, Takahiro Namatame, Yuta Oriike, Masaya Taniguchi, Sho Sonoda, and Hayata Yamasaki. Lean-Quantum: Toward AI-assisted formalization of quantum information, 2026

    2026

  26. [34]

    On quantum rényi entropies: A new generalization and some properties.Journal of Mathematical Physics, 54(12), December 2013

    Martin Müller-Lennert, Frédéric Dupuis, Oleg Szehr, Serge Fehr, and Marco Tomamichel. On quantum rényi entropies: A new generalization and some properties.Journal of Mathematical Physics, 54(12), December 2013

    2013

  27. [35]

    Wilde, Andreas Winter, and Dong Yang

    Mark M. Wilde, Andreas Winter, and Dong Yang. Strong converse for the classical capacity of entanglement-breaking and hadamard channels via a sandwiched rényi relative entropy.Communi- cations in Mathematical Physics, 331(2):593–622, 2014

    2014

  28. [36]

    Frank and Elliott H

    Rupert L. Frank and Elliott H. Lieb. Monotonicity of a relative Rényi entropy.Journal of Mathematical Physics, 54(12):122201, 2013

    2013

  29. [37]

    Sandwiched Rényi divergence satisfies data processing inequality.Journal of Mathematical Physics, 54(12):122202, 2013

    Salman Beigi. Sandwiched Rényi divergence satisfies data processing inequality.Journal of Mathematical Physics, 54(12):122202, 2013

    2013

  30. [38]

    A fully quantum asymptotic equipartition property.IEEE Transactions on Information Theory, 55(12):5840–5847, 2009

    Marco Tomamichel, Roger Colbeck, and Renato Renner. A fully quantum asymptotic equipartition property.IEEE Transactions on Information Theory, 55(12):5840–5847, 2009

    2009

  31. [39]

    Continuity of quantum conditional information.Journal of Physics A: Mathematical and General, 37(5):L55–L57, 2004

    Robert Alicki and Mark Fannes. Continuity of quantum conditional information.Journal of Physics A: Mathematical and General, 37(5):L55–L57, 2004

    2004

  32. [40]

    Andreas Winter. Tight uniform continuity bounds for quantum entropies: conditional entropy, relative entropy distance and energy constraints.Communications in Mathematical Physics, 347(1):291–313, 2016

    2016

  33. [41]

    Duality between smooth min- and max-entropies

    Marco Tomamichel, Roger Colbeck, and Renato Renner. Duality between smooth min- and max-entropies. IEEE Transactions on Information Theory, 56(9):4674–4681, 2010

    2010

  34. [42]

    General formulas for capacity of classical-quantum channels

    Masahito Hayashi and Hiroshi Nagaoka. General formulas for capacity of classical-quantum channels. IEEE Transactions on Information Theory, 49(7):1753–1768, 2003. 28 Lean-QIT QudeLeap Research

    2003

  35. [43]

    One-shot entanglement-assisted quantum and classical communica- tion.IEEE Transactions on Information Theory, 59:1929–1939, 2013

    Nilanjana Datta and Min-Hsiu Hsieh. One-shot entanglement-assisted quantum and classical communica- tion.IEEE Transactions on Information Theory, 59:1929–1939, 2013

    1929

  36. [44]

    Anurag Anshu, Rahul Jain, and Naqueeb A. Warsi. Building blocks for communication over noisy quantum networks.IEEE Transactions on Information Theory, 65:1287–1306, 2019

    2019

  37. [45]

    Haoyu Qi, Qing-Le Wang, and Mark M. Wilde. Applications of position-based coding to classical communication over quantum channels.Journal of Physics A: Mathematical and Theoretical, 51:444002, 2018

    2018

  38. [46]

    Samad Khabbazi Oskouei, Stefano Mancini, and Mark M. Wilde. Union bound for quantum information processing.Proceedings of the Royal Society A, 475:20180612, 2019

    2019

  39. [47]

    Finite blocklength converse bounds for quantum channels

    William Matthews and Stephanie Wehner. Finite blocklength converse bounds for quantum channels. IEEE Transactions on Information Theory, 60:7317–7329, 2014

    2014

  40. [48]

    Gupta and Mark M

    Manish K. Gupta and Mark M. Wilde. Multiplicativity of completely boundedp-norms implies a strong converse for entanglement-assisted capacity.Communications in Mathematical Physics, 334:867–887, 2015. 29

    2015

Pith tools

Reviewed July 13, 2026 · model on record in the stance chip above.