OAI/Analysis/LaughlinGap/Averaging.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

Averaging.

  1. def OAI.LaughlinGap.Averaging.coordinates line 15
  2. lemma OAI.LaughlinGap.Averaging.coordinates_inner line 24
  3. def OAI.LaughlinGap.Averaging.invariantSpace line 38
  4. def OAI.LaughlinGap.Averaging.average line 42
  5. lemma OAI.LaughlinGap.Averaging.average_mem line 47
  6. lemma OAI.LaughlinGap.Averaging.average_orthogonal line 57
  7. lemma OAI.LaughlinGap.Averaging.average_unique line 65
  8. lemma OAI.LaughlinGap.Averaging.average_eq_self line 79
  9. lemma OAI.LaughlinGap.Averaging.average_transpose line 84
  10. lemma OAI.LaughlinGap.Averaging.average_isHermitian line 99
  11. lemma OAI.LaughlinGap.Averaging.trace_mul_average line 105
  12. lemma OAI.LaughlinGap.Averaging.trace_mul_posSemidef line 113
  13. lemma OAI.LaughlinGap.Averaging.cfc_mem line 128
  14. lemma OAI.LaughlinGap.Averaging.trace_mul_cfc line 134
  15. lemma OAI.LaughlinGap.Averaging.cfc_nonnegative line 145
  16. theorem OAI.LaughlinGap.Averaging.average_positive line 151
  17. lemma OAI.LaughlinGap.Averaging.average_trace line 175
  18. def OAI.LaughlinGap.Averaging.adjointMap line 182
  19. lemma OAI.LaughlinGap.Averaging.adjointMap_inner line 189
  20. theorem OAI.LaughlinGap.Averaging.average_natural line 196
  21. def OAI.LaughlinGap.Averaging.commutator line 205
  22. lemma OAI.LaughlinGap.Averaging.commutator_adjoint line 211
  23. def OAI.LaughlinGap.Averaging.rotationCommutant line 219
  24. lemma OAI.LaughlinGap.Averaging.rotationCommutant_mem line 222
  25. lemma OAI.LaughlinGap.Averaging.coordinates_eq_zero_of_inner line 230
  26. lemma OAI.LaughlinGap.Averaging.commutator_intertwines_adjoint line 236
  27. lemma OAI.LaughlinGap.Averaging.map_rotationCommutant line 253
  28. theorem OAI.LaughlinGap.Averaging.rotation_average_natural line 264