OAI/Analysis/RotationWeights/EndpointMoments.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CircleCoupling.continuous_measureReal_of_le line 79
  2. lemma OAI.CircleCoupling.sq_measure_bound_of_generating_ring line 89
  3. lemma OAI.CircleCoupling.sqrt_measure_bound_of_generating_ring line 111
  4. lemma OAI.CircleCoupling.infinitePi_sqrt_bound line 127
  5. lemma OAI.CircleCoupling.infinitePi_l2_bound line 153
  6. lemma OAI.CircleCoupling.observedDigits_sqrt_bound line 181
  7. lemma OAI.CircleCoupling.hybridEndpoint_sqrt_bound line 202
  8. lemma OAI.CircleCoupling.hybridEndpoint_absolutelyContinuous line 220
  9. structure OAI.CircleCoupling.DigitSystem line 240
  10. def OAI.CircleCoupling.DigitSystem.radix line 246
  11. lemma OAI.CircleCoupling.DigitSystem.radix_ge_two line 247
  12. instance OAI.CircleCoupling.DigitSystem.(instance at line 251) line 251
  13. abbrev OAI.CircleCoupling.DigitSystem.Sample line 252
  14. abbrev OAI.CircleCoupling.DigitSystem.Samples line 253
  15. def OAI.CircleCoupling.DigitSystem.law line 255
  16. instance OAI.CircleCoupling.DigitSystem.(instance at line 258) line 258
  17. def OAI.CircleCoupling.DigitSystem.probability line 262
  18. instance OAI.CircleCoupling.DigitSystem.(instance at line 263) line 263
  19. def OAI.CircleCoupling.DigitSystem.observe line 265
  20. def OAI.CircleCoupling.DigitSystem.endpoint line 266
  21. lemma OAI.CircleCoupling.DigitSystem.measurable_observe line 267
  22. lemma OAI.CircleCoupling.DigitSystem.measurable_endpoint line 271
  23. def OAI.CircleCoupling.DigitSystem.error line 274
  24. lemma OAI.CircleCoupling.DigitSystem.error_nonneg line 277
  25. lemma OAI.CircleCoupling.DigitSystem.moment line 281
  26. lemma OAI.CircleCoupling.DigitSystem.hybrid_sqrt_bound line 299
  27. lemma OAI.CircleCoupling.DigitSystem.hybrid_ac line 307
  28. lemma OAI.CircleCoupling.DigitSystem.ae_hybrid_gridFree line 313
  29. lemma OAI.CircleCoupling.DigitSystem.ae_digit_order line 321
  30. lemma OAI.CircleCoupling.DigitSystem.ae_coordinate_order line 335