OAI/Probability/SKGap/Localization/GraphPrediction.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SKGap.Noncrossing.Primary.annihilation_diagonal_creation line 14
  2. lemma OAI.SKGap.Noncrossing.Primary.project_diagonal_creation line 26
  3. lemma OAI.SKGap.Noncrossing.Primary.project_creation line 38
  4. def OAI.SKGap.Noncrossing.Primary.Graph.sumWords line 50
  5. lemma OAI.SKGap.Noncrossing.Primary.Graph.polynomialOperator_sumWords line 53
  6. lemma OAI.SKGap.Noncrossing.Primary.Graph.matrixPolynomial_sumWords line 57
  7. abbrev OAI.SKGap.Noncrossing.Primary.Graph.Partials line 61
  8. def OAI.SKGap.Noncrossing.Primary.Graph.sourceWords line 63
  9. def OAI.SKGap.Noncrossing.Primary.Graph.fieldWords line 66
  10. def OAI.SKGap.Noncrossing.Primary.Graph.coefficients line 71
  11. def OAI.SKGap.Noncrossing.Primary.Graph.sourceOp line 81
  12. def OAI.SKGap.Noncrossing.Primary.Graph.fieldOp line 83
  13. lemma OAI.SKGap.Noncrossing.Primary.Graph.sourceOp_zero line 86
  14. lemma OAI.SKGap.Noncrossing.Primary.Graph.fieldOp_zero line 89
  15. lemma OAI.SKGap.Noncrossing.Primary.Graph.fieldOp_one line 91
  16. lemma OAI.SKGap.Noncrossing.Primary.Graph.sourceOp_succ line 96
  17. lemma OAI.SKGap.Noncrossing.Primary.Graph.fieldOp_add_two line 100
  18. theorem OAI.SKGap.Noncrossing.Primary.Graph.field_vacuum line 110
  19. theorem OAI.SKGap.Noncrossing.Primary.Graph.field_prediction_zero line 127
  20. theorem OAI.SKGap.Noncrossing.Primary.Graph.source_prediction_zero line 136