OAI/Analysis/CharacterCriterion/PrimeChannels.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.KirchbergRordam.PrimeDropPresentation.Channels.finalPath line 45
  2. def OAI.KirchbergRordam.PrimeDropPresentation.Channels.endPath line 46
  3. lemma OAI.KirchbergRordam.PrimeDropPresentation.Channels.endPath_continuous line 47
  4. lemma OAI.KirchbergRordam.PrimeDropPresentation.Channels.endPath_one line 49
  5. def OAI.KirchbergRordam.PrimeDropPresentation.Channels.stageLeft line 50
  6. def OAI.KirchbergRordam.PrimeDropPresentation.Channels.stageRight line 54
  7. lemma OAI.KirchbergRordam.PrimeDropPresentation.Channels.stage_unit_sum line 59
  8. lemma OAI.KirchbergRordam.PrimeDropPresentation.Channels.map_next line 61
  9. lemma OAI.KirchbergRordam.PrimeDropPresentation.Channels.stageLeft_bound line 67
  10. lemma OAI.KirchbergRordam.PrimeDropPresentation.Channels.stageRight_bound line 95
  11. lemma OAI.KirchbergRordam.PrimeDropPresentation.Channels.finite_stage line 143
  12. lemma OAI.KirchbergRordam.PrimeDropPresentation.Channels.channel_perturbation line 175
  13. lemma OAI.KirchbergRordam.PrimeDropPresentation.Channels.finite_control line 183
  14. theorem OAI.KirchbergRordam.PrimeDropPresentation.central_no_character line 205
  15. theorem OAI.KirchbergRordam.PrimeDropPresentation.character_criterion line 211
  16. theorem OAI.KirchbergRordam.PrimeDropPresentation.equiv line 228
  17. theorem OAI.KirchbergRordam.PrimeDropPresentation.equiv_balanced line 234
  18. theorem OAI.KirchbergRordam.PrimeDropPresentation.hom_injective line 241