OAI/InformationTheory/QuantumCircuit/Asymptotics.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.QAC.eventually_power_le line 12

   Source documentation

   Strict exponent gaps absorb every fixed multiplicative constant.

   lemma eventually_power_le {s t : ℝ} (hst : s < t) (C : ℝ) :
       ∀ᶠ N : ℕ in atTop, C * (N : ℝ) ^ s ≤ (N : ℝ) ^ t := by
   …

2. lemma OAI.QAC.eventually_power_log_le line 24

   Source documentation

   The same strict gap absorbs a logarithm, with no change to the exponent.

   lemma eventually_power_log_le {s t : ℝ} (hst : s < t) (C : ℝ) :
       ∀ᶠ N : ℕ in atTop, C * (N : ℝ) ^ s * Real.log N ≤ (N : ℝ) ^ t := by
   …

3. lemma OAI.QAC.ceil_rpow_bounds line 42
4. lemma OAI.QAC.ceil_rpow_log line 52
5. lemma OAI.QAC.approx_weight_exp line 69
6. lemma OAI.QAC.approx_decay_exp line 99
7. lemma OAI.QAC.ceil_approx_condition line 113
8. theorem OAI.QAC.polynomial_approximation line 159

   Source documentation

   Polynomial approximation uniform in N, including b > 1.

   theorem polynomial_approximation {a b u : ℝ} (ha : 0 < a) (hab : a < b)
       (hu : (a + b) / 2 < u) :
       ∀ᶠ N : ℕ in atTop, ∃ p : ℝ[X],
         (p.natDegree : ℝ) ≤ (N : ℝ) ^ u ∧ weight N p ≤ Real.exp ((N : ℝ) ^ u) ∧
         p.eval 0 = 1 ∧ ∀ x : ℕ, 1 ≤ x → x ≤ ⌈(N : ℝ) ^ b⌉₊ →
           |p.eval (x : ℝ)| ≤ Real.exp (-((N : ℝ) ^ a)) := by
   …

   Mentions: OAI.QAC.weight

9. lemma OAI.QAC.eventually_two_powers_le line 209
10. lemma OAI.QAC.eventually_exp_power_gap line 215

    Source documentation

    Every fixed coefficient and prefactor is absorbed by the strict power gaps.

    lemma eventually_exp_power_gap {s u v : ℝ} (hs : s < v) (hu : u < v) (hv : 0 < v)
        (C ε D K : ℝ) (hC : 0 < C) (hε : 0 < ε) :
        ∀ᶠ N : ℕ in atTop, C * Real.exp (K*(N:ℝ)^u - (N:ℝ)^v) ≤
          ε * Real.exp (-(D*(N:ℝ)^s)) := by
    …

11. lemma OAI.QAC.ceil_power_log_bound line 230
12. lemma OAI.QAC.eventually_pattern_cost line 246
13. lemma OAI.QAC.eventually_backward_cost line 260