OAI/InformationTheory/Entanglement/WeakStateSupport.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SecretKey.densityDiag line 11
2. lemma OAI.SecretKey.densityDiag_nonneg line 14
3. lemma OAI.SecretKey.densityDiag_summable line 17
4. lemma OAI.SecretKey.densityDiag_sum line 20
5. lemma OAI.SecretKey.positive_re_inner_zero line 24
6. lemma OAI.SecretKey.density_subtype_diag_le line 32
7. lemma OAI.SecretKey.density_kills_outside line 38
8. theorem OAI.SecretKey.weak_density_countable_support line 51