QuantumAcceptance.lean`

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Zero-ancilla witness inclusion and the actual Born probability bounds.

def OAI.ContinuumCoulomb.qmaWitnessBasis line 14
Source documentation
A witness basis vector with every ancillary qubit set to zero.
```
def qmaWitnessBasis (c : QMACircuit) (s : SourceSpinBasis c.witness) :
    SourceSpinBasis (c.work + 1) :=
…
```
Mentions: OAI.ContinuumCoulomb.QMACircuit, OAI.ContinuumCoulomb.SourceSpinBasis
def OAI.ContinuumCoulomb.qmaWitnessPrefix line 19
Source documentation
Restriction to the witness register of a well-formed circuit.
```
def qmaWitnessPrefix (c : QMACircuit) (hc : c.WellFormed)
    (s : SourceSpinBasis (c.work + 1)) : SourceSpinBasis c.witness :=
…
```
Mentions: OAI.ContinuumCoulomb.QMACircuit, OAI.ContinuumCoulomb.SourceSpinBasis
theorem OAI.ContinuumCoulomb.qmaWitnessPrefix_basis line 23
theorem OAI.ContinuumCoulomb.qmaWitnessBasis_injective line 28
theorem OAI.ContinuumCoulomb.qmaWitnessBasis_prefix line 32
theorem OAI.ContinuumCoulomb.qmaInitialState_eq_inclusion line 43
Source documentation
The initial-state definition is the concrete coordinate inclusion of the witness subspace, and therefore applies to arbitrary entangled witnesses.
```
theorem qmaInitialState_eq_inclusion (c : QMACircuit) (hc : c.WellFormed)
    (psi : EuclideanSpace ℂ (SourceSpinBasis c.witness)) :
    WithLp.toLp 2 (qmaInitialState c hc psi) = coordinateInclusion (qmaWitnessBasis c) psi := by
…
```
Mentions: OAI.ContinuumCoulomb.QMACircuit, OAI.ContinuumCoulomb.SourceSpinBasis, OAI.ContinuumCoulomb.qmaInitialState, OAI.ContinuumCoulomb.qmaWitnessBasis
theorem OAI.ContinuumCoulomb.qmaInitialState_norm line 63
theorem OAI.ContinuumCoulomb.qmaOutput_total line 70
Source documentation
The complete output distribution has exactly the witness norm squared.
```
theorem qmaOutput_total (c : QMACircuit) (hc : c.WellFormed)
    (psi : EuclideanSpace ℂ (SourceSpinBasis c.witness)) :
    (∑ s, Complex.normSq ((qmaCircuitMatrix c).mulVec (qmaInitialState c hc psi) s)) =
      ‖psi‖ ^ 2 := by
…
```
Mentions: OAI.ContinuumCoulomb.QMACircuit, OAI.ContinuumCoulomb.SourceSpinBasis, OAI.ContinuumCoulomb.qmaCircuitMatrix, OAI.ContinuumCoulomb.qmaInitialState
theorem OAI.ContinuumCoulomb.qmaAcceptance_nonneg line 84
theorem OAI.ContinuumCoulomb.qmaAcceptance_le_norm_sq line 94
theorem OAI.ContinuumCoulomb.qmaAcceptance_mem_unitInterval line 105
Source documentation
A normalized witness produces an actual probability in the unit interval.
```
theorem qmaAcceptance_mem_unitInterval (c : QMACircuit) (hc : c.WellFormed)
    (psi : EuclideanSpace ℂ (SourceSpinBasis c.witness)) (hpsi : ‖psi‖ = 1) :
    qmaAcceptance c hc psi ∈ Set.Icc (0 : ℝ) 1 := by
…
```
Mentions: OAI.ContinuumCoulomb.QMACircuit, OAI.ContinuumCoulomb.SourceSpinBasis, OAI.ContinuumCoulomb.qmaAcceptance