OAI/Probability/ClassicalON/SmoothBounds.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.ClassicalON.compact_continuous_norm_bound line 16
  2. theorem OAI.ClassicalON.smooth_compact_lipschitz_bound line 21
  3. theorem OAI.ClassicalON.scalar_lipschitz_of_deriv_bound line 35
  4. theorem OAI.ClassicalON.abs_sub_left_le_of_uIcc line 42
  5. theorem OAI.ClassicalON.first_remainder_bound line 52
  6. theorem OAI.ClassicalON.second_remainder_bound line 69
  7. theorem OAI.ClassicalON.trapezoid_error_bound line 89