OAI/Probability/SKGap/Matrix/FockTensor.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SKGap.Noncrossing.Primary.Tensor.Space line 13
  2. def OAI.SKGap.Noncrossing.Primary.Tensor.tensorValue line 15
  3. def OAI.SKGap.Noncrossing.Primary.Tensor.realize line 20
  4. lemma OAI.SKGap.Noncrossing.Primary.Tensor.realize_ket line 23
  5. def OAI.SKGap.Noncrossing.Primary.Tensor.diagonal line 26
  6. def OAI.SKGap.Noncrossing.Primary.Tensor.creation line 30
  7. def OAI.SKGap.Noncrossing.Primary.Tensor.annihilation line 34
  8. def OAI.SKGap.Noncrossing.Primary.Tensor.noise line 38
  9. def OAI.SKGap.Noncrossing.Primary.Tensor.project line 39
  10. def OAI.SKGap.Noncrossing.Primary.Tensor.vacuum line 44
  11. def OAI.SKGap.Noncrossing.Primary.Tensor.letter line 46
  12. def OAI.SKGap.Noncrossing.Primary.Tensor.word line 49
  13. lemma OAI.SKGap.Noncrossing.Primary.Tensor.realize_diagonal line 54
  14. lemma OAI.SKGap.Noncrossing.Primary.Tensor.realize_creation line 66
  15. lemma OAI.SKGap.Noncrossing.Primary.Tensor.realize_annihilation line 76
  16. lemma OAI.SKGap.Noncrossing.Primary.Tensor.realize_noise line 85
  17. lemma OAI.SKGap.Noncrossing.Primary.Tensor.project_realize line 89
  18. lemma OAI.SKGap.Noncrossing.Primary.Tensor.realize_word line 97
  19. lemma OAI.SKGap.Noncrossing.Primary.Tensor.diagram_map_id line 104
  20. lemma OAI.SKGap.Noncrossing.Primary.Tensor.project_word line 106
  21. lemma OAI.SKGap.Noncrossing.Primary.Tensor.word_append line 110
  22. lemma OAI.SKGap.Noncrossing.Primary.Tensor.diagonal_scale line 116
  23. lemma OAI.SKGap.Noncrossing.Primary.Tensor.annihilation_diagonal_creation line 120
  24. lemma OAI.SKGap.Noncrossing.Primary.Tensor.project_diagonal_creation line 125
  25. lemma OAI.SKGap.Noncrossing.Primary.Tensor.project_creation line 128