OAI/Probability/SKGap/Stability/OrdinaryGraph.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.SKGap.Noncrossing.Primary.SourceTree line 14
  2. def OAI.SKGap.Noncrossing.Primary.SourceTree.leafMass line 21
  3. def OAI.SKGap.Noncrossing.Primary.SourceTree.words line 25
  4. def OAI.SKGap.Noncrossing.Primary.SourceTree.sourceOperator line 32
  5. def OAI.SKGap.Noncrossing.Primary.SourceTree.fieldOperator line 33
  6. lemma OAI.SKGap.Noncrossing.Primary.SourceTree.source_leaf line 38
  7. lemma OAI.SKGap.Noncrossing.Primary.SourceTree.field_leaf line 40
  8. lemma OAI.SKGap.Noncrossing.Primary.SourceTree.source_branch line 42
  9. lemma OAI.SKGap.Noncrossing.Primary.SourceTree.field_branch line 46
  10. theorem OAI.SKGap.Noncrossing.Primary.SourceTree.field_vacuum line 56
  11. theorem OAI.SKGap.Noncrossing.Primary.SourceTree.field_prediction_zero line 67
  12. theorem OAI.SKGap.Noncrossing.Primary.SourceTree.source_prediction line 73
  13. def OAI.SKGap.Noncrossing.Primary.SourceTree.sourceMatrix line 87
  14. def OAI.SKGap.Noncrossing.Primary.SourceTree.fieldMatrix line 89
  15. lemma OAI.SKGap.Noncrossing.Primary.SourceTree.sourceMatrix_leaf line 91
  16. lemma OAI.SKGap.Noncrossing.Primary.SourceTree.fieldMatrix_leaf line 93
  17. lemma OAI.SKGap.Noncrossing.Primary.SourceTree.sourceMatrix_branch line 96
  18. lemma OAI.SKGap.Noncrossing.Primary.SourceTree.fieldMatrix_branch line 100