OAI/Analysis/IrrationalRotation/Operators/NormalTracialTransport.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Invariant233.NormalTracialTransport.extendedTrace line 15
  2. theorem OAI.Invariant233.NormalTracialTransport.extendedTrace_apply line 20
  3. theorem OAI.Invariant233.NormalTracialTransport.extendedTrace_one line 26
  4. theorem OAI.Invariant233.NormalTracialTransport.extendedTrace_cyclic line 31
  5. theorem OAI.Invariant233.NormalTracialTransport.extendedTrace_star line 38
  6. theorem OAI.Invariant233.NormalTracialTransport.extendedTrace_projection_nonneg line 44
  7. theorem OAI.Invariant233.NormalTracialTransport.extendedTrace_projection_real line 53
  8. theorem OAI.Invariant233.NormalTracialTransport.extendedTrace_tendsto line 60
  9. theorem OAI.Invariant233.NormalTracialTransport.extendedTrace_projection_mono line 72
  10. theorem OAI.Invariant233.NormalTracialTransport.extendedTrace_orthogonal line 83
  11. theorem OAI.Invariant233.NormalTracialTransport.extendedTrace_complement_pow_eq line 91
  12. theorem OAI.Invariant233.NormalTracialTransport.meanOperator_mem line 105
  13. theorem OAI.Invariant233.NormalTracialTransport.norm_meanOperator_le_one line 109
  14. theorem OAI.Invariant233.NormalTracialTransport.extendedTrace_tendsto_nat line 135
  15. theorem OAI.Invariant233.NormalTracialTransport.extendedTrace_kernel_eq_adjoint_kernel_of_norm_le_one line 154
  16. theorem OAI.Invariant233.NormalTracialTransport.extendedTrace_kernel_eq_adjoint_kernel line 192
  17. theorem OAI.Invariant233.NormalTracialTransport.range_closure_projection_mem line 222
  18. theorem OAI.Invariant233.NormalTracialTransport.extendedTrace_range_eq_of_injective line 229
  19. theorem OAI.Invariant233.NormalTracialTransport.extendedTrace_preimage_eq line 247
  20. theorem OAI.Invariant233.NormalTracialTransport.extendedTrace_le_of_normalizer line 268
  21. theorem OAI.Invariant233.NormalTracialTransport.extendedTrace_transported_eq_of_normalizer line 302
  22. theorem OAI.Invariant233.NormalTracialTransport.transported_trace_eq_of_normalizer line 349