論文の概要: A Formalization of the Generalized Quantum Stein's Lemma in Lean
- arxiv url: http://arxiv.org/abs/2510.08672v1
- Date: Thu, 09 Oct 2025 17:41:13 GMT
- ステータス: 翻訳完了
- システム内更新日: 2025-10-14 00:38:47.387573
- Title: A Formalization of the Generalized Quantum Stein's Lemma in Lean
- Title（参考訳）: リーンにおける一般化量子スタインの補題の一形式化
- Authors: Alex Meiburg, Leonardo A. Lessa, Rodolfo R. Soldati,
- Abstract要約: 我々は、リーン対話的定理証明器において、ハヤシとヤマサキ(2024年)で提示された証明を定式化する。
これは、これまでコンピュータで検証された証明を持つ物理学で最も技術的に要求される定理である。
- 参考スコア（独自算出の注目度）: 0.0
- License: http://creativecommons.org/licenses/by-sa/4.0/
- Abstract: The Generalized Quantum Stein's Lemma is a theorem in quantum hypothesis testing that provides an operational meaning to the relative entropy within the context of quantum resource theories. Its original proof was found to have a gap, which led to a search for a corrected proof. We formalize the proof presented in [Hayashi and Yamasaki (2024)] in the Lean interactive theorem prover. This is the most technically demanding theorem in physics with a computer-verified proof to date, building with a variety of intermediate results from topology, analysis, and operator algebra. In the process, we rectified minor imprecisions in [HY24]'s proof that formalization forces us to confront, and refine a more precise definition of quantum resource theory. Formalizing this theorem has ensured that our Lean-QuantumInfo library, which otherwise has begun to encompass a variety of topics from quantum information, includes a robust foundation suitable for a larger collaborative program of formalizing quantum theory more broadly.
- Abstract（参考訳）: 一般化量子シュタインのレムマ(英: Generalized Quantum Stein's Lemma)は、量子仮説における定理であり、量子資源理論の文脈における相対エントロピーに対する操作的意味を提供する。
元々の証明にはギャップがあることが判明し、修正された証明の探索に繋がった。
リーン対話的定理証明器において,[早志と山崎(2024)]で提示された証明を定式化する。
これは、トポロジー、解析、作用素代数から様々な中間結果を得るコンピュータ検証された証明を持つ物理学で最も技術的に要求される定理である。
この過程で、形式化が我々に対面させ、量子資源理論のより正確な定義を洗練させるという[HY24]の証明において、小さな不正確さを是正した。
この定理の形式化は、我々のLean-QuantumInfoライブラリが量子情報から様々なトピックを包含し始めたことを保証する。
関連論文リスト
- Majorization theory for quasiprobabilities [0.49478969093606673]
行列化理論は分布の障害を比較する強力なツールである。
無限測度空間上の連続準確率分布に対する偏化の概念を導入する。
量子資源理論の文脈における結果のいくつかの応用について述べる。
論文 参考訳（メタデータ） (2025-07-30T18:00:03Z) - Some mathematical issues regarding a new approach towards quantum foundations [0.0]
最も弱い可能性定理は、量子論のヒルベルト空間形式論の基礎を与えるものである。
ベル実験や決定理論へのいくつかの応用について概説する。
論文 参考訳（メタデータ） (2024-11-20T08:14:14Z) - Generalized Quantum Stein's Lemma and Second Law of Quantum Resource Theories [47.02222405817297]
量子情報理論の基本的な問題は、量子情報処理のためのリソースの変換性を単一の関数で特徴づけるために、類似の第2法則を定式化できるかどうかである。
2008年、有望な定式化が提案され、仮説テストの量子バージョンの変種における最適性能とリソース変換可能性のリンクが提案された。
2023年、この補題の元々の証明に論理的ギャップが発見され、そのような第二法則の定式化の可能性に疑問が投げかけられた。
論文 参考訳（メタデータ） (2024-08-05T18:00:00Z) - Generalized Quantum Stein's Lemma: Redeeming Second Law of Resource
Theories [1.90365714903665]
この問題と、一般化された量子シュタインの補題の証明を完了させるために必要な条件を説明するため、さらに原稿を更新する計画である。
論文 参考訳（メタデータ） (2024-01-03T19:00:00Z) - Depth-efficient proofs of quantumness [77.34726150561087]
量子性の証明は、古典的検証器が信頼できない証明器の量子的利点を効率的に証明できる挑戦応答プロトコルの一種である。
本稿では、証明者が量子回路を一定深度でしか実行できない量子性構成の証明を2つ与える。
論文 参考訳（メタデータ） (2021-07-05T17:45:41Z) - Quantum simulation of gauge theory via orbifold lattice [47.28069960496992]
普遍量子コンピュータ上で$textU(k)$ Yang-Mills理論をシミュレートするための新しいフレームワークを提案する。
本稿では,ヤン・ミルズ理論の静的特性と実時間ダイナミクスの計算への応用について論じる。
論文 参考訳（メタデータ） (2020-11-12T18:49:11Z) - Using Quantum Metrological Bounds in Quantum Error Correction: A Simple
Proof of the Approximate Eastin-Knill Theorem [77.34726150561087]
本稿では、量子誤り訂正符号の品質と、論理ゲートの普遍的な集合を達成する能力とを結びつける、近似したイージン・クニル定理の証明を示す。
我々の導出は、一般的な量子気象プロトコルにおける量子フィッシャー情報に強力な境界を用いる。
論文 参考訳（メタデータ） (2020-04-24T17:58:10Z) - From a quantum theory to a classical one [117.44028458220427]
量子対古典的交叉を記述するための形式的アプローチを提示し議論する。
この手法は、1982年にL. Yaffeによって、大きな$N$の量子場理論に取り組むために導入された。
論文 参考訳（メタデータ） (2020-04-01T09:16:38Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。