OAI/Computability/QuantumFactoring/OrderTrial.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ExactQuantumFactoring.OrderTrial.phase_bin_progression line 12
2. def OAI.ExactQuantumFactoring.OrderTrial.residueAmplitude line 37

   Source documentation

   Equation (order-P), before squaring the norm.

   noncomputable def residueAmplitude (Q d j t : ℕ) : ℂ :=
   …

3. def OAI.ExactQuantumFactoring.OrderTrial.residueProbability line 41
4. lemma OAI.ExactQuantumFactoring.OrderTrial.residueAmplitude_samples line 44
5. lemma OAI.ExactQuantumFactoring.OrderTrial.residueAmplitude_integral_error line 61
6. lemma OAI.ExactQuantumFactoring.OrderTrial.residueAmplitude_norm_le line 106
7. lemma OAI.ExactQuantumFactoring.OrderTrial.norm_square_difference_le line 124
8. lemma OAI.ExactQuantumFactoring.OrderTrial.residueProbability_integral_error line 131

   Source documentation

   The key approximation (majorant-integral-bounds), for the exact source P.

   lemma residueProbability_integral_error {Q d t : ℕ} (hd : 0 < d) (hdQ : d ≤ Q)
       (ht : t < d) (j : ℕ) :
       |residueProbability Q d j t -
         ‖residueIntegral d (((j*t)%d : ℕ):ℝ) (binError Q d j)‖^2| ≤ 32/(Q:ℝ) := by
   …

   Mentions: OAI.ExactQuantumFactoring.OrderTrial.residueProbability, OAI.ExactQuantumFactoring.OrderTrial.residueIntegral, OAI.ExactQuantumFactoring.OrderTrial.binError

9. def OAI.ExactQuantumFactoring.OrderTrial.rampSq line 157

   Source documentation

   A positive-part square. This supplies a globally C¹ rational spline primitive.

   noncomputable def rampSq (x : ℝ) : ℝ := (max 0 x)^2

10. lemma OAI.ExactQuantumFactoring.OrderTrial.rampSq_hasDerivAt line 159
11. lemma OAI.ExactQuantumFactoring.OrderTrial.rampSq_continuous line 185
12. lemma OAI.ExactQuantumFactoring.OrderTrial.rampSq_shift_hasDerivAt line 189
13. def OAI.ExactQuantumFactoring.OrderTrial.splineRe line 194
14. def OAI.ExactQuantumFactoring.OrderTrial.splineIm line 197
15. def OAI.ExactQuantumFactoring.OrderTrial.splineReDeriv line 201
16. def OAI.ExactQuantumFactoring.OrderTrial.splineImDeriv line 204
17. lemma OAI.ExactQuantumFactoring.OrderTrial.splineRe_hasDerivAt line 208
18. lemma OAI.ExactQuantumFactoring.OrderTrial.splineIm_hasDerivAt line 218
19. def OAI.ExactQuantumFactoring.OrderTrial.spline line 231
20. lemma OAI.ExactQuantumFactoring.OrderTrial.spline_hasDerivAt line 233
21. lemma OAI.ExactQuantumFactoring.OrderTrial.splineReDeriv_eq line 242
22. lemma OAI.ExactQuantumFactoring.OrderTrial.splineImDeriv_eq line 267
23. lemma OAI.ExactQuantumFactoring.OrderTrial.spline_derivative line 309
24. lemma OAI.ExactQuantumFactoring.OrderTrial.spline_zero line 316
25. lemma OAI.ExactQuantumFactoring.OrderTrial.spline_integral line 319
26. def OAI.ExactQuantumFactoring.OrderTrial.rampPiece line 336

    Source documentation

    Rational polynomial on a quarter interval; no real oracle is used in its data.

    noncomputable def rampPiece (q a : ℤ) : ℚ[X] :=
    …

27. def OAI.ExactQuantumFactoring.OrderTrial.evalReal line 339
28. lemma OAI.ExactQuantumFactoring.OrderTrial.evalReal_rampPiece line 341
29. def OAI.ExactQuantumFactoring.OrderTrial.splineRePiece line 354
30. def OAI.ExactQuantumFactoring.OrderTrial.splineImPiece line 358
31. lemma OAI.ExactQuantumFactoring.OrderTrial.evalReal_splineRePiece line 362
32. lemma OAI.ExactQuantumFactoring.OrderTrial.evalReal_splineImPiece line 375
33. lemma OAI.ExactQuantumFactoring.OrderTrial.poly_add_degree line 390
34. lemma OAI.ExactQuantumFactoring.OrderTrial.poly_sub_degree line 393
35. lemma OAI.ExactQuantumFactoring.OrderTrial.rampPiece_natDegree_le line 396
36. lemma OAI.ExactQuantumFactoring.OrderTrial.splineRePiece_natDegree_le line 405
37. lemma OAI.ExactQuantumFactoring.OrderTrial.splineImPiece_natDegree_le line 421