OAI/Analysis/IrrationalRotation/Rotation/DiagonalGauge.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Invariant233.DiagonalGauge.weight_apply line 13
  2. theorem OAI.Invariant233.DiagonalGauge.fiberOperator_apply line 15
  3. theorem OAI.Invariant233.DiagonalGauge.norm_weight_le line 18
  4. theorem OAI.Invariant233.DiagonalGauge.norm_fiberOperator_le line 23
  5. theorem OAI.Invariant233.DiagonalGauge.continuous_fiberOperator_apply line 27
  6. theorem OAI.Invariant233.DiagonalGauge.fiberOperator_zero line 36
  7. theorem OAI.Invariant233.DiagonalGauge.fiberOperator_add line 40
  8. theorem OAI.Invariant233.DiagonalGauge.fiberOperator_mul_neg line 47
  9. theorem OAI.Invariant233.DiagonalGauge.fiberOperator_neg_mul line 51
  10. theorem OAI.Invariant233.DiagonalGauge.norm_fiberOperator_apply line 55
  11. def OAI.Invariant233.DiagonalGauge.fiberEquiv line 66
  12. theorem OAI.Invariant233.DiagonalGauge.fiberOperator_mem_unitary line 75
  13. theorem OAI.Invariant233.DiagonalGauge.fiberOperator_adjoint line 79
  14. theorem OAI.Invariant233.DiagonalGauge.fieldOperator_ae line 92
  15. theorem OAI.Invariant233.DiagonalGauge.norm_fieldOperator_le line 96
  16. theorem OAI.Invariant233.DiagonalGauge.fieldOperator_zero line 99
  17. theorem OAI.Invariant233.DiagonalGauge.fieldOperator_add line 106
  18. theorem OAI.Invariant233.DiagonalGauge.fieldOperator_mul_neg line 118
  19. theorem OAI.Invariant233.DiagonalGauge.fieldOperator_neg_mul line 122
  20. theorem OAI.Invariant233.DiagonalGauge.norm_fieldOperator_apply line 126
  21. def OAI.Invariant233.DiagonalGauge.fieldEquiv line 138
  22. theorem OAI.Invariant233.DiagonalGauge.fieldOperator_mem_unitary line 149
  23. theorem OAI.Invariant233.DiagonalGauge.fieldOperator_adjoint line 153
  24. theorem OAI.Invariant233.DiagonalGauge.continuous_fieldOperator_apply line 166
  25. theorem OAI.Invariant233.DiagonalGauge.continuous_conjugate_apply line 186
  26. theorem OAI.Invariant233.DiagonalGauge.norm_conjugate_le line 195
  27. theorem OAI.Invariant233.DiagonalGauge.conjugate_zero line 210