OAI/Analysis/RotationWeights/ConditionalBounds.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CircleCoupling.measure_le_of_singletons line 77
  2. lemma OAI.CircleCoupling.map_restrict_le_of_fibers line 86
  3. lemma OAI.CircleCoupling.independent_fiber_failures line 98
  4. lemma OAI.CircleCoupling.independent_selected_failures line 130
  5. lemma OAI.CircleCoupling.full_tail_domination line 168
  6. lemma OAI.CircleCoupling.map_domination line 200
  7. lemma OAI.CircleCoupling.selected_failures_endpoint line 206
  8. lemma OAI.CircleCoupling.failure_power_exponential line 235
  9. lemma OAI.CircleCoupling.infinitePi_split line 252
  10. def OAI.CircleCoupling.glue line 289
  11. lemma OAI.CircleCoupling.measurable_glue line 293
  12. lemma OAI.CircleCoupling.map_glue line 300
  13. lemma OAI.CircleCoupling.observe_glue line 315
  14. lemma OAI.CircleCoupling.infinite_selected_failures line 324
  15. lemma OAI.CircleDigits.digit_interval_weak line 380
  16. lemma OAI.CircleDigits.measurable_prefixNumeral line 387
  17. lemma OAI.CircleDigits.measurable_scaledTail line 393