OAI/Analysis/BackwardIntertwiners/ConvexEnvelope.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BackwardIntertwiners.DiscreteConvex line 12
  2. lemma OAI.BackwardIntertwiners.DiscreteConvex.of_step line 19
  3. lemma OAI.BackwardIntertwiners.DiscreteConvex.step line 23
  4. lemma OAI.BackwardIntertwiners.DiscreteConvex.sub_zero_le line 27
  5. lemma OAI.BackwardIntertwiners.DiscreteConvex.secant_le line 37
  6. lemma OAI.BackwardIntertwiners.DiscreteConvex.le_endpoint line 51
  7. lemma OAI.BackwardIntertwiners.DiscreteConvex.bump line 66
  8. def OAI.BackwardIntertwiners.convexMinorants line 91
  9. def OAI.BackwardIntertwiners.convexEnvelope line 95
  10. lemma OAI.BackwardIntertwiners.ConvexEnvelope.bddAbove line 105
  11. lemma OAI.BackwardIntertwiners.ConvexEnvelope.le_envelope line 114
  12. lemma OAI.BackwardIntertwiners.ConvexEnvelope.zero line 119
  13. lemma OAI.BackwardIntertwiners.ConvexEnvelope.convex line 128
  14. lemma OAI.BackwardIntertwiners.ConvexEnvelope.below line 142
  15. lemma OAI.BackwardIntertwiners.ConvexEnvelope.mem line 148
  16. lemma OAI.BackwardIntertwiners.ConvexEnvelope.contact line 153
  17. lemma OAI.BackwardIntertwiners.DiscreteConvex.slopes_tendsto line 197
  18. lemma OAI.BackwardIntertwiners.quadratic_upper_of_curvature line 218
  19. lemma OAI.BackwardIntertwiners.large_curvature line 244
  20. lemma OAI.BackwardIntertwiners.DiscreteConvex.increment_mono line 280
  21. lemma OAI.BackwardIntertwiners.DiscreteConvex.increment_lower line 291
  22. lemma OAI.BackwardIntertwiners.DiscreteConvex.increment_upper line 302
  23. lemma OAI.BackwardIntertwiners.DiscreteConvex.summable_exp_neg_slope line 314
  24. def OAI.BackwardIntertwiners.normalizedTailTerm line 332
  25. lemma OAI.BackwardIntertwiners.DiscreteConvex.tail_term_bound line 339
  26. lemma OAI.BackwardIntertwiners.DiscreteConvex.tail_term_tendsto line 349
  27. lemma OAI.BackwardIntertwiners.DiscreteConvex.tail_summable line 367
  28. lemma OAI.BackwardIntertwiners.DiscreteConvex.tail_tsum_tendsto line 378