OAI/InformationTheory/DimensionTen/ChoiTransfer.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Transpose-adjoint transfer for the explicit dimension-ten maps.

  1. lemma OAI.DimensionTen.operational_matrixUnit line 15
  2. def OAI.DimensionTen.phiOneSharp line 20
  3. def OAI.DimensionTen.phiTwoLinear line 23
  4. lemma OAI.DimensionTen.phiOneSharp_single line 25
  5. lemma OAI.DimensionTen.phiOneSharp_apply line 32
  6. lemma OAI.DimensionTen.phiOneSharp_input_transpose line 39
  7. lemma OAI.DimensionTen.hsAdjoint_input_transpose line 51
  8. lemma OAI.DimensionTen.phiTwo_input_transpose line 65
  9. lemma OAI.DimensionTen.phiOneSharp_pptType line 70
  10. lemma OAI.DimensionTen.phiTwo_pptType line 81
  11. lemma OAI.DimensionTen.compositeChoi_transfer line 95