OAI/Analysis/IrrationalRotation/Operators/NormalTracialProjectionTransport.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Invariant233.TracialState.apply_selfAdjoint_eq_re line 15
2. theorem OAI.Invariant233.TracialState.projection_nonneg line 21
3. theorem OAI.Invariant233.TracialState.projection_mono line 26
4. theorem OAI.Invariant233.TracialState.projection_re_mem_Icc line 34
5. theorem OAI.Invariant233.NormalTracialProjectionTransport.tendsto_trace_projection_exhaustion line 48
6. theorem OAI.Invariant233.NormalTracialProjectionTransport.tendsto_trace_projection_exhaustion_re line 63
7. theorem OAI.Invariant233.NormalTracialProjectionTransport.trace_eq_of_cutoff_estimates line 75