OAI/Computability/QuantumFactoring/OrderTrialFurther.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ExactQuantumFactoring.OrderTrial.residueIntegral_eq_primitive line 12
  2. lemma OAI.ExactQuantumFactoring.OrderTrial.residueIntegral_zero line 24
  3. def OAI.ExactQuantumFactoring.OrderTrial.rampLinear line 28
  4. lemma OAI.ExactQuantumFactoring.OrderTrial.evalReal_rampLinear line 30
  5. def OAI.ExactQuantumFactoring.OrderTrial.phaseRePiece line 43
  6. def OAI.ExactQuantumFactoring.OrderTrial.phaseImPiece line 45
  7. lemma OAI.ExactQuantumFactoring.OrderTrial.evalReal_phaseRePiece line 49
  8. lemma OAI.ExactQuantumFactoring.OrderTrial.evalReal_phaseImPiece line 62
  9. lemma OAI.ExactQuantumFactoring.OrderTrial.rampLinear_natDegree_le line 76
  10. lemma OAI.ExactQuantumFactoring.OrderTrial.phaseRePiece_natDegree_le line 82
  11. lemma OAI.ExactQuantumFactoring.OrderTrial.phaseImPiece_natDegree_le line 96
  12. lemma OAI.ExactQuantumFactoring.OrderTrial.evalReal_add line 116
  13. lemma OAI.ExactQuantumFactoring.OrderTrial.evalReal_sub line 118
  14. lemma OAI.ExactQuantumFactoring.OrderTrial.evalReal_mul line 120
  15. lemma OAI.ExactQuantumFactoring.OrderTrial.evalReal_pow line 122
  16. lemma OAI.ExactQuantumFactoring.OrderTrial.evalReal_C line 124
  17. lemma OAI.ExactQuantumFactoring.OrderTrial.evalReal_X line 126
  18. lemma OAI.ExactQuantumFactoring.OrderTrial.evalReal_comp line 127
  19. def OAI.ExactQuantumFactoring.OrderTrial.linearArg line 130
  20. lemma OAI.ExactQuantumFactoring.OrderTrial.evalReal_linearArg line 132
  21. lemma OAI.ExactQuantumFactoring.OrderTrial.linearArg_natDegree_le line 138
  22. def OAI.ExactQuantumFactoring.OrderTrial.integralPiece line 144

    Source documentation

    The exact integral-coordinate polynomial, with the zero slope handled without division.

    noncomputable def integralPiece (d : ℕ) (η : ℚ) (A G₀ G₁ : ℚ[X]) : ℚ[X] :=
…
  23. lemma OAI.ExactQuantumFactoring.OrderTrial.integralPiece_natDegree_le line 148
  24. lemma OAI.ExactQuantumFactoring.OrderTrial.evalReal_integralPiece line 163
  25. def OAI.ExactQuantumFactoring.OrderTrial.massPiece line 170
  26. lemma OAI.ExactQuantumFactoring.OrderTrial.massPiece_natDegree_le line 174
  27. lemma OAI.ExactQuantumFactoring.OrderTrial.massPiece_eq line 186
  28. def OAI.ExactQuantumFactoring.OrderTrial.roundCoeff line 220

    Source documentation

    Upward coefficient rounding by a specified integer denominator.

    def roundCoeff (D : ℕ) (a : ℚ) : ℚ := (⌈(D:ℚ)*a⌉:ℤ)/(D:ℚ)
  29. lemma OAI.ExactQuantumFactoring.OrderTrial.roundCoeff_error line 222
  30. lemma OAI.ExactQuantumFactoring.OrderTrial.roundCoeff_error_real line 237
  31. def OAI.ExactQuantumFactoring.OrderTrial.roundedValue line 246
  32. lemma OAI.ExactQuantumFactoring.OrderTrial.roundedValue_error line 249
  33. lemma OAI.ExactQuantumFactoring.OrderTrial.five_powers_bound line 270
  34. lemma OAI.ExactQuantumFactoring.OrderTrial.roundedValue_small_error line 289
  35. def OAI.ExactQuantumFactoring.OrderTrial.binErrorRat line 316

    Source documentation

    Exact rational form of the nearest-bin error.

    def binErrorRat (Q d j : ℕ) : ℚ := (bin Q d j : ℚ)-(j:ℚ)*Q/d

    Mentions: OAI.ExactQuantumFactoring.OrderTrial.bin

  36. lemma OAI.ExactQuantumFactoring.OrderTrial.binErrorRat_cast line 318
  37. def OAI.ExactQuantumFactoring.OrderTrial.quarterIndex line 322

    Source documentation

    Half-open quarter assignment, computed only by rational arithmetic.

    def quarterIndex (x : ℚ) : ℤ := ⌊4*x⌋
  38. lemma OAI.ExactQuantumFactoring.OrderTrial.quarterIndex_bounds line 324
  39. def OAI.ExactQuantumFactoring.OrderTrial.selectedMass line 334
  40. lemma OAI.ExactQuantumFactoring.OrderTrial.selectedMass_natDegree_le line 337
  41. lemma OAI.ExactQuantumFactoring.OrderTrial.selectedMass_eq line 340
  42. def OAI.ExactQuantumFactoring.OrderTrial.majorant line 350

    Source documentation

    Literal majorant from (majorant-construction), retaining Q and B as arguments.

    noncomputable def majorant (Q B d j u : ℕ) : ℚ :=
…
  43. lemma OAI.ExactQuantumFactoring.OrderTrial.majorant_ideal_error line 353
  44. lemma OAI.ExactQuantumFactoring.OrderTrial.majorant_nonneg line 366
  45. lemma OAI.ExactQuantumFactoring.OrderTrial.majorant_probability_error line 375

    Source documentation

    Source majorant-error, with the stronger explicit margin 32/Q..97/Q.

    lemma majorant_probability_error {Q B d t : ℕ} (hB : 2 ≤ B)
    (hd : 0 < d) (hdB : d ≤ B) (hdQ : d ≤ Q) (ht : t < d) (j : ℕ) :
    32/(Q:ℝ) ≤ (majorant Q B d j ((j*t)%d):ℝ)-residueProbability Q d j t ∧
      (majorant Q B d j ((j*t)%d):ℝ)-residueProbability Q d j t ≤ 97/(Q:ℝ) := by
…

    Mentions: OAI.ExactQuantumFactoring.OrderTrial.majorant, OAI.ExactQuantumFactoring.OrderTrial.residueProbability

  46. def OAI.ExactQuantumFactoring.OrderTrial.majorantSum line 386

    Source documentation

    Source half-sum, initially a mathematical sum; bounded-piece evaluation follows.

    noncomputable def majorantSum (Q B d j : ℕ) : ℚ :=
…
  47. lemma OAI.ExactQuantumFactoring.OrderTrial.majorantSum_lower line 389
  48. lemma OAI.ExactQuantumFactoring.OrderTrial.majorantSum_upper line 411