OAI/InformationTheory/Entanglement/IndependentTapes.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SecretKey.UniformTapes line 10
  2. def OAI.SecretKey.uniformTapesLaw line 11
  3. instance OAI.SecretKey.(instance at line 12) line 12
  4. def OAI.SecretKey.tapeInformation line 14
  5. lemma OAI.SecretKey.tapeInformation_le line 16
  6. lemma OAI.SecretKey.tapeInformation_mono line 18
  7. lemma OAI.SecretKey.tapeInformation_union line 20
  8. lemma OAI.SecretKey.independent_tape_groups line 27
  9. lemma OAI.SecretKey.tape_coordinate_law line 31
  10. lemma OAI.SecretKey.fresh_coordinate_independent line 33
  11. lemma OAI.SecretKey.initial_conditional_independence line 43
  12. theorem OAI.SecretKey.initial_uniform_tape_independence line 53