OAI/Combinatorics/SharpRamsey/Learning/TestPointTail.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SharpLogRamsey.PoissonGrouping.law line 14
  2. instance OAI.SharpLogRamsey.PoissonGrouping.probability line 17
  3. lemma OAI.SharpLogRamsey.PoissonGrouping.sum_hasLaw line 21
  4. def OAI.SharpLogRamsey.PoissonGrouping.regroup line 49
  5. lemma OAI.SharpLogRamsey.PoissonGrouping.regroup_hasLaw line 52
  6. def OAI.SharpLogRamsey.PoissonGrouping.groupedCount line 80
  7. theorem OAI.SharpLogRamsey.PoissonGrouping.groupedCount_hasLaw line 83
  8. lemma OAI.SharpLogRamsey.PoissonGrouping.groupedCount_eq_zero line 102
  9. lemma OAI.SharpLogRamsey.PoissonGrouping.grouped_empty_iff line 108
  10. theorem OAI.SharpLogRamsey.PoissonGrouping.grouped_moment line 117
  11. def OAI.SharpLogRamsey.PointScore.pointEmpty line 133
  12. def OAI.SharpLogRamsey.PointScore.pointScore line 136
  13. def OAI.SharpLogRamsey.PointScore.held line 141
  14. def OAI.SharpLogRamsey.PointScore.outsideGroup line 143
  15. def OAI.SharpLogRamsey.PointScore.ownBit line 147
  16. lemma OAI.SharpLogRamsey.PointScore.grouped_empty line 152
  17. lemma OAI.SharpLogRamsey.PointScore.source_score_eq_grouped line 171
  18. theorem OAI.SharpLogRamsey.BoundedProbability.mass_above_half line 217
  19. theorem OAI.SharpLogRamsey.BoundedProbability.real_markov line 239
  20. lemma OAI.SharpLogRamsey.BoundedProbability.good_minus_bad line 252
  21. theorem OAI.SharpLogRamsey.BoundedProbability.product_event_le line 271
  22. theorem OAI.SharpLogRamsey.BoundedProbability.even_moment_tail line 282
  23. def OAI.SharpLogRamsey.BoundedProbability.eventCount line 302
  24. lemma OAI.SharpLogRamsey.BoundedProbability.eventCount_nonneg line 306
  25. lemma OAI.SharpLogRamsey.BoundedProbability.integrable_eventCount line 309
  26. lemma OAI.SharpLogRamsey.BoundedProbability.integral_eventCount line 316
  27. theorem OAI.SharpLogRamsey.BoundedProbability.eventCount_tail line 327
  28. theorem OAI.SharpLogRamsey.PoissonConditioning.own_outside_tail line 355
  29. lemma OAI.SharpLogRamsey.PointScore.centeredFactor_abs line 401
  30. lemma OAI.SharpLogRamsey.PointScore.radial_score_abs line 411
  31. lemma OAI.SharpLogRamsey.PointScore.integrable_radial_power line 433
  32. theorem OAI.SharpLogRamsey.PointScore.point_score_tail line 444
  33. def OAI.SharpLogRamsey.PreparedProjectiveGeometry.direction line 492
  34. lemma OAI.SharpLogRamsey.PreparedProjectiveGeometry.direction_eq_iff line 496
  35. lemma OAI.SharpLogRamsey.PreparedProjectiveGeometry.direction_mem_lines line 506
  36. theorem OAI.SharpLogRamsey.PreparedProjectiveGeometry.direction_fiber_card line 515
  37. def OAI.SharpLogRamsey.PointScore.outsideBatchFiber line 541
  38. lemma OAI.SharpLogRamsey.PointScore.outside_uniform_rate line 554
  39. def OAI.SharpLogRamsey.PreparedProjectiveGeometry.outsideDirection line 573
  40. def OAI.SharpLogRamsey.PreparedProjectiveGeometry.outsideDirectionFiber line 577
  41. lemma OAI.SharpLogRamsey.PreparedProjectiveGeometry.outsideDirection_card line 595
  42. lemma OAI.SharpLogRamsey.PreparedProjectiveGeometry.outsideDirection_incidence line 601
  43. theorem OAI.SharpLogRamsey.PreparedProjectiveGeometry.actual_radial_rate line 609