OAI/Combinatorics/SharpRamsey/Learning/TestLearningRowBase.lean

GitHub source file

54 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SharpLogRamsey.PoissonSchedules.scheduleLaw line 13
  2. instance OAI.SharpLogRamsey.PoissonSchedules.schedule_probability line 16
  3. theorem OAI.SharpLogRamsey.PoissonSchedules.coordinate_independence line 20
  4. def OAI.SharpLogRamsey.PoissonSchedules.hitLedger line 24
  5. def OAI.SharpLogRamsey.PoissonSchedules.emptyLedger line 26
  6. theorem OAI.SharpLogRamsey.PoissonSchedules.measurable_hitLedger line 28
  7. theorem OAI.SharpLogRamsey.PoissonSchedules.measurable_emptyLedger line 31
  8. theorem OAI.SharpLogRamsey.PoissonSchedules.poisson_zero_real line 34
  9. theorem OAI.SharpLogRamsey.PoissonSchedules.poisson_nonzero_real line 37
  10. theorem OAI.SharpLogRamsey.PoissonSchedules.hitLedger_probability line 42
  11. theorem OAI.SharpLogRamsey.PoissonSchedules.emptyLedger_probability line 51
  12. theorem OAI.SharpLogRamsey.PoissonSchedules.hitLedger_le_mean_product line 60
  13. theorem OAI.SharpLogRamsey.PoissonSchedules.static_certificate_bound line 71
  14. def OAI.SharpLogRamsey.EmptyExceptional.emptySum line 92
  15. def OAI.SharpLogRamsey.EmptyExceptional.emptySet line 95
  16. lemma OAI.SharpLogRamsey.EmptyExceptional.emptySum_eq line 98
  17. lemma OAI.SharpLogRamsey.EmptyExceptional.emptySum_one line 102
  18. lemma OAI.SharpLogRamsey.EmptyExceptional.emptySum_nonneg line 106
  19. lemma OAI.SharpLogRamsey.EmptyExceptional.emptySum_le_sum line 114
  20. lemma OAI.SharpLogRamsey.EmptyExceptional.integrable_emptySum line 124
  21. lemma OAI.SharpLogRamsey.EmptyExceptional.integral_emptySum line 130
  22. theorem OAI.SharpLogRamsey.EmptyExceptional.many_empty line 143
  23. theorem OAI.SharpLogRamsey.EmptyExceptional.heavy_empty_expectation line 158
  24. lemma OAI.SharpLogRamsey.EmptyExceptional.empty_weight_split line 181
  25. lemma OAI.SharpLogRamsey.EmptyExceptional.emptySum_mono line 203
  26. theorem OAI.SharpLogRamsey.EmptyExceptional.empty_good_event line 212
  27. def OAI.SharpLogRamsey.LearningRow.test line 255
  28. lemma OAI.SharpLogRamsey.LearningRow.capture_score line 258
  29. lemma OAI.SharpLogRamsey.LearningRow.exclude_score line 274
  30. theorem OAI.SharpLogRamsey.LearningRow.capture_count line 292
  31. theorem OAI.SharpLogRamsey.LearningRow.ambient_count line 316
  32. def OAI.SharpLogRamsey.LearningRow.failures line 349
  33. lemma OAI.SharpLogRamsey.LearningRow.eventCount_eq_card line 352
  34. theorem OAI.SharpLogRamsey.LearningRow.row_success_probability line 357
  35. lemma OAI.SharpLogRamsey.PoissonTail.weighted_power_hasSum line 443
  36. lemma OAI.SharpLogRamsey.PoissonTail.integrable_power line 455
  37. lemma OAI.SharpLogRamsey.PoissonTail.integral_power line 460
  38. theorem OAI.SharpLogRamsey.PoissonTail.double_mean_tail line 465
  39. theorem OAI.SharpLogRamsey.PoissonTail.total_tail line 492
  40. def OAI.SharpLogRamsey.ExceptionalScore.empty line 514
  41. def OAI.SharpLogRamsey.ExceptionalScore.term line 516
  42. def OAI.SharpLogRamsey.ExceptionalScore.fullyEmpty line 519
  43. lemma OAI.SharpLogRamsey.ExceptionalScore.empty_mono line 522
  44. lemma OAI.SharpLogRamsey.ExceptionalScore.factor_abs_le line 526
  45. lemma OAI.SharpLogRamsey.ExceptionalScore.term_empty line 531
  46. lemma OAI.SharpLogRamsey.ExceptionalScore.term_hit line 536
  47. lemma OAI.SharpLogRamsey.ExceptionalScore.fullyEmpty_decomposition line 565
  48. theorem OAI.SharpLogRamsey.ExceptionalScore.exceptional_error line 579
  49. def OAI.SharpLogRamsey.PreparedMass.count line 614
  50. def OAI.SharpLogRamsey.PreparedMass.outside line 616
  51. lemma OAI.SharpLogRamsey.PreparedMass.count_split line 618
  52. lemma OAI.SharpLogRamsey.PreparedMass.normalized_split line 656
  53. theorem OAI.SharpLogRamsey.PreparedMass.typical_range line 664
  54. theorem OAI.SharpLogRamsey.PreparedMass.typical_square_sum line 673