OAI/Probability/SKGap/Matrix/ClosedTreeMatrix.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SKGap.Noncrossing.Primary.Tensor.Series.ClosedTree.ofOrdinary line 14
  2. lemma OAI.SKGap.Noncrossing.Primary.Tensor.Series.ClosedTree.words_ofOrdinary line 18
  3. def OAI.SKGap.Noncrossing.Primary.Tensor.Series.ClosedTree.sourceMatrix line 24
  4. def OAI.SKGap.Noncrossing.Primary.Tensor.Series.ClosedTree.fieldMatrix line 26
  5. lemma OAI.SKGap.Noncrossing.Primary.Tensor.Series.ClosedTree.sourceMatrix_ofOrdinary line 28
  6. lemma OAI.SKGap.Noncrossing.Primary.Tensor.Series.ClosedTree.fieldMatrix_ofOrdinary line 32
  7. lemma OAI.SKGap.Noncrossing.Primary.Tensor.Series.ClosedTree.sourceMatrix_leaf line 36
  8. lemma OAI.SKGap.Noncrossing.Primary.Tensor.Series.ClosedTree.fieldMatrix_leaf line 39
  9. lemma OAI.SKGap.Noncrossing.Primary.Tensor.Series.ClosedTree.sourceMatrix_branch line 43
  10. lemma OAI.SKGap.Noncrossing.Primary.Tensor.Series.ClosedTree.fieldMatrix_branch line 48
  11. def OAI.SKGap.Noncrossing.Primary.Tensor.Series.ClosedTree.branches line 56
  12. lemma OAI.SKGap.Noncrossing.Primary.Tensor.Series.ClosedTree.branches_leafMass line 59
  13. lemma OAI.SKGap.Noncrossing.Primary.Tensor.Series.ClosedTree.branches_source line 63
  14. lemma OAI.SKGap.Noncrossing.Primary.Tensor.Series.ClosedTree.branches_field line 72