OAI/InformationTheory/QuantumCircuit/Trajectory.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

Excitation tails and regular trajectories of shallow quantum circuits.

  1. abbrev OAI.QAC.State line 14
  2. def OAI.QAC.act line 16
  3. lemma OAI.QAC.act_mul line 19
  4. lemma OAI.QAC.act_one line 23
  5. lemma OAI.QAC.act_zero line 26
  6. lemma OAI.QAC.act_add line 29
  7. lemma OAI.QAC.act_sub line 32
  8. lemma OAI.QAC.act_norm_le line 35
  9. lemma OAI.QAC.act_norm_le_of_contraction line 38
  10. lemma OAI.QAC.act_unitary_norm line 42
  11. lemma OAI.QAC.projection_action_tail_bound line 52
  12. def OAI.QAC.HasExcitationTails line 69
  13. theorem OAI.QAC.excitation_tail_transport line 75
  14. inductive OAI.QAC.AnalyticLayer line 105
  15. def OAI.QAC.AnalyticLayer.matrix line 111
  16. lemma OAI.QAC.AnalyticLayer.isCircuit line 115
  17. def OAI.QAC.evolution line 125
  18. lemma OAI.QAC.evolution_append line 129
  19. lemma OAI.QAC.evolution_isCircuit line 135
  20. def OAI.QAC.jointTest line 141
  21. def OAI.QAC.RegularTrajectory line 145
  22. def OAI.QAC.projectedInput line 153
  23. lemma OAI.QAC.projectedInput_at_cut line 156
  24. theorem OAI.QAC.regular_projection_insertion line 172