OAI/Computability/MinUncut/Estimates/ActualBoxBound.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MinUncut.Inner.actual_zero_box_bound line 25
  2. theorem OAI.MinUncut.Inner.actual_zero_box_average line 39
  3. def OAI.MinUncut.Inner.firstFailure line 62
  4. def OAI.MinUncut.Inner.firstRejection line 66
  5. lemma OAI.MinUncut.Inner.firstFailure_eq line 71
  6. lemma OAI.MinUncut.Inner.measurable_smooth line 78
  7. lemma OAI.MinUncut.Inner.smooth_abs_le line 85
  8. lemma OAI.MinUncut.Inner.firstRejection_eq line 92
  9. lemma OAI.MinUncut.Inner.measurable_firstRejection line 111
  10. lemma OAI.MinUncut.Inner.firstRejection_range line 121
  11. lemma OAI.MinUncut.Inner.smooth_energy_first line 127
  12. theorem OAI.MinUncut.Inner.gradient_energy_first line 134