§4, p. 14 — |sin 3A − sin 3B| ≤ 3|sin A − sin B| for A, B ∈ [0, π/4]
ProvedQuantumWalkSearch.ApproxRAA.sin_three_mul_lipschitzinequalitiesp2o-batch-pfp2bp2o-gran-per-chapterp2o-plan-paperp2o-v1trigonometry
For all angles ,
In the error analysis of Lemma 1 this shows that one level of amplitude amplification at most triples an error on the marked amplitude.
Preamble
import Mathlib
Formal statement
namespace QuantumWalkSearch.ApproxRAA
/-- §4, p. 14: `|sin 3A − sin 3B| ≤ 3 |sin A − sin B|` for all angles `A, B ∈ [0, π/4]`. -/
theorem sin_three_mul_lipschitz (A B : ℝ) (hA : A ∈ Set.Icc 0 (Real.pi / 4))
(hB : B ∈ Set.Icc 0 (Real.pi / 4)) :
|Real.sin (3 * A) - Real.sin (3 * B)| ≤ 3 * |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, second trigonometric inequality after Eq. (4)
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.