OAI/Analysis/RotationWeights/Discrepancy.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CircleSampling.negLower line 34
  2. def OAI.CircleSampling.negUpper line 35
  3. lemma OAI.CircleSampling.neg_support_strict line 38
  4. def OAI.CircleSampling.negArcLeft line 51
  5. def OAI.CircleSampling.negArcRight line 53
  6. lemma OAI.CircleSampling.negative_superlevel_intervals line 56
  7. lemma OAI.CircleSampling.negArcs_sub_Ioo line 108
  8. lemma OAI.CircleSampling.negArcs_disjoint line 118
  9. lemma OAI.CircleSampling.preimage_repr_interval line 126
  10. lemma OAI.CircleSampling.repr_ne_ae line 137
  11. lemma OAI.CircleSampling.uNeg_superlevel_ae line 145
  12. lemma OAI.CircleSampling.interval_image_ball line 157
  13. def OAI.CircleSampling.IsTwoArcs line 189
  14. lemma OAI.CircleSampling.uNeg_isTwoArcs line 194
  15. lemma OAI.CircleSampling.uPos_isTwoArcs line 217
  16. lemma OAI.CircleSampling.prod_eventuallyEq_of_marginals line 251
  17. lemma OAI.CircleSampling.disjoint_prod_of_left line 262
  18. lemma OAI.CircleSampling.disjoint_prod_of_right line 265
  19. lemma OAI.CircleSampling.measureReal_two_unions line 269
  20. lemma OAI.CircleSampling.twoArcs_rectangle_discrepancy line 278
  21. lemma OAI.CircleSampling.boundedLayercake line 308
  22. lemma OAI.CircleSampling.boundedLayercake_weighted line 324
  23. lemma OAI.CircleSampling.boundedLayercake_product line 365
  24. lemma OAI.CircleSampling.integrable_superlevel_measure line 389
  25. lemma OAI.CircleSampling.superlevel_discrepancy line 404