OAI/Analysis/IrrationalRotation/Operators/ProjectionMeetTrace.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Invariant233.ProjectionMeetTrace.vectorFunctional line 15
  2. theorem OAI.Invariant233.ProjectionMeetTrace.vectorFunctional_apply line 19
  3. theorem OAI.Invariant233.ProjectionMeetTrace.norm_one_sub_gram_le_one line 22
  4. theorem OAI.Invariant233.ProjectionMeetTrace.mul_complement_pow line 35
  5. theorem OAI.Invariant233.ProjectionMeetTrace.vectorTrace_complement_pow_eq line 43
  6. def OAI.Invariant233.ProjectionMeetTrace.meanOperator line 60
  7. theorem OAI.Invariant233.ProjectionMeetTrace.meanOperator_apply line 65
  8. theorem OAI.Invariant233.ProjectionMeetTrace.eqLocus_one_sub_gram line 74
  9. theorem OAI.Invariant233.ProjectionMeetTrace.meanOperator_one_sub_gram_tendsto line 81
  10. theorem OAI.Invariant233.ProjectionMeetTrace.vectorTrace_kernel_eq_adjoint_kernel line 91
  11. instance OAI.Invariant233.ProjectionMeetTrace.inf_complete line 124
  12. theorem OAI.Invariant233.ProjectionMeetTrace.projection_mul_of_le line 132
  13. theorem OAI.Invariant233.ProjectionMeetTrace.kernel_projection_complement_mul line 138
  14. theorem OAI.Invariant233.ProjectionMeetTrace.meet_projection_mem line 178
  15. theorem OAI.Invariant233.ProjectionMeetTrace.norm_projection_le_one line 195
  16. theorem OAI.Invariant233.ProjectionMeetTrace.vectorTrace_meet_lower_bound line 201
  17. theorem OAI.Invariant233.ProjectionMeetTrace.faithful_vectorTrace_meet_lower_bound line 243