Research proof index

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)

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) : ℝ) •...

Exercise 2.8 of Hayashi's book "A group theoretic approach to Quantum Information".

Everything is integrable over PMFs with finite support

Pushforward of PMF.uniformOfFintype α under a map f : α → β whose fibers over the image all have the same cardinality k > 0 is the uniform distribution on the image of f. Useful when f is an affine-linear surjection: every fiber is a translate of the kernel and hence has constant cardinality. The proximity-gap proofs use this to bridge the coeff...

Consecutive prime gaps are small relative to the primes themselves. If $p_n$ is the $n$th prime, then $p_{n+1}-p_n=o(p_n).$ Formally, there is a sequence $c_n\to0$ such that $p_{n+1}-p_n=c_np_n$ for every $n$.