OAI/Computability/QuantumFactoring/ExactnessFurther.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ExactQuantumFactoring.Exactness.finiteInner line 10
  2. def OAI.ExactQuantumFactoring.Exactness.outcomeMass line 13
  3. def OAI.ExactQuantumFactoring.Exactness.goodPart line 17
  4. def OAI.ExactQuantumFactoring.Exactness.stateReflection line 21
  5. lemma OAI.ExactQuantumFactoring.Exactness.finiteInner_self line 24
  6. lemma OAI.ExactQuantumFactoring.Exactness.finiteInner_goodPart line 29
  7. lemma OAI.ExactQuantumFactoring.Exactness.finiteInner_sub line 38
  8. lemma OAI.ExactQuantumFactoring.Exactness.finiteInner_mul line 42
  9. lemma OAI.ExactQuantumFactoring.Exactness.one_reflection line 51

    Source documentation

    Literal one-reflection identity (6.9). The amplitude is not renormalized by fiat.

    lemma one_reflection {ι : Type*} [Fintype ι] (good : ι → Prop) (ψ : ι → ℂ)
    (hψ : (∑ x, Complex.normSq (ψ x))=1) (hg : outcomeMass good ψ=1/4) :
    stateReflection ψ (fun x => ψ x-2*goodPart good ψ x) = fun x => 2*goodPart good ψ x := by
…

    Mentions: OAI.ExactQuantumFactoring.Exactness.outcomeMass, OAI.ExactQuantumFactoring.Exactness.stateReflection, OAI.ExactQuantumFactoring.Exactness.goodPart

  10. lemma OAI.ExactQuantumFactoring.Exactness.amplified_mass line 62
  11. lemma OAI.ExactQuantumFactoring.Exactness.one_reflection_correct line 79

    Source documentation

    Exact success also applies to the externally requested correct-output predicate.

    lemma one_reflection_correct {ι : Type*} [Fintype ι]
    (good correct : ι → Prop) (ψ : ι → ℂ)
    (hψ : (∑ x, Complex.normSq (ψ x))=1)
    (hg : outcomeMass good ψ=1/4) (hc : ∀ x, good x → correct x) :
    outcomeMass correct (stateReflection ψ (fun x => ψ x-2*goodPart good ψ x))=1 := by
…

    Mentions: OAI.ExactQuantumFactoring.Exactness.outcomeMass, OAI.ExactQuantumFactoring.Exactness.stateReflection, OAI.ExactQuantumFactoring.Exactness.goodPart