OAI/Computability/MinUncut/Estimates/OuterRemainder.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MinUncut.Outer.actual_remainder_fourth line 15
  2. structure OAI.MinUncut.Outer.LocalRows line 46
  3. def OAI.MinUncut.Outer.LocalRows.lists line 53
  4. def OAI.MinUncut.Outer.LocalRows.atom line 57
  5. def OAI.MinUncut.Outer.LocalRows.distance line 61
  6. def OAI.MinUncut.Outer.LocalRows.fourth line 66
  7. lemma OAI.MinUncut.Outer.LocalRows.card_first line 71
  8. lemma OAI.MinUncut.Outer.LocalRows.card_second line 78
  9. lemma OAI.MinUncut.Outer.LocalRows.mean_fourth line 84
  10. theorem OAI.MinUncut.Outer.LocalRows.atom_bound line 97
  11. lemma OAI.MinUncut.integrable_expect line 126
  12. lemma OAI.MinUncut.Outer.backgroundMean_integrable line 138
  13. lemma OAI.MinUncut.Outer.integral_backgroundMean line 145