LevelBounds.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.ExactQuantumFactoring.div_lower_power_two line 14

theorem OAI.ExactQuantumFactoring.levelCount_closed line 23

Source documentation

The traditional cyclic-group level law u, u, 2u, 4u, ... .

theorem levelCount_closed (G : Type*) [CommGroup G] [Fintype G] [IsCyclic G] (t : ℕ) :
    levelCount G t = if t = 0 then Fintype.card G / 2^padicValNat 2 (Fintype.card G)
      else if t ≤ padicValNat 2 (Fintype.card G) then
        2^(t-1) * (Fintype.card G / 2^padicValNat 2 (Fintype.card G)) else 0 := by
…

Mentions: OAI.ExactQuantumFactoring.levelCount

theorem OAI.ExactQuantumFactoring.two_mul_levelCount_le line 50
Source documentation
No particular level has more than half the elements of a cyclic group of even order, including the lowest level and the unique top level.
```
theorem two_mul_levelCount_le (G : Type*) [CommGroup G] [Fintype G] [IsCyclic G]
    (heven : 2 ∣ Fintype.card G) (t : ℕ) : 2 * levelCount G t ≤ Fintype.card G := by
…
```
Mentions: OAI.ExactQuantumFactoring.levelCount