OAI/Analysis/IrrationalRotation/Sampling/SamplingMomentBounds.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.InvariantRotation.SamplingMomentBounds.abs_prod_le_pow_card line 9
  2. theorem OAI.InvariantRotation.SamplingMomentBounds.abs_prod_sub_prod_le line 18
  3. theorem OAI.InvariantRotation.SamplingMomentBounds.product_perturbation_bound line 26
  4. theorem OAI.InvariantRotation.SamplingMomentBounds.product_perturbation_bound_exp line 35
  5. theorem OAI.InvariantRotation.SamplingMomentBounds.averaged_moment_bound line 56
  6. theorem OAI.InvariantRotation.SamplingMomentBounds.norm_average_sub_sq_le line 107
  7. theorem OAI.InvariantRotation.SamplingMomentBounds.l2_norm_sq_eq_integral_sq line 128
  8. theorem OAI.InvariantRotation.SamplingMomentBounds.l2_coe_finset_sum line 133
  9. theorem OAI.InvariantRotation.SamplingMomentBounds.integral_average_sub_sq_le line 146
  10. theorem OAI.InvariantRotation.SamplingMomentBounds.integral_average_sub_sq_le_of_memLp line 172