ArithmeticBounds.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.ExactQuantumFactoring.prod_le_card_mul_pred_prod line 13

Source documentation

The telescoping estimate for any distinct integers at least two.

theorem prod_le_card_mul_pred_prod (s : Finset ℕ) (hs : ∀ p ∈ s, 2 ≤ p) :
    (∏ p ∈ s, p) ≤ (s.card + 1) * ∏ p ∈ s, (p - 1) := by
…

theorem OAI.ExactQuantumFactoring.primeFactors_card_lt line 38
Source documentation
The number of distinct prime factors is less than a strict binary cutoff.
```
theorem primeFactors_card_lt {d n : ℕ} (hd : 0 < d) (hb : d < 2 ^ n) :
    d.primeFactors.card < n := by
…
```
theorem OAI.ExactQuantumFactoring.le_succ_mul_totient line 49
Source documentation
Integer form of (5.2), retaining the original global binary cutoff.
```
theorem le_succ_mul_totient {d n : ℕ} (hd : 0 < d) (hb : d < 2 ^ n) :
    d ≤ (n + 1) * Nat.totient d := by
…
```
theorem OAI.ExactQuantumFactoring.totient_ratio_lower line 66
Source documentation
Real ratio version, ready for the exact transition-probability bound.
```
theorem totient_ratio_lower {d n : ℕ} (hd : 0 < d) (hb : d < 2 ^ n) :
    1 / ((n : ℝ) + 1) ≤ (Nat.totient d : ℝ) / d := by
…
```