OAI/Analysis/AffineBernstein/SmoothPositivePart.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.AffineBernstein.smoothTransition_reflect line 13
  2. def OAI.AffineBernstein.smoothPositiveSlope line 23
  3. def OAI.AffineBernstein.smoothPositivePart line 25
  4. lemma OAI.AffineBernstein.smoothPositiveSlope_smooth line 27
  5. lemma OAI.AffineBernstein.smoothPositivePart_hasDeriv line 31
  6. lemma OAI.AffineBernstein.smoothPositivePart_smooth line 37
  7. lemma OAI.AffineBernstein.smoothPositivePart_deriv_bounds line 45
  8. lemma OAI.AffineBernstein.smoothPositiveSlope_monotone line 50
  9. lemma OAI.AffineBernstein.smoothPositivePart_second_nonneg line 56
  10. lemma OAI.AffineBernstein.smoothPositiveSlope_zero line 62
  11. lemma OAI.AffineBernstein.smoothPositiveSlope_one line 67
  12. lemma OAI.AffineBernstein.smoothPositiveSlope_reflect line 73
  13. lemma OAI.AffineBernstein.smoothPositivePart_zero line 79
  14. lemma OAI.AffineBernstein.smoothPositivePart_at_right line 90
  15. lemma OAI.AffineBernstein.smoothPositivePart_identity line 105