OAI/InformationTheory/Entanglement/ScalarGap.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SecretKey.sqrt_memLp_two line 10
2. lemma OAI.SecretKey.sqrt_product_integrable line 14
3. lemma OAI.SecretKey.integral_sqrt_product_le line 18
4. lemma OAI.SecretKey.two_sqrt_products_le line 31
5. lemma OAI.SecretKey.two_sqrt_le_add line 39
6. theorem OAI.SecretKey.scalar_secret_bit_gap line 44