OAI/Probability/ParisiFinite/TerminalThird.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Terminal Third.

  1. def OAI.ParisiFinite.terminalThird line 17
  2. lemma OAI.ParisiFinite.terminal_expThird line 40
  3. lemma OAI.ParisiFinite.expThird_change_bound line 46
  4. lemma OAI.ParisiFinite.ordered_coefficient_bounds line 71
  5. def OAI.ParisiFinite.recursionThird line 83
  6. lemma OAI.ParisiFinite.recursion_expThird_bound line 87
  7. lemma OAI.ParisiFinite.recursion_d3_bound line 112
  8. lemma OAI.ParisiFinite.ordered_lower line 119
  9. lemma OAI.ParisiFinite.ordered_upper line 125
  10. lemma OAI.ParisiFinite.ordered_append line 131
  11. lemma OAI.ParisiFinite.dyadicSchedule_ordered line 138
  12. lemma OAI.ParisiFinite.dyadic_recursion_d3_bound line 151
  13. lemma OAI.ParisiFinite.recursion_curvature_lipschitz line 157
  14. lemma OAI.ParisiFinite.taylor_error_of_derivative_lipschitz line 177
  15. lemma OAI.ParisiFinite.derivative_stability_lipschitz line 194
  16. lemma OAI.ParisiFinite.exists_uniform_derivative_lipschitz_limit line 207