OAI/Combinatorics/MatchingCount/Probability/FinitePMF.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MatchingFPRAS.Concentration.hoeffding_mean line 14
  2. theorem OAI.MatchingFPRAS.Concentration.hoeffding_observables line 59
  3. def OAI.MatchingFPRAS.Concentration.finitePMF line 85
  4. lemma OAI.MatchingFPRAS.Concentration.finitePMF_apply line 90
  5. theorem OAI.MatchingFPRAS.Concentration.finite_hoeffding line 93
  6. lemma OAI.MatchingFPRAS.Concentration.observables_exp_tail line 133
  7. lemma OAI.MatchingFPRAS.Concentration.stage_hoeffding_budget line 163
  8. def OAI.MatchingFPRAS.Concentration.trials line 171
  9. lemma OAI.MatchingFPRAS.Concentration.median_tail line 173
  10. lemma OAI.MatchingFPRAS.Enlargement.logicalActivity_le_off line 206
  11. lemma OAI.MatchingFPRAS.Enlargement.bagReweight_range_off line 214
  12. lemma OAI.MatchingFPRAS.Enlargement.observableD_range_off line 230
  13. lemma OAI.MatchingFPRAS.Enlargement.observableProbe_range_off line 241
  14. abbrev OAI.MatchingFPRAS.Enlargement.ObservableIndex line 252
  15. def OAI.MatchingFPRAS.Enlargement.sourceObservable line 254
  16. lemma OAI.MatchingFPRAS.Enlargement.sourceObservable_range line 259
  17. lemma OAI.MatchingFPRAS.Enlargement.observableIndex_card line 272
  18. def OAI.MatchingFPRAS.Enlargement.sampleAverage line 278
  19. def OAI.MatchingFPRAS.Enlargement.sourceMean line 281
  20. def OAI.MatchingFPRAS.Enlargement.StageGood line 284
  21. theorem OAI.MatchingFPRAS.Enlargement.source_ideal_concentration line 287
  22. def OAI.MatchingFPRAS.Enlargement.empiricalData line 312
  23. lemma OAI.MatchingFPRAS.Enlargement.StageData.sigma_pos line 321
  24. def OAI.MatchingFPRAS.Enlargement.stageSampleCount line 328
  25. lemma OAI.MatchingFPRAS.Enlargement.StageData.sampleCount_pos line 331
  26. lemma OAI.MatchingFPRAS.Enlargement.StageData.sampleCount_bound line 338
  27. theorem OAI.MatchingFPRAS.Enlargement.source_ideal_budget line 349
  28. theorem OAI.MatchingFPRAS.Enlargement.source_nearby_budget line 373
  29. theorem OAI.MatchingFPRAS.Enlargement.source_run_stage_budget line 405