OAI/InformationTheory/Entanglement/CausalPublic.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SecretKey.snoc_information line 11
  2. lemma OAI.SecretKey.causalPublic_succ line 38
  3. lemma OAI.SecretKey.causalPublicInfo_succ line 45
  4. lemma OAI.SecretKey.causalPublicInfo_succ_of_private line 50
  5. lemma OAI.SecretKey.causalOutcome_local line 63
  6. lemma OAI.SecretKey.causalPublic_succ_local line 72
  7. lemma OAI.SecretKey.source_view_eq_public line 80
  8. lemma OAI.SecretKey.causal_source_step line 88