OAI/Geometry/UnitDistances/Tails.lean

GitHub source file

54 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PlanarUnitDistances.IncidenceCoercivity.errorCoefficient line 18
  2. theorem OAI.PlanarUnitDistances.IncidenceCoercivity.bounds line 23
  3. theorem OAI.PlanarUnitDistances.IncidenceCoercivity.error_limit line 48
  4. lemma OAI.PlanarUnitDistances.IncidenceCoercivity.leading_joint line 70
  5. def OAI.PlanarUnitDistances.IncidenceRare.Ready line 96
  6. theorem OAI.PlanarUnitDistances.IncidenceRare.prepare line 102
  7. def OAI.PlanarUnitDistances.IncidenceHeights.Z line 170
  8. lemma OAI.PlanarUnitDistances.IncidenceHeights.Z_nonneg line 171
  9. theorem OAI.PlanarUnitDistances.IncidenceHeights.averages line 173
  10. lemma OAI.PlanarUnitDistances.IncidenceHeights.row_support line 203
  11. theorem OAI.PlanarUnitDistances.IncidenceHeights.pointwise line 209
  12. theorem OAI.PlanarUnitDistances.IncidenceHeights.baseline line 220
  13. def OAI.PlanarUnitDistances.TailControl.layer line 239
  14. lemma OAI.PlanarUnitDistances.TailControl.layer_apply line 241
  15. lemma OAI.PlanarUnitDistances.TailControl.layer_integrable line 245
  16. lemma OAI.PlanarUnitDistances.TailControl.integral_layer line 249
  17. lemma OAI.PlanarUnitDistances.TailControl.layer_min line 254
  18. lemma OAI.PlanarUnitDistances.TailControl.layer_nonneg line 258
  19. def OAI.PlanarUnitDistances.TailControl.mass line 261
  20. def OAI.PlanarUnitDistances.TailControl.tails line 266
  21. lemma OAI.PlanarUnitDistances.TailControl.tails_integrable line 268
  22. lemma OAI.PlanarUnitDistances.TailControl.integral_tails line 271
  23. lemma OAI.PlanarUnitDistances.TailControl.tails_nonneg line 277
  24. lemma OAI.PlanarUnitDistances.TailControl.tails_eq_mass line 280
  25. lemma OAI.PlanarUnitDistances.TailControl.tails_eq_zero line 288
  26. def OAI.PlanarUnitDistances.TailControl.pairTails line 291
  27. lemma OAI.PlanarUnitDistances.TailControl.pairTails_integrable line 294
  28. lemma OAI.PlanarUnitDistances.TailControl.integral_pairTails line 299
  29. lemma OAI.PlanarUnitDistances.TailControl.pairTails_eq_rectangle line 310
  30. lemma OAI.PlanarUnitDistances.TailControl.pairTails_eq_zero line 325
  31. lemma OAI.PlanarUnitDistances.TailControl.layer_young line 329
  32. theorem OAI.PlanarUnitDistances.TailControl.capped_expectation line 335
  33. lemma OAI.PlanarUnitDistances.TailControl.average_distinct line 366
  34. def OAI.PlanarUnitDistances.TailControl.capped line 405
  35. theorem OAI.PlanarUnitDistances.TailControl.finite_tail_bound line 409
  36. lemma OAI.PlanarUnitDistances.LawTail.capped_pointwise line 464
  37. theorem OAI.PlanarUnitDistances.LawTail.estimate line 478
  38. def OAI.PlanarUnitDistances.AccurateBand.kept line 534
  39. lemma OAI.PlanarUnitDistances.AccurateBand.weighted_kept line 537
  40. lemma OAI.PlanarUnitDistances.AccurateBand.kept_probability line 559
  41. lemma OAI.PlanarUnitDistances.AccurateBand.dyadic_cover line 570
  42. lemma OAI.PlanarUnitDistances.AccurateBand.exists_cover_piece line 586
  43. theorem OAI.PlanarUnitDistances.AccurateBand.select line 611
  44. lemma OAI.PlanarUnitDistances.RareBand.pair_tail line 650
  45. lemma OAI.PlanarUnitDistances.RareBand.wedge_tail line 653
  46. theorem OAI.PlanarUnitDistances.RareBand.select line 661
  47. def OAI.PlanarUnitDistances.TailParameters.coefficient line 694
  48. lemma OAI.PlanarUnitDistances.TailParameters.noise_limit line 695
  49. lemma OAI.PlanarUnitDistances.TailParameters.radius_limit line 698
  50. lemma OAI.PlanarUnitDistances.TailParameters.exists_radius line 704
  51. lemma OAI.PlanarUnitDistances.TailParameters.exists_band line 710
  52. def OAI.PlanarUnitDistances.IncidenceBand.band line 728
  53. lemma OAI.PlanarUnitDistances.IncidenceBand.tail line 733
  54. theorem OAI.PlanarUnitDistances.IncidenceBand.choose line 772