OAI/InformationTheory/QuantumCircuit/ProductState.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Product input states and their excitation counts.

  1. def OAI.QAC.pureProjector line 13
  2. structure OAI.QAC.ProductInput line 16
  3. lemma OAI.QAC.act_pureProjector line 23
  4. lemma OAI.QAC.act_smul_state line 41
  5. lemma OAI.QAC.inner_act_right line 44
  6. lemma OAI.QAC.projection_inner_self line 50
  7. lemma OAI.QAC.conjugated_product_projection_action line 59
  8. theorem OAI.QAC.uniform_product_overlap_tail line 66
  9. theorem OAI.QAC.product_overlap_tail line 85