OAI/Probability/SKGap/Stability/OrdinaryRecipe.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.SKGapCutoff.Recipe.OrdinaryData line 14
  2. def OAI.SKGapCutoff.Recipe.OrdinaryData.seedCoefficient line 29
  3. def OAI.SKGapCutoff.Recipe.OrdinaryData.auxCoefficient line 30
  4. def OAI.SKGapCutoff.Recipe.OrdinaryData.seedPartial line 31
  5. def OAI.SKGapCutoff.Recipe.OrdinaryData.auxPartial line 32
  6. def OAI.SKGapCutoff.Recipe.OrdinaryData.sourceOf line 34
  7. def OAI.SKGapCutoff.Recipe.OrdinaryData.partialOf line 37
  8. def OAI.SKGapCutoff.Recipe.OrdinaryData.fieldOf line 40
  9. def OAI.SKGapCutoff.Recipe.OrdinaryData.evaluate line 45
  10. def OAI.SKGapCutoff.Recipe.OrdinaryData.source line 50
  11. def OAI.SKGapCutoff.Recipe.OrdinaryData.auxiliary line 51
  12. def OAI.SKGapCutoff.Recipe.OrdinaryData.sourcePartial line 52
  13. lemma OAI.SKGapCutoff.Recipe.OrdinaryData.source_eq line 54
  14. lemma OAI.SKGapCutoff.Recipe.OrdinaryData.auxiliary_eq line 56
  15. structure OAI.SKGapCutoff.Recipe.CoefficientBound line 61
  16. lemma OAI.SKGapCutoff.Recipe.CoefficientBound.small_product line 67
  17. lemma OAI.SKGapCutoff.Recipe.CoefficientBound.mean_product line 72
  18. lemma OAI.SKGapCutoff.Recipe.OrdinaryData.sourceOf_bound line 80
  19. lemma OAI.SKGapCutoff.Recipe.OrdinaryData.partialOf_bound line 90
  20. lemma OAI.SKGapCutoff.Recipe.OrdinaryData.fieldOf_bound line 100