OAI/InformationTheory/QuantumCircuit/Polynomial.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.QAC.weight line 12

    Source documentation

    The coefficient norm required to pay for expanding powers of a count.

    def weight (R : ℝ) (p : ℝ[X]) : ℝ := p.sum fun k c => |c| * R ^ k
  2. lemma OAI.QAC.weight_nonneg line 14
  3. lemma OAI.QAC.weight_zero line 17
  4. lemma OAI.QAC.weight_monomial line 18
  5. lemma OAI.QAC.weight_C line 20
  6. lemma OAI.QAC.weight_one line 21
  7. lemma OAI.QAC.weight_X line 23
  8. lemma OAI.QAC.weight_add_le line 25
  9. lemma OAI.QAC.weight_neg line 38
  10. lemma OAI.QAC.weight_sub_le line 41
  11. lemma OAI.QAC.weight_sum_le line 45
  12. lemma OAI.QAC.weight_mul_le line 54
  13. lemma OAI.QAC.weight_prod_le line 73
  14. lemma OAI.QAC.weight_chebyshev line 83
  15. lemma OAI.QAC.chebyshev_abs_le_one line 115
  16. lemma OAI.QAC.chebyshev_denominator line 121

    Source documentation

    An elementary hyperbolic lower bound for the Chebyshev denominator.

    lemma chebyshev_denominator (k : ℕ) {m r : ℝ} (hr : 0 < r) (hm : r < m) :
    1 ≤ (Polynomial.Chebyshev.T ℝ k).eval ((m + r) / (m - r)) ∧
    Real.exp ((k : ℝ) * Real.sqrt (r / m)) / 2 ≤
      (Polynomial.Chebyshev.T ℝ k).eval ((m + r) / (m - r)) := by
…
  17. def OAI.QAC.rootPoly line 162

    Source documentation

    Exact roots at the first r positive integers.

    def rootPoly (r : ℕ) : ℝ[X] :=
…
  18. lemma OAI.QAC.rootPoly_eval_zero line 165
  19. lemma OAI.QAC.rootPoly_eval_nat line 168
  20. lemma OAI.QAC.rootPoly_weight line 178
  21. lemma OAI.QAC.rootPoly_abs_eval line 196
  22. lemma OAI.QAC.rootPoly_degree line 213
  23. def OAI.QAC.scalePoly line 225

    Source documentation

    The affine map taking [r,m] onto [1,-1].

    def scalePoly (r m : ℝ) : ℝ[X] := C ((m + r) / (m - r)) - C (2 / (m - r)) * X
  24. lemma OAI.QAC.scalePoly_eval line 227
  25. lemma OAI.QAC.scalePoly_zero line 232
  26. lemma OAI.QAC.scalePoly_interval line 235
  27. lemma OAI.QAC.scalePoly_degree line 244
  28. lemma OAI.QAC.scalePoly_weight line 249
  29. def OAI.QAC.approxPoly line 266
  30. lemma OAI.QAC.approxPoly_bounds line 271

    Source documentation

    Finite degree, coefficient, normalization, and decay bounds for the approximating polynomial.

    lemma approxPoly_bounds {r m k : ℕ} {R : ℝ} (hR : 0 ≤ R)
    (hr : 1 ≤ r) (hm : 2 * r ≤ m)
    (hk : 4 * (r : ℝ) * Real.log m ≤ (k : ℝ) * Real.sqrt ((r : ℝ) / m)) :
    (approxPoly r m k).natDegree ≤ r + k ∧
    weight R (approxPoly r m k) ≤ (1 + R) ^ r * (7 + 4 * R) ^ k ∧
    (approxPoly r m k).eval 0 = 1 ∧
    ∀ x : ℕ, 1 ≤ x → x ≤ m →
      |(approxPoly r m k).eval (x : ℝ)| ≤ 2 * Real.exp (-(3 * (r : ℝ) * Real.log m)) := by
…

    Mentions: OAI.QAC.approxPoly, OAI.QAC.weight