OAI/Probability/SKGap/Matrix/LoopPrediction.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SKGap.Noncrossing.Primary.Tensor.Loop.blockDegree_reverse line 14
  2. def OAI.SKGap.Noncrossing.Primary.Tensor.Loop.blockReverse line 16
  3. def OAI.SKGap.Noncrossing.Primary.Tensor.Loop.blockPrepend line 22
  4. lemma OAI.SKGap.Noncrossing.Primary.Tensor.Loop.blockPrepend_bijective line 25
  5. def OAI.SKGap.Noncrossing.Primary.Tensor.Loop.blockSnocEquiv line 42
  6. lemma OAI.SKGap.Noncrossing.Primary.Tensor.Loop.blockSnocEquiv_inl line 45
  7. lemma OAI.SKGap.Noncrossing.Primary.Tensor.Loop.blockSnocEquiv_inr line 49
  8. lemma OAI.SKGap.Noncrossing.Primary.Tensor.Loop.sum_blocks_snoc line 54
  9. lemma OAI.SKGap.Noncrossing.Primary.Tensor.Loop.blocks_one line 62
  10. instance OAI.SKGap.Noncrossing.Primary.Tensor.Loop.blocksOneUnique line 65
  11. def OAI.SKGap.Noncrossing.Primary.Tensor.Loop.kernel line 69
  12. lemma OAI.SKGap.Noncrossing.Primary.Tensor.Loop.kernel_zero line 71
  13. lemma OAI.SKGap.Noncrossing.Primary.Tensor.Loop.kernel_one line 73
  14. lemma OAI.SKGap.Noncrossing.Primary.Tensor.Loop.kernel_add_two line 75
  15. lemma OAI.SKGap.Noncrossing.Primary.Tensor.Loop.project_kernel_zero_creation line 85
  16. lemma OAI.SKGap.Noncrossing.Primary.Tensor.Loop.project_kernel_creation line 89
  17. lemma OAI.SKGap.Noncrossing.Primary.Tensor.Loop.project_kernel_incoming line 105