OAI/Geometry/UnitDistances/Integration.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PlanarUnitDistances.TailWindows.tail line 11
  2. lemma OAI.PlanarUnitDistances.TailWindows.tail_antitone line 12
  3. lemma OAI.PlanarUnitDistances.TailWindows.below_all line 15
  4. lemma OAI.PlanarUnitDistances.TailWindows.above_all line 19
  5. lemma OAI.PlanarUnitDistances.TailWindows.step line 24
  6. lemma OAI.PlanarUnitDistances.TailWindows.nonempty_type line 47
  7. lemma OAI.PlanarUnitDistances.TailWindows.least_threshold line 53
  8. theorem OAI.PlanarUnitDistances.TailWindows.window line 70
  9. lemma OAI.PlanarUnitDistances.StarWindow.common_window line 92
  10. lemma OAI.PlanarUnitDistances.StarWindow.central_window line 96
  11. theorem OAI.PlanarUnitDistances.StarWindow.exists_joint_window line 104
  12. lemma OAI.PlanarUnitDistances.StarWindow.tail_eq line 114
  13. theorem OAI.PlanarUnitDistances.StarWindow.mean_excess line 116
  14. def OAI.PlanarUnitDistances.WindowVariation.variation line 156
  15. lemma OAI.PlanarUnitDistances.WindowVariation.variation_nonneg line 159
  16. lemma OAI.PlanarUnitDistances.WindowVariation.central_lower line 166
  17. lemma OAI.PlanarUnitDistances.WindowVariation.window_le_variation line 181
  18. lemma OAI.PlanarUnitDistances.WindowVariation.excess_le_variation line 194
  19. lemma OAI.PlanarUnitDistances.FiniteLawIntegral.measurable_avg line 212
  20. lemma OAI.PlanarUnitDistances.FiniteLawIntegral.integrable_avg line 216
  21. lemma OAI.PlanarUnitDistances.FiniteLawIntegral.integral_avg line 220
  22. lemma OAI.PlanarUnitDistances.FiniteLawIntegral.avg_sum line 227
  23. lemma OAI.PlanarUnitDistances.FiniteLawIntegral.avg_div line 232
  24. lemma OAI.PlanarUnitDistances.FiniteLawIntegral.avg_mono_support line 236
  25. lemma OAI.PlanarUnitDistances.FiniteLawIntegral.avg_indicator_mul line 244
  26. def OAI.PlanarUnitDistances.ExpectedBudget.pairScore line 261
  27. def OAI.PlanarUnitDistances.ExpectedBudget.excess line 265
  28. lemma OAI.PlanarUnitDistances.ExpectedBudget.excess_nonneg line 273
  29. theorem OAI.PlanarUnitDistances.ExpectedBudget.star_upper line 276
  30. def OAI.PlanarUnitDistances.SlotIntegration.truncatedPositive line 342
  31. lemma OAI.PlanarUnitDistances.SlotIntegration.positive_integrable line 350
  32. lemma OAI.PlanarUnitDistances.SlotIntegration.piece_score line 357
  33. lemma OAI.PlanarUnitDistances.SlotIntegration.score_eq_pairScore line 376
  34. lemma OAI.PlanarUnitDistances.TailVariation.tail_measurable line 409
  35. lemma OAI.PlanarUnitDistances.TailVariation.variation_measurable line 412
  36. lemma OAI.PlanarUnitDistances.TailVariation.variation_bounds line 418
  37. lemma OAI.PlanarUnitDistances.TailVariation.variation_off line 424
  38. lemma OAI.PlanarUnitDistances.TailVariation.variation_integrable line 437
  39. lemma OAI.PlanarUnitDistances.TailVariation.variation_integral line 452
  40. lemma OAI.PlanarUnitDistances.ActualBudget.snapshot_frequency line 472
  41. lemma OAI.PlanarUnitDistances.ActualBudget.snapshot_conditional line 478
  42. theorem OAI.PlanarUnitDistances.ActualBudget.star_upper line 484
  43. def OAI.PlanarUnitDistances.ActualBudgetIntegral.commonVariation line 554
  44. lemma OAI.PlanarUnitDistances.ActualBudgetIntegral.variation_integral line 558
  45. theorem OAI.PlanarUnitDistances.ActualBudgetIntegral.upper line 591
  46. theorem OAI.PlanarUnitDistances.ActualFamilyBudget.upper line 621
  47. theorem OAI.PlanarUnitDistances.ActualRowBudget.raw line 668
  48. theorem OAI.PlanarUnitDistances.ActualRowBudget.compressed_upper line 702