OAI/InformationTheory/Entanglement/ConditionalUpdate.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SecretKey.setIntegral_eq_on_generated line 11
  2. def OAI.SecretKey.joinTests line 31
  3. lemma OAI.SecretKey.joinTests_pi line 33
  4. lemma OAI.SecretKey.joinTests_generate line 39
  5. lemma OAI.SecretKey.indicator_one_mul line 55
  6. lemma OAI.SecretKey.integrable_indicator_one line 59
  7. theorem OAI.SecretKey.conditional_marginal_join line 63
  8. lemma OAI.SecretKey.conditional_inter_pullout line 98
  9. lemma OAI.SecretKey.independence_of_local_marginals line 110
  10. theorem OAI.SecretKey.sender_message_preserves_independence line 131
  11. theorem OAI.SecretKey.public_source_preserves_independence line 147
  12. theorem OAI.SecretKey.conditional_independence_adjoin_public line 163
  13. lemma OAI.SecretKey.independent_of_public_conditional_laws line 174