OAI/Probability/SKGap/Localization/RecipeMarked.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SKGap.Noncrossing.Primary.MarkedPolynomial.diagonalWords line 15
  2. def OAI.SKGap.Noncrossing.Primary.MarkedPolynomial.averageWords line 17
  3. def OAI.SKGap.Noncrossing.Primary.MarkedPolynomial.mass line 19
  4. lemma OAI.SKGap.Noncrossing.Primary.MarkedPolynomial.plain_diagonalWords line 21
  5. lemma OAI.SKGap.Noncrossing.Primary.MarkedPolynomial.plain_averageWords line 24
  6. lemma OAI.SKGap.Noncrossing.Primary.MarkedPolynomial.budget_diagonalWords line 28
  7. lemma OAI.SKGap.Noncrossing.Primary.MarkedPolynomial.budget_averageWords line 35
  8. abbrev OAI.SKGap.Noncrossing.Primary.MarkedPolynomial.Pair line 43
  9. def OAI.SKGap.Noncrossing.Primary.MarkedPolynomial.pairPlain line 45
  10. def OAI.SKGap.Noncrossing.Primary.MarkedPolynomial.zeroPair line 47
  11. lemma OAI.SKGap.Noncrossing.Primary.MarkedPolynomial.zeroPair_plain line 48
  12. def OAI.SKGap.Noncrossing.Primary.MarkedPolynomial.smallBranch line 51
  13. def OAI.SKGap.Noncrossing.Primary.MarkedPolynomial.boundedBranch line 55
  14. lemma OAI.SKGap.Noncrossing.Primary.MarkedPolynomial.smallBranch_plain line 59
  15. lemma OAI.SKGap.Noncrossing.Primary.MarkedPolynomial.boundedBranch_plain line 68
  16. lemma OAI.SKGap.Noncrossing.Primary.MarkedPolynomial.fold_plain line 77
  17. def OAI.SKGapCutoff.Recipe.OrdinaryData.markedRecipe line 90
  18. theorem OAI.SKGapCutoff.Recipe.OrdinaryData.markedRecipe_plain line 97