OAI/Analysis/CharacterCriterion/MultiplicativeChannels.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.KirchbergRordam.MultiplicativeChannel.Channel line 41
  2. instance OAI.KirchbergRordam.MultiplicativeChannel.(instance at line 46) line 46
  3. lemma OAI.KirchbergRordam.MultiplicativeChannel.map_zero line 47
  4. lemma OAI.KirchbergRordam.MultiplicativeChannel.map_add line 48
  5. lemma OAI.KirchbergRordam.MultiplicativeChannel.map_smul line 49
  6. lemma OAI.KirchbergRordam.MultiplicativeChannel.norm_map_le line 50
  7. lemma OAI.KirchbergRordam.MultiplicativeChannel.mul_eq line 51
  8. def OAI.KirchbergRordam.MultiplicativeChannel.postcompose line 53
  9. def OAI.KirchbergRordam.MultiplicativeChannel.normalized line 59
  10. lemma OAI.KirchbergRordam.MultiplicativeChannel.no_character_of_pair line 70
  11. def OAI.KirchbergRordam.MultiplicativeChannel.weighted line 81
  12. def OAI.KirchbergRordam.MultiplicativeChannel.restrictDrop line 100
  13. def OAI.KirchbergRordam.DropChannels.conjugated line 116
  14. def OAI.KirchbergRordam.DropChannels.leftScalar line 129
  15. def OAI.KirchbergRordam.DropChannels.rightScalar line 131
  16. lemma OAI.KirchbergRordam.DropChannels.leftScalar_zero line 133
  17. lemma OAI.KirchbergRordam.DropChannels.leftScalar_one line 134
  18. lemma OAI.KirchbergRordam.DropChannels.rightScalar_zero line 135
  19. lemma OAI.KirchbergRordam.DropChannels.rightScalar_one line 136
  20. lemma OAI.KirchbergRordam.DropChannels.leftScalar_norm line 137
  21. lemma OAI.KirchbergRordam.DropChannels.rightScalar_norm line 141
  22. def OAI.KirchbergRordam.DropChannels.left line 147
  23. def OAI.KirchbergRordam.DropChannels.right line 158
  24. lemma OAI.KirchbergRordam.DropChannels.left_apply line 169
  25. lemma OAI.KirchbergRordam.DropChannels.right_apply line 171
  26. lemma OAI.KirchbergRordam.DropChannels.unit_sum line 173
  27. lemma OAI.KirchbergRordam.DropChannels.norm_conjugate_commutator line 187
  28. lemma OAI.KirchbergRordam.DropChannels.norm_commutator_change line 191
  29. lemma OAI.KirchbergRordam.DropChannels.smul_commutator line 201
  30. lemma OAI.KirchbergRordam.DropChannels.commutator_map_bound line 210
  31. lemma OAI.KirchbergRordam.DropChannels.norm_sub_conj line 214
  32. lemma OAI.KirchbergRordam.DropChannels.norm_twisted_difference line 217
  33. lemma OAI.KirchbergRordam.DropChannels.transport_bound line 224
  34. lemma OAI.KirchbergRordam.BalancedDropChannels.zeroCount line 241
  35. lemma OAI.KirchbergRordam.BalancedDropChannels.oneCount line 245
  36. def OAI.KirchbergRordam.BalancedDropChannels.zeroRep line 249
  37. def OAI.KirchbergRordam.BalancedDropChannels.oneRep line 253
  38. lemma OAI.KirchbergRordam.BalancedDropChannels.zeroRep_bound line 257
  39. lemma OAI.KirchbergRordam.BalancedDropChannels.oneRep_bound line 274