Measurement.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

def OAI.QAC.outputZeroCount line 12
Source documentation
The measured zero-outcome projector is a product projection on one qubit.
```
def outputZeroCount {N : ℕ} (out : Fin N) : Count N where
…
```
Mentions: OAI.QAC.Count
lemma OAI.QAC.outputZeroCount_diagonal line 17
def OAI.QAC.outputProbability line 34
Source documentation
Born probability for an arbitrary fixed input basis state.
```
def outputProbability {N : ℕ} (W : Operator N) (out : Fin N) (b : Bit) (z : Word N) : ℝ :=
…
```
Mentions: OAI.QAC.Operator, OAI.QAC.Bit, OAI.QAC.Word
lemma OAI.QAC.born_zero_diagonal line 37
lemma OAI.QAC.total_born_probability line 48
lemma OAI.QAC.outputProbability_complement line 55
lemma OAI.QAC.success_character_lower line 64

lemma OAI.QAC.parity_advantage_from_entries line 79

Source documentation

The finite Fourier step, with all final garbage summed out by the Born rule.

lemma parity_advantage_from_entries {n N : ℕ} (hn : 0<n) (hnN : n ≤ N)
    (W : Operator N) (hW : W ∈ unitary (Operator N)) (out : Fin N) {ε δ : ℝ}
    (hsuccess : ∀ x : Word n, 1/2+ε ≤ successProbability W out x)
    (hentry : ∀ x : Word n,
      ‖(localMatrix (inputHadamard n N)*(star W*(outputZeroCount out).zero*W)*
        localMatrix (inputHadamard n N)) (flipWord (inputSet n N) (inputWord x)) (inputWord x)‖ ≤ δ) :
    ε ≤ δ := by
…

Mentions: OAI.QAC.Operator, OAI.QAC.Word, OAI.QAC.successProbability, OAI.QAC.localMatrix, OAI.QAC.inputHadamard, OAI.QAC.outputZeroCount, OAI.QAC.flipWord, OAI.QAC.inputSet, OAI.QAC.inputWord