OAI/Analysis/IrrationalRotation/Product/OneCoordinateDensity.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Invariant233.OneCoordinateCoupling.intervalDensity_measurable line 12
  2. lemma OAI.Invariant233.OneCoordinateCoupling.intervalDensity_nonneg line 15
  3. lemma OAI.Invariant233.OneCoordinateCoupling.intervalDensity_memLp line 20
  4. lemma OAI.Invariant233.OneCoordinateCoupling.intervalDensity_integral line 24
  5. lemma OAI.Invariant233.OneCoordinateCoupling.intervalDensity_variance line 30
  6. lemma OAI.Invariant233.OneCoordinateCoupling.intervalDensity_le_inv_length line 38
  7. lemma OAI.Invariant233.OneCoordinateCoupling.intervalDensity_le_width line 45
  8. lemma OAI.Invariant233.OneCoordinateCoupling.leftLaw_eq_withDensity line 54
  9. lemma OAI.Invariant233.OneCoordinateCoupling.rightLaw_eq_withDensity line 64
  10. lemma OAI.Invariant233.OneCoordinateCoupling.leftDensity_bound line 74
  11. lemma OAI.Invariant233.OneCoordinateCoupling.rightDensity_bound line 91
  12. lemma OAI.Invariant233.OneCoordinateCoupling.pairLaw_fst_density line 108
  13. lemma OAI.Invariant233.OneCoordinateCoupling.pairLaw_snd_density line 130
  14. lemma OAI.Invariant233.OneCoordinateCoupling.leftMarginalDensity_bounds line 154
  15. lemma OAI.Invariant233.OneCoordinateCoupling.rightMarginalDensity_bounds line 169
  16. lemma OAI.Invariant233.OneCoordinateCoupling.intervalDensity_variance_le_width line 184
  17. lemma OAI.Invariant233.OneCoordinateCoupling.leftDensity_variance_bound line 191
  18. lemma OAI.Invariant233.OneCoordinateCoupling.rightDensity_variance_bound line 207
  19. lemma OAI.Invariant233.OneCoordinateCoupling.marginalDensity_sub_one line 223
  20. lemma OAI.Invariant233.OneCoordinateCoupling.leftMarginalDensity_energy line 230
  21. lemma OAI.Invariant233.OneCoordinateCoupling.rightMarginalDensity_energy line 242
  22. lemma OAI.Invariant233.OneCoordinateCoupling.leftMarginalDensity_memLp line 254
  23. lemma OAI.Invariant233.OneCoordinateCoupling.rightMarginalDensity_memLp line 262
  24. lemma OAI.Invariant233.OneCoordinateCoupling.leftMarginalDensity_integral line 270
  25. lemma OAI.Invariant233.OneCoordinateCoupling.rightMarginalDensity_integral line 293
  26. lemma OAI.Invariant233.OneCoordinateCoupling.pairLaw_fst_le_ten line 316
  27. lemma OAI.Invariant233.OneCoordinateCoupling.pairLaw_snd_le_ten line 329