UpperBoundArithmetic.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem335.gateCount_le_pow line 9

Source documentation

The elementary gate-count estimate, before specializing the block parameters.

theorem gateCount_le_pow (n t r : ℕ) (hn : 3 ≤ n)
    (ht : 2 ≤ t) (hr : r ≤ t) (htn : t ≤ n) :
    2 * n ^ 3 + r * n ^ 2 + r * n ^ (t + 1) + n ^ (r - 1) + 1 ≤
      n ^ (t + 3) := by
…

theorem OAI.Problem335.gateCount_le_rpow line 42

Source documentation

Conversion of the integer block gate count into the advertised real-power bound.

theorem gateCount_le_rpow (n t r : ℕ) (hn : 3 ≤ n)
    (ht : 2 ≤ t) (hr : r ≤ t) (htn : t ≤ n)
    (htsqrt : (t : ℝ) ≤ Real.sqrt (n : ℝ) + 1) :
    ((2 * n ^ 3 + r * n ^ 2 + r * n ^ (t + 1) + n ^ (r - 1) + 1 : ℕ) : ℝ) ≤
      (n : ℝ) ^ (Real.sqrt (n : ℝ) + 4) := by
…

theorem OAI.Problem335.upperGateBound_two_le_rpow line 58
Source documentation
The exceptional smallest size in the upper-bound estimate.
```
theorem upperGateBound_two_le_rpow :
    (upperGateBound 2 : ℝ) ≤ (2 : ℝ) ^ (Real.sqrt 2 + 4) := by
…
```
Mentions: OAI.Problem335.upperGateBound
theorem OAI.Problem335.upperGateBound_le_rpow line 72
Source documentation
The explicit gate bound is at most n^(sqrt n + 4).
```
theorem upperGateBound_le_rpow (n : ℕ) (hn : 2 ≤ n) :
    (upperGateBound n : ℝ) ≤ (n : ℝ) ^ (Real.sqrt (n : ℝ) + 4) := by
…
```
Mentions: OAI.Problem335.upperGateBound