Lemma 5, p. 17 — for k ≥ 2, µij ∈ [0, 1], vij ∈ [−1/3, 1] and sij ∈ [−1, 1]
ProvedQMCProduct.HalfApprox.lemma_5p2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1quantum-informationquantum-max-cut
Let be a -positive pseudo-density on qubits, with , and let . For the QMC edge values of Definition 12,
These intervals delimit the feasible edge values used in the rounding and monogamy analysis.
Formalization Note Distinct sites are explicit because an edge has distinct endpoints.
Preamble
import Definitions.Def_QMCProduct_HalfApprox_Basic set_option autoImplicit false
Formal statement
namespace QMCProduct.HalfApprox
/-- Lemma 5, p. 17. -/
theorem lemma_5 {n k : ℕ} (hk : 2 ≤ k) (ρt : Op n)
(hρ : IsPseudoDensity k ρt) (i j : Fin n) (hij : i ≠ j) :
(0 ≤ mu ρt i j ∧ mu ρt i j ≤ 1) ∧
(-(1 / 3 : ℝ) ≤ v ρt i j ∧ v ρt i j ≤ 1) ∧
(-1 ≤ s ρt i j ∧ s ρt i j ≤ 1) := by sorry
end QMCProduct.HalfApprox
Source
Parekh & Thompson, An Optimal Product-State Approximation for 2-Local Quantum Hamiltonians with Positive Terms, arXiv:2206.08342v2, p. 17, Lemma 5
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.