OAI/Computability/QuantumFactoring/RepeatedTrials.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Exact independent-trial laws and the source's K=n^5 success guarantee.

  1. def OAI.ExactQuantumFactoring.RepeatedTrials.tensorState line 16
  2. lemma OAI.ExactQuantumFactoring.RepeatedTrials.tensor_normalized line 19
  3. lemma OAI.ExactQuantumFactoring.RepeatedTrials.tensor_all_mass line 28
  4. lemma OAI.ExactQuantumFactoring.RepeatedTrials.mass_compl line 44
  5. lemma OAI.ExactQuantumFactoring.RepeatedTrials.tensor_some_mass line 56
  6. lemma OAI.ExactQuantumFactoring.RepeatedTrials.mass_bounds line 66
  7. lemma OAI.ExactQuantumFactoring.RepeatedTrials.repetition_failure_bound line 82

    Source documentation

    Deliberately uses the original cutoff128 and repetition exponent5.

    lemma repetition_failure_bound {n : ℕ} (hn : 128≤n) {x : ℝ}
    (hx₀ : 1/(2048*(n+1):ℝ)≤x) (hx₁ : x≤1) :
    (1-x)^(n^5)≤1/(2:ℝ)^(2*n) := by
…
  8. lemma OAI.ExactQuantumFactoring.RepeatedTrials.repeated_success_lower line 119