OAI/Probability/SKGap/Terminal/TerminalRates.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SKGap.nat_pow_exp_neg_tendsto line 13
  2. lemma OAI.SKGap.nat_pow_exp_sqrt_tendsto line 24
  3. def OAI.SKGap.terminalEntryScale line 35
  4. lemma OAI.SKGap.terminalEntryScale_nonneg line 37
  5. lemma OAI.SKGap.terminalEntryScale_tendsto line 39
  6. lemma OAI.SKGap.terminalEntryScale_sq line 44
  7. lemma OAI.SKGap.terminalEntryScale_rate line 48
  8. def OAI.SKGap.terminalRowBound line 64
  9. def OAI.SKGap.terminalRawGood line 66
  10. def OAI.SKGap.terminalRawTail line 77
  11. lemma OAI.SKGap.terminalRaw_bad_bound line 86
  12. def OAI.SKGap.terminalMatrixBound line 150
  13. def OAI.SKGap.terminalMatrixData line 152
  14. lemma OAI.SKGap.terminalMatrixData_of_raw line 159
  15. lemma OAI.SKGap.terminalMatrixData_forms line 213