OAI/InformationTheory/Entanglement/CorrelationBound.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ProjectionCriterion.symmetric_trace_square line 11
2. lemma OAI.ProjectionCriterion.trace_square_lower line 21
3. theorem OAI.ProjectionCriterion.correlation_lower line 34