OAI/Analysis/RotationWeights/DigitCouplings.lean

GitHub source file

51 declarations, 0 contain sorry, 0 declared as axioms

  1. instance OAI.CircleCoupling.labelMeasurableSpace line 67
  2. instance OAI.CircleCoupling.labelMeasurableSingleton line 68
  3. def OAI.CircleCoupling.uniformOn line 70
  4. instance OAI.CircleCoupling.(instance at line 72) line 72
  5. lemma OAI.CircleCoupling.uniformOn_singleton line 75
  6. def OAI.CircleCoupling.labelled line 81
  7. def OAI.CircleCoupling.mixture line 85
  8. lemma OAI.CircleCoupling.labelled_univ line 90
  9. lemma OAI.CircleCoupling.mixture_probability line 95
  10. lemma OAI.CircleCoupling.labelled_fiber line 103
  11. lemma OAI.CircleCoupling.labelled_fiber_label line 112
  12. lemma OAI.CircleCoupling.mixture_fiber line 132
  13. lemma OAI.CircleCoupling.mixture_fiber_label line 141
  14. lemma OAI.CircleCoupling.prod_fiber_fst line 150
  15. lemma OAI.CircleCoupling.prod_fiber_snd line 156
  16. def OAI.CircleCoupling.lowerDigits line 163
  17. def OAI.CircleCoupling.upperDigits line 164
  18. lemma OAI.CircleCoupling.lowerDigits_nonempty line 166
  19. lemma OAI.CircleCoupling.upperDigits_nonempty line 169
  20. lemma OAI.CircleCoupling.card_lowerDigits line 173
  21. lemma OAI.CircleCoupling.card_upperDigits line 175
  22. lemma OAI.CircleCoupling.mem_lowerDigits line 177
  23. lemma OAI.CircleCoupling.mem_upperDigits line 179
  24. def OAI.CircleCoupling.rectangle line 182
  25. instance OAI.CircleCoupling.rectangle_probability line 186
  26. lemma OAI.CircleCoupling.rectangle_fst_singleton line 189
  27. lemma OAI.CircleCoupling.rectangle_snd_singleton line 192
  28. lemma OAI.CircleCoupling.uniformOn_ae_mem line 196
  29. lemma OAI.CircleCoupling.rectangle_ae line 204
  30. def OAI.CircleCoupling.diagonal line 214
  31. instance OAI.CircleCoupling.diagonal_probability line 216
  32. lemma OAI.CircleCoupling.diagonal_fiber_fst line 220
  33. lemma OAI.CircleCoupling.diagonal_fiber_snd line 225
  34. def OAI.CircleCoupling.components line 231
  35. instance OAI.CircleCoupling.components_probability line 238
  36. def OAI.CircleCoupling.sixWeights line 242
  37. lemma OAI.CircleCoupling.sum_sixWeights line 243
  38. def OAI.CircleCoupling.sixLaw line 247
  39. lemma OAI.CircleCoupling.sixLaw_probability line 251
  40. lemma OAI.CircleCoupling.sixLaw_top_t line 257
  41. lemma OAI.CircleCoupling.sixLaw_bottom_t line 264
  42. lemma OAI.CircleCoupling.sixLaw_top_u line 271
  43. lemma OAI.CircleCoupling.sixLaw_bottom_u line 278
  44. lemma OAI.CircleCoupling.sixLaw_tag line 285
  45. lemma OAI.CircleCoupling.mixture_fiber_real line 293
  46. lemma OAI.CircleCoupling.rectangle_fst_real line 307
  47. lemma OAI.CircleCoupling.rectangle_snd_real line 312
  48. lemma OAI.CircleCoupling.rectangle_fst_real_le line 318
  49. lemma OAI.CircleCoupling.rectangle_snd_real_le line 324
  50. lemma OAI.CircleCoupling.sixLaw_fiber_real_le line 331
  51. lemma OAI.CircleCoupling.twoWidth_density_numerical line 351