OAI/Analysis/Pureness/States/RegularizedStateTraceIdentification.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.CuntzPureness.normalizedStateCauchyValue_add_iff_original line 15
2. theorem OAI.CuntzPureness.regularizedState_agreeing_trace_iff_original_additive line 61
3. theorem OAI.CuntzPureness.regularizedState_agreeing_trace_of_extreme_additivity line 72