OAI/Computability/QuantumFactoring/ListTransition.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The actual uniform-list transition in Section 5: its event, exact closed probability, and unchanged repetition guarantee.

  1. def OAI.ExactQuantumFactoring.FavorableBits line 22
  2. lemma OAI.ExactQuantumFactoring.favorableBits_mass line 26
  3. lemma OAI.ExactQuantumFactoring.coveringPower_le_twice line 51
  4. lemma OAI.ExactQuantumFactoring.favorableBits_lower line 62
  5. def OAI.ExactQuantumFactoring.GoodList line 80
  6. theorem OAI.ExactQuantumFactoring.list_good_mass line 85

    Source documentation

    Source formula (5.4), over the literal independent fair-bit preparation.

    theorem list_good_mass {m n : ℕ} (hm : m ≠ 0) (hb : m < 2^n)
    (hodd : Odd m) (p₀ : Component m) (K : ℕ) :
    outcomeMass (GoodList hm hb p₀ K) (tensorState (fairState (Nat.clog 2 m)) K)=
      1-(1-(favorableCount m n : ℝ)/(2:ℝ)^(Nat.clog 2 m))^K := by
…

    Mentions: OAI.ExactQuantumFactoring.Component, OAI.ExactQuantumFactoring.GoodList, OAI.ExactQuantumFactoring.fairState, OAI.ExactQuantumFactoring.favorableCount

  7. theorem OAI.ExactQuantumFactoring.list_good_lower line 93