OAI/Analysis/IrrationalRotation/Sampling/ProductSamplingPhaseMoments.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Invariant233.ProductSamplingPhaseMoments.eVariationOn_ofReal line 13
  2. theorem OAI.Invariant233.ProductSamplingPhaseMoments.real_bv_discrepancy line 17
  3. theorem OAI.Invariant233.ProductSamplingPhaseMoments.real_one_phase_error line 47
  4. def OAI.Invariant233.ProductSamplingPhaseMoments.unitInterval line 61
  5. instance OAI.Invariant233.ProductSamplingPhaseMoments.unitInterval_probability line 63
  6. theorem OAI.Invariant233.ProductSamplingPhaseMoments.integral_unitInterval line 67
  7. theorem OAI.Invariant233.ProductSamplingPhaseMoments.fractionLaw_le_two line 72
  8. theorem OAI.Invariant233.ProductSamplingPhaseMoments.integral_sample_le_two line 82
  9. def OAI.Invariant233.ProductSamplingPhaseMoments.mean line 98
  10. def OAI.Invariant233.ProductSamplingPhaseMoments.sample line 100
  11. def OAI.Invariant233.ProductSamplingPhaseMoments.realBVSize line 103
  12. theorem OAI.Invariant233.ProductSamplingPhaseMoments.realBVSize_nonneg line 107
  13. theorem OAI.Invariant233.ProductSamplingPhaseMoments.measurable_sample line 113
  14. theorem OAI.Invariant233.ProductSamplingPhaseMoments.measurable_mean line 117
  15. theorem OAI.Invariant233.ProductSamplingPhaseMoments.sample_memLp line 121
  16. theorem OAI.Invariant233.ProductSamplingPhaseMoments.mean_memLp line 129
  17. theorem OAI.Invariant233.ProductSamplingPhaseMoments.coordinate_pair_error_le line 140
  18. theorem OAI.Invariant233.ProductSamplingPhaseMoments.section_intervalIntegrable line 179
  19. theorem OAI.Invariant233.ProductSamplingPhaseMoments.coordinate_cross_error_le line 189
  20. theorem OAI.Invariant233.ProductSamplingPhaseMoments.coordinate_square_le_two line 231
  21. theorem OAI.Invariant233.ProductSamplingPhaseMoments.coordinate_cross_error_le_four line 256
  22. theorem OAI.Invariant233.ProductSamplingPhaseMoments.expected_average_error_le line 275