Source-pinned research
Search theorem names, mathematical ideas, modules, topics, projects, and role-labelled researchers. Open a result for its complete indexed Lean declaration and source record.
This index contains 160 research declarations. Search 10,000 more complete Mathlib declarations.
160 results
Clear filterspinching_bound
Plain-language statement
Lemma 3.10 of Hayashi's book "Quantum Information Theory - Mathematical Foundations". Also, Lemma 5 in https://arxiv.org/pdf/quant-ph/0107004. -- Used in (S60)
Source project: quantumInfo
Person-level attribution pending.
pinching_kraus_ker_of_ne_zero
Project documentation
Lemma 3.10 of Hayashi's book "Quantum Information Theory - Mathematical Foundations". Also, Lemma 5 in https://arxiv.org/pdf/quant-ph/0107004. -- Used in (S60) -/ theorem pinching_bound (ρ σ : MState d) : ρ.M ≤ (↑(Fintype.card (spectrum ℝ σ.m)) : ℝ) • (pinching_map σ ρ).M := by rw [pinchingMap_apply_M] suffices ρ.M ≤ (Fintype.card (spectrum ℝ σ.m) : ℝ) •...
Source project: quantumInfo
Person-level attribution pending.
pinching_pythagoras
Plain-language statement
Exercise 2.8 of Hayashi's book "A group theoretic approach to Quantum Information".
Source project: quantumInfo
Person-level attribution pending.
PosDef_traceRight
Plain-language statement
The partial trace (left) of a positive definite matrix is positive definite.
Source project: quantumInfo
Person-level attribution pending.
ProbabilityTheory.iIndepFun.sum_elim
Plain-language statement
Two internally independent families remain jointly independent after they are combined over a disjoint union, provided the two family-valued random variables are independent of one another.
Source project: Polynomial Freiman-Ruzsa project
Person-level attribution pending.
ProbDistribution.constant_of_exists_one
Plain-language statement
If a distribution has an element with probability 1, the distribution has a constant.
Source project: quantumInfo
Person-level attribution pending.