OAI/Analysis/CharacterCriterion/BalancedChannels.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.KirchbergRordam.BalancedDropChannels.finalPath line 43
  2. def OAI.KirchbergRordam.BalancedDropChannels.endPath line 44
  3. lemma OAI.KirchbergRordam.BalancedDropChannels.endPath_continuous line 45
  4. lemma OAI.KirchbergRordam.BalancedDropChannels.endPath_one line 47
  5. def OAI.KirchbergRordam.BalancedDropChannels.stageLeft line 48
  6. def OAI.KirchbergRordam.BalancedDropChannels.stageRight line 52
  7. lemma OAI.KirchbergRordam.BalancedDropChannels.stage_unit_sum line 57
  8. lemma OAI.KirchbergRordam.BalancedDropChannels.norm_sub_two line 59
  9. lemma OAI.KirchbergRordam.BalancedDropChannels.map_next line 65
  10. lemma OAI.KirchbergRordam.BalancedDropChannels.stageLeft_bound line 71
  11. lemma OAI.KirchbergRordam.BalancedDropChannels.stageRight_bound line 99
  12. lemma OAI.KirchbergRordam.BalancedDropChannels.finite_stage line 146
  13. lemma OAI.KirchbergRordam.BalancedDropChannels.channel_perturbation line 178
  14. lemma OAI.KirchbergRordam.BalancedDropChannels.finite_control line 186
  15. def OAI.KirchbergRordam.MultiplicativeChannel.sequence line 207
  16. lemma OAI.KirchbergRordam.MultiplicativeChannel.sequence_apply line 215
  17. def OAI.KirchbergRordam.MultiplicativeChannel.centralize line 217
  18. lemma OAI.KirchbergRordam.MultiplicativeChannel.sequence_central line 227
  19. theorem OAI.KirchbergRordam.MultiplicativeChannel.no_central_character_of_finite_channels line 248
  20. theorem OAI.KirchbergRordam.TensorHalfFlip.injective_of_halfFlip line 289
  21. theorem OAI.KirchbergRordam.BalancedDropLimit.central_no_character line 316
  22. theorem OAI.KirchbergRordam.balanced_drop_character_criterion line 325
  23. theorem OAI.KirchbergRordam.balanced_drop_hom_injective line 340