OAI/Analysis/CoulombIonization/Fermionic/Basis.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CoulombPauli.tensor_add_left line 17
  2. lemma OAI.CoulombPauli.tensor_smul_left line 26
  3. def OAI.CoulombPauli.tensorRight line 34
  4. lemma OAI.CoulombPauli.tensorRight_apply line 44
  5. lemma OAI.CoulombPauli.tensor_adjoint_exchange line 46
  6. lemma OAI.CoulombPauli.hilbertBasis_inner_eq_zero line 53
  7. lemma OAI.CoulombPauli.tensor_orthonormal line 62
  8. lemma OAI.CoulombPauli.tensor_basis_total line 73
  9. def OAI.CoulombPauli.tensorBasis line 95
  10. lemma OAI.CoulombPauli.tensorBasis_apply line 99
  11. lemma OAI.CoulombPauli.basis_parseval line 105
  12. lemma OAI.CoulombPauli.tensorRight_parseval line 117
  13. lemma OAI.CoulombPauli.hilbertBasis_countable line 136
  14. def OAI.CoulombPackets.windowed line 162
  15. lemma OAI.CoulombPackets.windowed_apply line 166
  16. lemma OAI.CoulombPackets.norm_windowed line 175
  17. lemma OAI.CoulombPackets.integrable_shift_product line 179
  18. lemma OAI.CoulombPackets.integrated_plancherel line 193
  19. def OAI.CoulombPackets.frameFunction line 203
  20. lemma OAI.CoulombPackets.frameFunction_stronglyMeasurable line 206
  21. lemma OAI.CoulombPackets.frameFunction_memLp line 219
  22. lemma OAI.CoulombPackets.l2_norm_sq line 235
  23. lemma OAI.CoulombPackets.frame_norm_sq line 244
  24. def OAI.CoulombPackets.frameLinear line 263
  25. lemma OAI.CoulombPackets.frameLinear_norm line 284
  26. def OAI.CoulombPackets.frame line 290
  27. lemma OAI.CoulombPackets.frame_toLp line 294
  28. lemma OAI.CoulombPackets.frame_norm line 300
  29. def OAI.CoulombPackets.frameIsometry line 309