OAI/Analysis/GroupDeterminants/LampCoefficients.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LampProjectionDraft.baseEmbedding line 16
  2. lemma OAI.LampProjectionDraft.baseEmbedding_injective line 19
  3. lemma OAI.LampProjectionDraft.baseEmbedding_coeff_one line 22
  4. def OAI.LampProjectionDraft.fullLampSymbol line 27
  5. def OAI.LampProjectionDraft.shiftSymbol line 29
  6. lemma OAI.LampProjectionDraft.shiftSymbol_one_lamp line 31
  7. def OAI.LampProjectionDraft.projection line 38
  8. def OAI.LampProjectionDraft.average line 41
  9. lemma OAI.LampProjectionDraft.average_def line 43
  10. lemma OAI.LampProjectionDraft.projection_idempotent line 51
  11. lemma OAI.LampProjectionDraft.projection_selfAdjoint line 54
  12. lemma OAI.LampProjectionDraft.projection_trace line 60
  13. lemma OAI.LampProjectionDraft.baseAverage_one_mul_projection line 64
  14. lemma OAI.LampProjectionDraft.baseProjection_mul_average_eq_zero line 68
  15. lemma OAI.LampProjectionDraft.shift_average line 79
  16. lemma OAI.LampProjectionDraft.projection_separates line 90
  17. def OAI.LampProjectionDraft.baseSum line 104
  18. def OAI.LampProjectionDraft.baseNumerator line 107
  19. def OAI.LampProjectionDraft.denominator line 110
  20. def OAI.LampProjectionDraft.numerator line 112
  21. def OAI.LampProjectionDraft.intToRat line 115
  22. lemma OAI.LampProjectionDraft.intToRat_baseSum line 118
  23. lemma OAI.LampProjectionDraft.intToRat_baseNumerator line 121
  24. lemma OAI.LampProjectionDraft.denominator_pos line 131
  25. lemma OAI.LampProjectionDraft.denominator_odd line 134