OAI/Analysis/IrrationalRotation/Rotation/CircleQuantizedMarginals.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Invariant233.CircleCoupling.digitReference_isProbabilityMeasure line 14
  2. lemma OAI.Invariant233.CircleCoupling.rawDensity_memLp line 21
  3. lemma OAI.Invariant233.CircleCoupling.rawDensity_laws line 31
  4. lemma OAI.Invariant233.CircleCoupling.coordinateLaw_map_endpoint line 53
  5. lemma OAI.Invariant233.CircleCoupling.observedDigit_density line 72
  6. lemma OAI.Invariant233.CircleCoupling.digitDensity_laws line 87
  7. lemma OAI.Invariant233.CircleCoupling.digitDensity_memLp line 107
  8. lemma OAI.Invariant233.CircleCoupling.measurable_hybridDigits line 115
  9. lemma OAI.Invariant233.CircleCoupling.measurable_hybridPoint line 120
  10. lemma OAI.Invariant233.CircleCoupling.map_hybridDigits line 126
  11. lemma OAI.Invariant233.CircleCoupling.hybridPoint_const line 139