OAI/Analysis/IrrationalRotation/Sampling/ProductSamplingMoments.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.InvariantRotation.SamplingMomentBounds.memLp_coordinate_prod line 10
  2. theorem OAI.InvariantRotation.SamplingMomentBounds.integral_coordinate_prod_mul line 23
  3. theorem OAI.InvariantRotation.SamplingMomentBounds.integral_coordinate_prod_sq line 31
  4. theorem OAI.InvariantRotation.SamplingMomentBounds.coordinate_product_pair_error_le line 38
  5. theorem OAI.InvariantRotation.SamplingMomentBounds.coordinate_product_sq_le_pow line 56
  6. theorem OAI.InvariantRotation.SamplingMomentBounds.integral_average_coordinate_products_sub_sq_le line 69
  7. theorem OAI.InvariantRotation.SamplingMomentBounds.integral_iterated_eq_coordinate_prod line 111
  8. theorem OAI.InvariantRotation.SamplingMomentBounds.memLp_average_coordinate_products line 130
  9. theorem OAI.InvariantRotation.SamplingMomentBounds.expected_integral_average_products_sub_sq_le line 140