OAI/Analysis/RotationWeights/CrossingEstimates.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CircleCoupling.digit_below_threshold line 81
  2. lemma OAI.CircleCoupling.digit_above_threshold line 92
  3. lemma OAI.CircleCoupling.top_forces_above line 102
  4. lemma OAI.CircleCoupling.bottom_forces_below line 113
  5. abbrev OAI.CircleCoupling.LabelledDigits line 124
  6. def OAI.CircleCoupling.selectedBelow line 125
  7. def OAI.CircleCoupling.selectedAbove line 128
  8. lemma OAI.CircleCoupling.crossing_top_domination line 132
  9. lemma OAI.CircleCoupling.crossing_bottom_domination line 171
  10. lemma OAI.CircleCoupling.measurable_selectedBelow_card line 210
  11. def OAI.CircleCoupling.noCross line 223
  12. lemma OAI.CircleCoupling.measurableSet_noCross line 226
  13. lemma OAI.CircleCoupling.selected_card_sum line 236
  14. lemma OAI.CircleCoupling.crossing_split line 257
  15. lemma OAI.CircleCoupling.conditional_crossing_estimates line 289
  16. def OAI.CircleCoupling.CoordinateParameters.width line 362
  17. def OAI.CircleCoupling.CoordinateParameters.prob line 363
  18. def OAI.CircleCoupling.CoordinateParameters.topLabel line 364
  19. def OAI.CircleCoupling.CoordinateParameters.bottomLabel line 365
  20. lemma OAI.CircleCoupling.CoordinateParameters.width_pos line 366
  21. lemma OAI.CircleCoupling.CoordinateParameters.width_round line 367
  22. lemma OAI.CircleCoupling.CoordinateParameters.prob_nonneg line 371
  23. lemma OAI.CircleCoupling.CoordinateParameters.prob_le_one line 372
  24. lemma OAI.CircleCoupling.CoordinateParameters.top_failure line 373
  25. lemma OAI.CircleCoupling.CoordinateParameters.bottom_failure line 380
  26. lemma OAI.CircleCoupling.CoordinateParameters.top_support line 387
  27. lemma OAI.CircleCoupling.CoordinateParameters.bottom_support line 399
  28. def OAI.CircleCoupling.DigitSystem.crossingWidth line 413
  29. def OAI.CircleCoupling.DigitSystem.crossingDigit line 414
  30. def OAI.CircleCoupling.DigitSystem.supported line 415
  31. lemma OAI.CircleCoupling.DigitSystem.measurableSet_supported line 418
  32. lemma OAI.CircleCoupling.DigitSystem.ae_supported line 423
  33. lemma OAI.CircleCoupling.DigitSystem.actual_crossing_estimates line 439