OAI/Probability/SKGap/Matrix/WordFockSeries.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SKGap.Noncrossing.Primary.Tensor.Series.wordOperator line 14
  2. def OAI.SKGap.Noncrossing.Primary.Tensor.Series.wordSeq line 20
  3. lemma OAI.SKGap.Noncrossing.Primary.Tensor.Series.act_comp line 24
  4. lemma OAI.SKGap.Noncrossing.Primary.Tensor.Series.act_ofVector line 27
  5. lemma OAI.SKGap.Noncrossing.Primary.Tensor.Series.wordOperator_append line 32
  6. lemma OAI.SKGap.Noncrossing.Primary.Tensor.Series.wordOperator_lift line 37
  7. lemma OAI.SKGap.Noncrossing.Primary.Tensor.Series.wordSeq_lift line 42
  8. lemma OAI.SKGap.Noncrossing.Primary.Tensor.Series.wordSeq_oneInverse line 45
  9. lemma OAI.SKGap.Noncrossing.Primary.Tensor.Series.project_kernel_sandwich line 50
  10. theorem OAI.SKGap.Noncrossing.Primary.Tensor.Series.wordSeq_project_coeff line 58
  11. def OAI.SKGap.Noncrossing.Primary.Tensor.Series.shifts line 84
  12. def OAI.SKGap.Noncrossing.Primary.Tensor.Series.letterOperator line 88
  13. lemma OAI.SKGap.Noncrossing.Primary.Tensor.Series.letter_shift line 92
  14. lemma OAI.SKGap.Noncrossing.Primary.Tensor.Series.letter_shifts line 98
  15. lemma OAI.SKGap.Noncrossing.Primary.Tensor.Series.wordSeq_cons line 103
  16. abbrev OAI.SKGap.Noncrossing.Primary.Tensor.Series.GradedWords line 106
  17. def OAI.SKGap.Noncrossing.Primary.Tensor.Series.GradedWords.scalar line 109
  18. def OAI.SKGap.Noncrossing.Primary.Tensor.Series.GradedWords.scale line 110
  19. def OAI.SKGap.Noncrossing.Primary.Tensor.Series.GradedWords.bump line 111
  20. def OAI.SKGap.Noncrossing.Primary.Tensor.Series.GradedWords.prepend line 112
  21. def OAI.SKGap.Noncrossing.Primary.Tensor.Series.GradedWords.seq line 113
  22. def OAI.SKGap.Noncrossing.Primary.Tensor.Series.GradedWords.predictionPolynomial line 116
  23. def OAI.SKGap.Noncrossing.Primary.Tensor.Series.GradedWords.prediction line 119
  24. lemma OAI.SKGap.Noncrossing.Primary.Tensor.Series.GradedWords.seq_scalar line 122
  25. lemma OAI.SKGap.Noncrossing.Primary.Tensor.Series.GradedWords.seq_append line 128
  26. lemma OAI.SKGap.Noncrossing.Primary.Tensor.Series.GradedWords.seq_scale line 130
  27. lemma OAI.SKGap.Noncrossing.Primary.Tensor.Series.GradedWords.seq_bump line 138
  28. lemma OAI.SKGap.Noncrossing.Primary.Tensor.Series.GradedWords.seq_prepend line 141
  29. lemma OAI.SKGap.Noncrossing.Primary.Tensor.Series.GradedWords.predictionPolynomial_eval line 144
  30. def OAI.SKGap.Noncrossing.Primary.Tensor.Series.projectSeries line 155
  31. lemma OAI.SKGap.Noncrossing.Primary.Tensor.Series.projectSeries_coeff line 160
  32. lemma OAI.SKGap.Noncrossing.Primary.Tensor.Series.projectSeries_shift line 163
  33. lemma OAI.SKGap.Noncrossing.Primary.Tensor.Series.projectSeries_shifts line 170
  34. lemma OAI.SKGap.Noncrossing.Primary.Tensor.Series.projectSeries_word line 175
  35. theorem OAI.SKGap.Noncrossing.Primary.Tensor.Series.GradedWords.projectSeries_eq line 182
  36. theorem OAI.SKGap.Noncrossing.Primary.Tensor.Series.GradedWords.prediction_zero_of_project line 195