OAI/InformationTheory/Entanglement/InstrumentCovariance.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SecretKey.PositiveMatrixMeasure.eq_of_value line 14
2. lemma OAI.SecretKey.CPOutcomeLaw.ref_sandwich_entry line 28
3. theorem OAI.SecretKey.CPOutcomeLaw.reference_filter line 38
4. theorem OAI.SecretKey.CPOutcomeLaw.reference_pure line 49