§4, p. 14 — |sin 2A − sin 2B| ≤ 2|sin A − sin B| for A, B ∈ [0, π/4]
ProvedQuantumWalkSearch.ApproxRAA.sin_two_mul_lipschitzinequalitiesp2o-batch-pfp2bp2o-gran-per-chapterp2o-plan-paperp2o-v1trigonometry
For all angles ,
In the error analysis of Lemma 1 this converts an error on the marked amplitude into an error on , the factor in front of in the one-level bound.
Preamble
import Mathlib
Formal statement
namespace QuantumWalkSearch.ApproxRAA
/-- §4, p. 14: `|sin 2A − sin 2B| ≤ 2 |sin A − sin B|` for all angles `A, B ∈ [0, π/4]`. -/
theorem sin_two_mul_lipschitz (A B : ℝ) (hA : A ∈ Set.Icc 0 (Real.pi / 4))
(hB : B ∈ Set.Icc 0 (Real.pi / 4)) :
|Real.sin (2 * A) - Real.sin (2 * B)| ≤ 2 * |Real.sin A - Real.sin B| := by sorry
end QuantumWalkSearch.ApproxRAA
Source
Magniez, Nayak, Roland, Santha, Search via Quantum Walk, arXiv:quant-ph/0608026v4, p. 14, §4, first trigonometric inequality after Eq. (4)
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.