OAI/InformationTheory/Entanglement/ActualDefaults.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SecretKey.PositiveHilbertMeasure.value_eq_zero_of_trace_null line 16
2. lemma OAI.SecretKey.PositiveHilbertMeasure.coeff_eq_zero_of_trace_null line 23
3. lemma OAI.SecretKey.PositiveHilbertMeasure.value_eq_of_ae_set line 28
4. lemma OAI.SecretKey.PositiveHilbertMeasure.mapRecord_value_congr_ae line 49
5. theorem OAI.SecretKey.actual_completion_removes_defaults line 60