OAI/Analysis/IrrationalRotation/Sampling/ProductSamplingIdealBounds.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Invariant233.ProductSampling.partial_product_sq_le_exp line 16
  2. theorem OAI.Invariant233.ProductSampling.partial_product_eLpNorm_le_exp line 45
  3. def OAI.Invariant233.ProductModel.SamplingWeights.idealCoordinate line 69
  4. theorem OAI.Invariant233.ProductModel.SamplingWeights.measurable_idealCoordinate line 73
  5. theorem OAI.Invariant233.ProductModel.SamplingWeights.idealCoordinate_nonneg line 78
  6. theorem OAI.Invariant233.ProductModel.SamplingWeights.norm_idealCoordinate_le line 84
  7. theorem OAI.Invariant233.ProductModel.SamplingWeights.memLp_idealCoordinate line 93
  8. theorem OAI.Invariant233.ProductModel.SamplingWeights.intervalIntegrable_idealCoordinate line 102
  9. theorem OAI.Invariant233.ProductModel.SamplingWeights.testedCoordinateWeight_le_univ line 112
  10. theorem OAI.Invariant233.ProductModel.SamplingWeights.intervalIntegrable_testedCoordinateWeight line 129
  11. theorem OAI.Invariant233.ProductModel.SamplingWeights.idealCoordinate_le_univ line 141
  12. theorem OAI.Invariant233.ProductModel.SamplingWeights.idealCoordinate_univ_eq_scalar line 150
  13. theorem OAI.Invariant233.ProductModel.SamplingWeights.idealCoordinate_univ_le_one_of_mem line 162
  14. theorem OAI.Invariant233.ProductModel.SamplingWeights.idealCoordinate_square_integral_le line 174
  15. theorem OAI.Invariant233.ProductModel.SamplingWeights.integral_circleRepresentative_eq_interval line 215
  16. theorem OAI.Invariant233.ProductModel.SamplingWeights.idealCoordinate_circle_square_integral_le line 227
  17. def OAI.Invariant233.ProductModel.SamplingWeights.idealProduct line 238
  18. theorem OAI.Invariant233.ProductModel.SamplingWeights.memLp_idealProduct line 242
  19. theorem OAI.Invariant233.ProductModel.SamplingWeights.manuscript_idealProduct_eLpNorm_le line 249
  20. theorem OAI.Invariant233.ProductModel.SamplingWeights.idealProduct_eLpNorm_le_height line 268
  21. theorem OAI.Invariant233.ProductModel.SamplingWeights.source_idealProduct_uniform_bound line 290