OAI/Analysis/RotationWeights/TaggedEvents.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CircleCoupling.independent_one_tag_bound line 81
  2. lemma OAI.CircleCoupling.log_one_sub_lower line 129
  3. lemma OAI.CircleCoupling.one_tag_survival line 138
  4. lemma OAI.CircleCoupling.count_fin_lower line 157
  5. lemma OAI.CircleCoupling.finite_fiber_mass line 170
  6. lemma OAI.CircleCoupling.finite_lower_fiber_mass line 181
  7. def OAI.CircleCoupling.CoordinateParameters.tagEvent line 193
  8. def OAI.CircleCoupling.CoordinateParameters.marginEvent line 194
  9. def OAI.CircleCoupling.CoordinateParameters.untaggedMargin line 196
  10. lemma OAI.CircleCoupling.CoordinateParameters.law_tag_mass line 198
  11. lemma OAI.CircleCoupling.CoordinateParameters.tag_forces_margin line 201
  12. lemma OAI.CircleCoupling.CoordinateParameters.law_lower_digit line 231
  13. lemma OAI.CircleCoupling.CoordinateParameters.law_upper_digit line 240
  14. lemma OAI.CircleCoupling.CoordinateParameters.law_untagged_margin_mass line 265
  15. def OAI.CircleCoupling.DigitSystem.coordinateTag line 299
  16. def OAI.CircleCoupling.DigitSystem.coordinateMargin line 303
  17. def OAI.CircleCoupling.DigitSystem.coordinateUntaggedMargin line 307
  18. lemma OAI.CircleCoupling.DigitSystem.measurableSet_coordinateTag line 310
  19. lemma OAI.CircleCoupling.DigitSystem.measurableSet_coordinateMargin line 312
  20. lemma OAI.CircleCoupling.DigitSystem.measurableSet_coordinateUntaggedMargin line 314
  21. def OAI.CircleCoupling.DigitSystem.oneTagEvent line 317
  22. lemma OAI.CircleCoupling.DigitSystem.measurableSet_oneTagEvent line 319
  23. lemma OAI.CircleCoupling.DigitSystem.oneTagEvent_mass line 327
  24. lemma OAI.CircleCoupling.DigitSystem.oneTagEvent_margins line 358
  25. def OAI.CircleSampling.blockCoordinates line 378
  26. lemma OAI.CircleSampling.blockCoordinates_card line 379
  27. lemma OAI.CircleSampling.blockCoordinates_zero line 384
  28. lemma OAI.CircleSampling.blockCoordinates_block line 385
  29. def OAI.CircleSampling.stageTagEvent line 389
  30. lemma OAI.CircleSampling.stageTagEvent_measurable line 390
  31. lemma OAI.CircleSampling.stageTagEvent_mass line 391
  32. lemma OAI.CircleSampling.stageTagEvent_margins line 400