OAI/InformationTheory/AmplitudeDamping/SequentialMatrices.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.GAD.projectionAction line 13
  2. theorem OAI.GAD.projectionAction_frob line 17
  3. theorem OAI.GAD.projectionAction_orthogonal line 21
  4. theorem OAI.GAD.matrix_sequential_union_bound line 27
  5. def OAI.GAD.rejectProduct line 35
  6. theorem OAI.GAD.rejectProduct_loss line 39
  7. theorem OAI.GAD.rejectProduct_sum line 51
  8. theorem OAI.GAD.sequential_projector_success line 58
  9. theorem OAI.GAD.mass_triangle_sq line 91
  10. theorem OAI.GAD.projected_self_failure line 96