Skip to content

Commit 53119af

Browse files
gpafentakisgpafentakis
committed
Added DJ and Grover's search proofs
1 parent 20dae29 commit 53119af

3 files changed

Lines changed: 403 additions & 0 deletions

File tree

‎QCLib/Circuit/Algorithms/DeutschJozsa.lean‎

Lines changed: 61 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,61 @@
1+
/-
2+
Copyright (c) 2026 David Gross, Davood Tehrani. All rights reserved.
3+
Released under MIT license as described in the file LICENSE.
4+
Authors: David Gross, Davood Tehrani, George Afentakis
5+
-/
6+
import QCLib.Circuit.Gate.Qubit
7+
import QCLib.Circuit.Hadamard
8+
9+
open Matrix
10+
11+
variable {n}
12+
variable (f : Register n → Fin 2)
13+
14+
def oracle : 𝐔[Register n] :=
15+
⟨diagonal (fun k ↦ (-1 : ℂ)^((f k) : ℕ)), by simp [Unitary.mem_iff, ← pow_add]⟩
16+
17+
noncomputable def DJ := HH n * oracle f * (HH n)⁻¹
18+
19+
theorem oracle_const (h : ∃ c, f = Function.const _ c) :
20+
oracle f = 1 ∨ oracle f = -1 := by
21+
obtain ⟨c, rfl⟩ := h
22+
fin_cases c <;> simp [UnitaryGroup.ext_iff,oracle, diagonal_apply, one_apply, Submonoid.smul_def]
23+
24+
theorem if_const (h : ∃ c, f = Function.const _ c) :
25+
‖(DJ f • δ[(0 : Register n)]) (0 : Register n)‖ = 1 := by
26+
rcases oracle_const f h with h | h <;> simp [DJ, h, Submonoid.smul_def, basisVector_def]
27+
28+
open Classical in
29+
def Function.IsBalanced {ι : Type} [Fintype ι] (f : ι → Fin 2) : Prop :=
30+
(Finset.univ.filter (fun i ↦ f i = 0)).card = (Finset.univ.filter (fun i ↦ f i = 1)).card
31+
32+
-- Maybe move this in QCLib.LinearAlgebra.UnitaryGroup.Basic? or .Action or .Lemmas?
33+
-- Or do we have it already?
34+
theorem Unitary.IsHermitian_inv {α : Type*} {m : Type*} [CommRing α] [StarRing α] [Fintype m]
35+
[DecidableEq m] {A : unitaryGroup m α} (h : Matrix.IsHermitian A.val) : A⁻¹ = A := by
36+
exact UnitaryGroup.ext A⁻¹ A fun i ↦ congrFun (congrFun h i)
37+
38+
lemma neg_one_pow_fin2 (a : Fin 2) : (-1 : ℂ) ^ (a : ℕ) = if a = 0 then 1 else -1 := by
39+
fin_cases a <;> simp
40+
41+
lemma balanced_sum_zero (h : Function.IsBalanced f) : ∑ k, (-1 : ℂ) ^ ↑((f k) : ℕ) = 0 := by
42+
have h2 : ∀ x, ¬ f x = 0 ↔ f x = 1 := fun x => by fin_cases (f x) <;> grind
43+
simp only [neg_one_pow_fin2,Finset.sum_ite,Finset.sum_const]
44+
rw [Finset.filter_inj'.mpr (fun a _ ↦ h2 a), h]
45+
simp
46+
47+
theorem if_balanced (h : Function.IsBalanced f) : (DJ f • δ[(0 : Register n)]) 0 = (0 : ℂ) := by
48+
simp_rw [DJ, Unitary.IsHermitian_inv (HH_isHermitian n), ← smul_eq_mul, smul_assoc, HH_apply]
49+
rw [HadamardBasisVector, ← smul_assoc, smul_comm, smul_assoc, Finset.smul_sum]
50+
simp [oracle, basisVector_def, Finset.smul_sum, Matrix.unitaryGroup.smul_vec_def,
51+
HH_first_row_eq, ← Finset.mul_sum, balanced_sum_zero f h]
52+
53+
theorem deutsch_jozsa (f : Register n → Fin 2)
54+
(h : (∃ c, f = Function.const _ c) ∨ Function.IsBalanced f) :
55+
Function.IsBalanced f ↔ ‖(DJ f • δ[(0 : Register n)]) 0‖ = 0 := by
56+
grind [if_balanced f, norm_zero, if_const f]
57+
58+
theorem deutsch_jozsa' (f : Register n → Fin 2)
59+
(h : (∃ c, f = Function.const _ c) ∨ Function.IsBalanced f) :
60+
(∃ c, f = Function.const _ c) ↔ ‖(DJ f • δ[(0 : Register n)]) 0‖ = 1 := by
61+
grind [if_balanced f, norm_zero, if_const f]

‎QCLib/Circuit/Algorithms/GroverSearch.lean‎

Lines changed: 334 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,334 @@
1+
/-
2+
Copyright (c) 2026 David Gross, Davood Tehrani. All rights reserved.
3+
Released under MIT license as described in the file LICENSE.
4+
Authors: David Gross, Davood Tehrani, George Afentakis
5+
-/
6+
7+
import QCLib.Circuit.Gate.Qubit
8+
import QCLib.Circuit.Hadamard
9+
import Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
10+
import Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
11+
12+
open Matrix Qubit EuclideanSpace Module Real Orientation
13+
14+
15+
attribute [instance 10000] instModuleForall
16+
17+
18+
variable {n}
19+
variable (f : Register n → Fin 2)
20+
21+
-- Oracle is identical to DJ
22+
def oracle : 𝐔[Register n] :=
23+
⟨diagonal (fun k ↦ (-1 : ℂ)^((f k) : ℕ)), by simp [Unitary.mem_iff, ← pow_add]⟩
24+
25+
26+
/-- The uniform superposition over all basis states orthogonal to `ω`. -/
27+
noncomputable def sPerp (ω : Register n) : Register n → ℂ :=
28+
(Real.sqrt (2^n - 1) : ℂ)⁻¹ • ∑ k ∈ Finset.univ.filter (· ≠ ω), δ[k]
29+
30+
/-- The reflection around the zero state, which is `2|0><0| - I` -/
31+
def zeroRefl (n : ℕ) : 𝐔[Register n] :=
32+
⟨diagonal (fun k : Register n ↦ (-1 : ℂ) ^ (if k = 0 then 0 else 1 : ℕ)),
33+
by constructor <;> simp [ext,diagonal_apply] <;> aesop⟩
34+
35+
/-- The Grover diffusion operator `H (2|0⟩⟨0| - I) H`. -/
36+
noncomputable def diffusion (n : ℕ) : 𝐔[Register n] := (HH n) * (zeroRefl n) * (HH n)
37+
38+
noncomputable def groverIterate : 𝐔[Register n] := diffusion n * oracle f
39+
40+
/-- The state after `r` Grover iterates applied to the initial uniform superposition. -/
41+
noncomputable def grover (r : ℕ) : (Register n → ℂ) :=
42+
(groverIterate f) ^ r • (HH n • δ[0])
43+
44+
noncomputable def groverTheta (n : ℕ) : ℝ :=
45+
Real.arcsin ((Real.sqrt 2)⁻¹ ^ n)
46+
47+
/-- The basis vector orthogonal to the uniform superposition `HH n • δ[0]`. Part of the diffusion
48+
operator's eigenbasis `{HH n • δ[0], perp ω}`. -/
49+
noncomputable def perp (ω : Register n) : Register n → ℂ :=
50+
(Real.cos (groverTheta n) : ℂ) • δ[ω] - (Real.sin (groverTheta n) : ℂ) • sPerp ω
51+
52+
/-- Flips the first coordinate of a 2D vector. -/
53+
def reflectTarget (v : EuclideanSpace ℝ (Fin 2)) : EuclideanSpace ℝ (Fin 2) := !₂[-v 0, v 1]
54+
55+
private noncomputable def groverOrientation : Orientation ℝ (EuclideanSpace ℝ (Fin 2)) (Fin 2) :=
56+
-(EuclideanSpace.basisFun (Fin 2) ℝ).toBasis.orientation
57+
58+
/-- Expresses the state in the 2D `(δ[ω], sPerp ω)` coordinate frame -/
59+
noncomputable def coord (ω : Register n) (v : EuclideanSpace ℝ (Fin 2)) : Register n → ℂ :=
60+
(v 0 : ℂ) • δ[ω] + (v 1 : ℂ) • sPerp ω
61+
62+
private lemma groverOrientation_areaForm (x y : EuclideanSpace ℝ (Fin 2)) :
63+
groverOrientation.areaForm x y = x 1 * y 0 - x 0 * y 1 := by
64+
simp [groverOrientation, Orientation.areaForm_neg_orientation,
65+
Orientation.volumeForm_robust _ (EuclideanSpace.basisFun (Fin 2) ℝ) rfl, Basis.det_apply,
66+
Orientation.areaForm_to_volumeForm, det_fin_two, Basis.toMatrix_apply]
67+
ring_nf
68+
69+
-- computes the 90° rotation operator
70+
private lemma groverOrientation_rightAngle (v : EuclideanSpace ℝ (Fin 2)) :
71+
groverOrientation.rightAngleRotation v = !₂[v 1, -v 0] := by
72+
apply ext_inner_left ℝ
73+
intro w
74+
rw [Orientation.inner_rightAngleRotation_right, groverOrientation_areaForm,PiLp.inner_apply]
75+
simp
76+
ring
77+
78+
private lemma groverOrientation_rotation_comp (α θ : ℝ) :
79+
groverOrientation.rotation (θ : Real.Angle) !₂[Real.sin α, Real.cos α] =
80+
!₂[Real.sin (α + θ), Real.cos (α + θ)] := by
81+
matrix_expand [Orientation.rotation_apply,groverOrientation_rightAngle,Real.sin_add, Real.cos_add]
82+
83+
theorem oracle_apply (k : Register n) : oracle f • δ[k] = (-1)^ ((f k) : ℕ) • δ[k] := by
84+
simp [funext_iff,oracle, basisVector_def,Submonoid.smul_def]
85+
grind
86+
87+
lemma uniform_decomp (ω : Register n) :
88+
HH n • δ[0] = (√2 : ℂ)⁻¹^n • δ[ω] + (√2 : ℂ)⁻¹^n • ∑ k ∈ Finset.univ.filter (· ≠ ω), δ[k] := by
89+
simp_rw [HH_apply,HadamardBasisVector,basisVector_def]
90+
aesop
91+
92+
93+
lemma zeroRefl_entry (j k : Register n) :(zeroRefl n).val j k =
94+
if j = k then (-1 : ℂ)^(if j = 0 then 0 else 1) else 0 := by
95+
rw [zeroRefl]
96+
aesop
97+
98+
lemma oracle_apply_omega {ω} (hω : f ω = 1) : oracle f • δ[ω] = -δ[ω] := by
99+
simp [oracle_apply,hω]
100+
101+
lemma zeroRefl_diagonal : (zeroRefl n).val = diagonal (fun x ↦ if x = 0 then 1 else -1) := by
102+
ext i j
103+
rw [zeroRefl_entry]
104+
aesop
105+
106+
lemma zeroRefl_smul_eq (r : Register n → ℂ) :
107+
(zeroRefl n) • r = (2 * r 0) • δ[0] - r := by
108+
simp [funext,Submonoid.smul_def,zeroRefl_diagonal,mulVec_diagonal,basisVector_def]
109+
grind
110+
111+
-- plus one eigenvalue
112+
lemma diffusion_fixes_uniform :
113+
(diffusion n) • (HH n • δ[0]) = HH n • δ[(0 : Register n)] := by
114+
rw [diffusion,SemigroupAction.mul_smul, SemigroupAction.mul_smul]
115+
with_reducible_and_instances congr 1
116+
simp [← SemigroupAction.mul_smul (HH n) (HH n),HH_sq,zeroRefl_smul_eq, basisVector_def, two_smul]
117+
118+
--- Math helper lemmas (extracting them like this keeps the ugliness contained)
119+
private lemma sqrt_two_inv_le_one : (√2 : ℝ)⁻¹ ≤ 1 :=
120+
inv_le_one_of_one_le₀ (by norm_num [← Real.sqrt_one,Real.sqrt_le_sqrt])
121+
122+
private lemma sqrt_two_pow_sub_sq (n : ℕ) :
123+
(Real.sqrt (2^n - 1) : ℂ)^2 = (2^n - 1 : ℂ) := by
124+
have: 1 ≤ 2^n := by exact Nat.one_le_two_pow
125+
norm_cast
126+
grind
127+
128+
private lemma amp_sq (n : ℕ) : ((√2)⁻¹ ^ n) ^ 2 = 1 / 2 ^ n := by
129+
rw [← pow_mul, mul_comm, pow_mul, inv_pow, Real.sq_sqrt (by norm_num : (0:ℝ) ≤ 2),
130+
inv_pow, one_div]
131+
132+
private lemma amp_sq_mul_two_pow (n : ℕ) : ((√2)⁻¹ ^ n) ^ 2 * 2 ^ n = 1 := by
133+
rw [amp_sq, one_div, inv_mul_cancel₀ (by positivity)]
134+
135+
private lemma sqrt_two_pow_sub_ne_zero (n : ℕ) (hn : n ≠ 0) :
136+
(Real.sqrt (2^n - 1) : ℂ) ≠ 0 := by
137+
have: (1 : ℝ) < 2^n := by exact_mod_cast Nat.one_lt_two_pow_iff.mpr hn
138+
grind [Complex.ofReal_ne_zero.mpr,Real.sqrt_ne_zero'.mpr]
139+
-----------------------------------------------------------------------
140+
141+
142+
--- Useful trigonometric lemmas specifically for groverTheta
143+
lemma sin_groverTheta_eq (n : ℕ) : Real.sin (groverTheta n) = (Real.sqrt 2)⁻¹ ^ n := by
144+
rw [groverTheta,Real.sin_arcsin]
145+
· linarith [pow_nonneg (inv_nonneg.mpr (Real.sqrt_nonneg 2)) n]
146+
· exact pow_le_one₀ (by positivity) sqrt_two_inv_le_one
147+
148+
lemma cos_groverTheta_eq (n : ℕ) :
149+
Real.cos (groverTheta n) = (√2)⁻¹ ^ n * √(2 ^ n - 1) := by
150+
rw [groverTheta,Real.cos_arcsin, ← Real.sqrt_sq (by positivity : (0:ℝ) ≤ (√2)⁻¹ ^ n),
151+
← Real.sqrt_mul (by positivity),Real.sq_sqrt (by positivity)]
152+
with_reducible_and_instances congr 1
153+
nlinarith [amp_sq n, amp_sq_mul_two_pow n]
154+
155+
156+
lemma groverTheta_pos : 0 < groverTheta n := by
157+
rw [groverTheta, Real.arcsin_pos]; positivity
158+
159+
lemma groverTheta_le (hn : n ≠ 0) : groverTheta n ≤ π / 4 := by
160+
rw [groverTheta,← Real.arcsin_sin (by linarith [Real.pi_pos])
161+
(show π/4 ≤ π/2 by linarith [Real.pi_pos]),Real.sin_pi_div_four]
162+
apply Real.monotone_arcsin
163+
rw [show √2/2 = (√2)⁻¹ by grind]
164+
exact pow_le_of_le_one (by positivity) sqrt_two_inv_le_one hn
165+
-------------------------------------------------------------------------
166+
167+
168+
lemma sPerp_apply (ω k : Register n) :
169+
sPerp ω k = if k = ω then 0 else (Real.sqrt ((2^n - 1 : ℕ) : ℝ) : ℂ)⁻¹ := by
170+
simp [sPerp,basisVector_def]
171+
172+
lemma oracle_apply_sPerp (ω : Register n)
173+
(hb : ∀ k, k ≠ ω → f k = 0) : oracle f • sPerp ω = sPerp ω := by
174+
rw [sPerp, smul_comm,Submonoid.smul_def, smul_eq_mulVec, mulVec_sum]
175+
with_reducible_and_instances congr 1
176+
refine Finset.sum_congr rfl fun k hk => ?_
177+
simpa [Submonoid.smul_def, hb k (by simpa using hk)] using oracle_apply f k
178+
179+
lemma diffusion_reflection (v : Register n → ℂ) :
180+
(diffusion n) • v = (2 * ((√2)⁻¹ : ℂ)^n * ∑ k, v k) • (HH n • δ[0]) - v := by
181+
simp_rw [diffusion, SemigroupAction.mul_smul, zeroRefl_smul_eq, HH_smul_zero_apply, smul_sub,
182+
← SemigroupAction.mul_smul, HH_sq, one_smul, smul_comm (HH n )]
183+
184+
lemma sum_sPerp (ω : Register n) :
185+
∑ k, sPerp ω k = (Real.sqrt (2^n - 1))⁻¹ * (2^n - 1) := by
186+
simp only [sPerp, Pi.smul_apply, smul_eq_mul, ← Finset.mul_sum,Finset.sum_apply]
187+
rw [Finset.sum_comm]
188+
simp [basisVector_def, Pi.basisFun_apply, Finset.filter_ne']
189+
190+
lemma uniform_decomp_orthonormal (ω : Register n) (hn : n ≠ 0) :
191+
HH n • δ[0] = Real.sin (groverTheta n) • δ[ω] + Real.cos (groverTheta n) • sPerp ω := by
192+
norm_num [uniform_decomp ω, sin_groverTheta_eq, cos_groverTheta_eq,sPerp,funext_iff]
193+
grind [sqrt_two_pow_sub_ne_zero n hn]
194+
195+
-- minus 1 eigenvalue
196+
lemma diffusion_negates_perp (ω : Register n) : (diffusion n) • perp ω = -perp ω := by
197+
have hsum : ∑ k, (perp ω) k = 0 := by
198+
simp only [perp, Finset.sum_sub_distrib, Pi.sub_apply, Pi.smul_apply, ← Finset.smul_sum]
199+
simp [basisVector_def, sum_sPerp, sin_groverTheta_eq, cos_groverTheta_eq]
200+
grind [sqrt_two_pow_sub_sq n]
201+
simp [diffusion_reflection,hsum]
202+
203+
204+
lemma oracle_coord (ω : Register n) (hω : f ω = 1) (hb : ∀ k, k ≠ ω → f k = 0)
205+
(v : EuclideanSpace ℝ (Fin 2)) :
206+
oracle f • coord ω v = coord ω (reflectTarget v) := by
207+
simp only [reflectTarget,funext_iff,coord, DistribSMul.smul_add, smul_comm,
208+
oracle_apply_omega f hω, oracle_apply_sPerp f ω hb]
209+
simp
210+
211+
-- eigenbasis {HH n • δ[0], perp ω}
212+
-- δ[ω] and sPerp ω are rotated by an angle
213+
lemma delta_in_eigenbasis (ω : Register n) (hn : n ≠ 0) :
214+
δ[ω] = (Real.sin (groverTheta n) : ℂ) • (HH n • δ[0]) + (Real.cos (groverTheta n) : ℂ) • perp ω
215+
:= by
216+
rw [perp,uniform_decomp_orthonormal ω hn]
217+
match_scalars <;> norm_num <;> ring_nf
218+
simp
219+
220+
lemma sPerp_in_eigenbasis (ω : Register n) (hn : n ≠ 0) :
221+
sPerp ω = (Real.cos (groverTheta n) : ℂ) • (HH n • δ[0]) - (Real.sin (groverTheta n) : ℂ) • perp ω
222+
:= by
223+
rw [perp,uniform_decomp_orthonormal ω hn]
224+
match_scalars <;> norm_num <;>ring_nf
225+
simp
226+
227+
lemma diffusion_eigen (ω : Register n) (a b : ℂ) :
228+
(diffusion n) • (a • (HH n • δ[0]) + b • perp ω) = a • (HH n • δ[0]) - b • perp ω
229+
:= by
230+
rw [smul_add, smul_comm (diffusion n) a, smul_comm (diffusion n) b,
231+
diffusion_fixes_uniform, diffusion_negates_perp, smul_neg]
232+
grind
233+
234+
lemma diffusion_omega (ω : Register n) (hn : n ≠ 0) :
235+
(diffusion n) • δ[ω] = coord ω !₂[-Real.cos (2*groverTheta n), Real.sin (2*groverTheta n)] := by
236+
rw [delta_in_eigenbasis ω hn, diffusion_eigen ω _ _,perp,coord]
237+
norm_num [funext_iff, uniform_decomp_orthonormal ω hn,Real.cos_two_mul, Real.sin_two_mul]
238+
grind [Complex.sin_sq_add_cos_sq]
239+
240+
lemma diffusion_sPerp (ω : Register n) (hn : n ≠ 0) :
241+
(diffusion n) • sPerp ω = coord ω !₂[Real.sin (2*groverTheta n), Real.cos (2*groverTheta n)] := by
242+
rw [sPerp_in_eigenbasis ω hn, sub_eq_add_neg, ← neg_smul, diffusion_eigen ω _, neg_smul,perp]
243+
norm_num [funext_iff, uniform_decomp_orthonormal ω hn, coord,Real.cos_two_mul, Real.sin_two_mul]
244+
grind [Complex.sin_sq_add_cos_sq]
245+
246+
-- Diffusion is a reflection too
247+
lemma diffusion_coord (ω : Register n) (hn : n ≠ 0)
248+
(v : EuclideanSpace ℝ (Fin 2)) : (diffusion n) • coord ω v =
249+
coord ω (groverOrientation.rotation (2 * groverTheta n : ℝ) (reflectTarget v)) := by
250+
ext
251+
simp [reflectTarget, Orientation.rotation_apply, groverOrientation_rightAngle, coord,
252+
smul_comm (diffusion n), diffusion_omega ω hn, diffusion_sPerp ω hn]
253+
ring
254+
255+
-- composing two reflections (diffusion and oracle) is a rotation by 2θ.
256+
lemma groverIterate_coord (ω : Register n) (hn : n ≠ 0) (hω : f ω = 1)
257+
(hb : ∀ k, k ≠ ω → f k = 0) (v : EuclideanSpace ℝ (Fin 2)) :
258+
groverIterate f • coord ω v =
259+
coord ω (groverOrientation.rotation (2 * groverTheta n : ℝ) v) := by
260+
rw [groverIterate, SemigroupAction.mul_smul, oracle_coord f ω hω hb,diffusion_coord ω hn]
261+
with_reducible_and_instances congr 2
262+
matrix_expand [reflectTarget]
263+
264+
lemma grover_coord_rotation (ω : Register n) (hn : n ≠ 0)
265+
(hω : f ω = 1) (hb : ∀ k, k ≠ ω → f k = 0) (t : ℕ) :
266+
grover f t = coord ω (groverOrientation.rotation (2 * t * groverTheta n : ℝ)
267+
!₂[Real.sin (groverTheta n), Real.cos (groverTheta n)]) := by
268+
induction t with
269+
| zero =>
270+
simp [funext_iff,Orientation.rotation_zero,grover, uniform_decomp_orthonormal ω hn, coord]
271+
| succ t ih =>
272+
simp only [grover, pow_succ', SemigroupAction.mul_smul] at ih ⊢
273+
norm_num [ih, groverIterate_coord f ω hn hω hb, ← Real.Angle.coe_add]
274+
ring_nf
275+
276+
lemma grover_rotation (ω : Register n) (hn : n ≠ 0) (hω : f ω = 1)
277+
(hb : ∀ k, k ≠ ω → f k = 0) (t : ℕ) :
278+
grover f t = (Real.sin ((2 * t + 1) * groverTheta n) : ℂ) • δ[ω] +
279+
(Real.cos ((2 * t + 1) * groverTheta n) : ℂ) • sPerp ω := by
280+
norm_num [grover_coord_rotation f ω hn hω hb, groverOrientation_rotation_comp, coord]
281+
ring_nf
282+
283+
theorem grover_success_prob (ω : Register n) (hn : n ≠ 0)
284+
(hω : f ω = 1) (hb : ∀ k, k ≠ ω → f k = 0) (r : ℕ) :
285+
‖(grover f r) ω‖^2 = Real.sin ((2 * r + 1) * groverTheta n) ^ 2 := by
286+
simp_rw [grover_rotation f ω hn hω hb,Pi.add_apply, Pi.smul_apply, smul_eq_mul,sPerp_apply,
287+
if_true,basisVector_def, Pi.basisFun_apply, Pi.single_eq_same,mul_zero, add_zero, mul_one,
288+
Complex.norm_real,Real.norm_eq_abs, sq_abs]
289+
290+
-- Finding per-iteration success probability of grover is the hard part and has been done.
291+
-- Arguing about the best iteration r is simple but tedious algerba without much physics.
292+
-- This is done below:
293+
294+
noncomputable def r_grover (n : ℕ) : ℕ := Nat.floor (π / (4 * groverTheta n))
295+
296+
lemma r_grover_window :
297+
|(2 * r_grover n + 1) * groverTheta n - π/2| ≤ groverTheta n := by
298+
have hpos : 0 < groverTheta n := groverTheta_pos
299+
have hpos2 : 0 ≤ π / (4 * groverTheta n) := by positivity
300+
have hpi : 2 * (π / (4 * groverTheta n)) * groverTheta n = π / 2 := by field_simp; ring
301+
rw [r_grover, abs_le]
302+
constructor <;>
303+
nlinarith [hpi, hpos.le, Nat.floor_le hpos2, Nat.lt_floor_add_one (π / (4 * groverTheta n))]
304+
305+
lemma sin_square_phi_gt {φ θ : ℝ}
306+
(hθ : 0 ≤ θ) (hθover4 : θ ≤ π / 4) (hw : |φ - π / 2| ≤ θ) : 1 - Real.sin φ ^ 2 ≤ Real.sin θ ^ 2
307+
:= by
308+
have hge : Real.cos θ ≤ Real.sin φ := by
309+
rw [Eq.symm (Real.cos_sub_pi_div_two φ),← Real.cos_abs (φ - π/2)]
310+
exact Real.cos_le_cos_of_nonneg_of_le_pi (abs_nonneg _) (by linarith [Real.pi_pos]) hw
311+
have hcos_pos : 0 ≤ Real.cos θ := Real.cos_nonneg_of_mem_Icc ⟨?_,?_ ⟩<;>
312+
nlinarith [Real.pi_pos, Real.sin_sq_add_cos_sq θ, Real.sin_sq_add_cos_sq φ]
313+
314+
theorem grover_finds_target (ω : Register n) (hn : n ≠ 0)
315+
(hω : f ω = 1) (hb : ∀ k, k ≠ ω → f k = 0) :
316+
1 - ‖(grover f (r_grover n)) ω‖ ^ 2 ≤ 1 / 2 ^ n := by
317+
rw [grover_success_prob f ω hn hω hb]
318+
have := sin_square_phi_gt groverTheta_pos.le (groverTheta_le hn) (r_grover_window)
319+
grind [sin_groverTheta_eq, amp_sq n]
320+
321+
lemma r_grover_upper_bound : r_grover n ≤ π / 4 * Real.sqrt (2 ^ n) := by
322+
have hθ : 0 < groverTheta n := groverTheta_pos
323+
have: (√2)⁻¹ ^ n ≤ groverTheta n := sin_groverTheta_eq n ▸ (Real.sin_lt hθ).le
324+
refine (Nat.floor_le (by positivity)).trans ?_
325+
ring_nf
326+
with_reducible_and_instances gcongr
327+
rw [Real.le_sqrt' (by positivity), ← inv_inv (2 ^ n), ← one_div (2 ^ n), ← amp_sq n, ← inv_pow]
328+
with_reducible_and_instances gcongr
329+
330+
--- A final theorem that wraps up the important results
331+
332+
theorem grover_search (ω : Register n) (hn : n ≠ 0) (hω : f ω = 1) (hb : ∀ k, k ≠ ω → f k = 0) :
333+
∃ r : ℕ, r ≤ π / 4 * Real.sqrt (2 ^ n) ∧ 1 - ‖(grover f r) ω‖ ^ 2 ≤ 1 / 2 ^ n :=
334+
⟨r_grover n, r_grover_upper_bound , grover_finds_target f ω hn hω hb⟩

0 commit comments

Comments
 (0)