OAI/Analysis/IrrationalRotation/Sampling/ProductSamplingWeights.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Invariant233.ProductModel.SamplingWeights.coordinateWeight line 14
  2. def OAI.Invariant233.ProductModel.SamplingWeights.orbitWeight line 17
  3. def OAI.Invariant233.ProductModel.SamplingWeights.prefixWeight line 22
  4. def OAI.Invariant233.ProductModel.SamplingWeights.height line 27
  5. theorem OAI.Invariant233.ProductModel.SamplingWeights.measurable_triangularKernel line 29
  6. theorem OAI.Invariant233.ProductModel.SamplingWeights.measurable_coordinateWeight line 38
  7. theorem OAI.Invariant233.ProductModel.SamplingWeights.coordinateWeight_bounds line 44
  8. theorem OAI.Invariant233.ProductModel.SamplingWeights.coordinateWeight_ne_zero_imp line 57
  9. theorem OAI.Invariant233.ProductModel.SamplingWeights.measurable_orbitWeight line 77
  10. theorem OAI.Invariant233.ProductModel.SamplingWeights.measurable_prefixWeight line 85
  11. theorem OAI.Invariant233.ProductModel.SamplingWeights.prefixWeight_restrict line 93
  12. theorem OAI.Invariant233.ProductModel.SamplingWeights.orbitWeight_bounds line 101
  13. theorem OAI.Invariant233.ProductModel.SamplingWeights.orbitWeight_ne_zero_prefix_order line 113
  14. theorem OAI.Invariant233.ProductModel.SamplingWeights.orbitWeight_ae_prefix_order line 129
  15. theorem OAI.Invariant233.ProductModel.SamplingWeights.memLp_orbitWeight line 141
  16. theorem OAI.Invariant233.ProductModel.SamplingWeights.orbitWeight_finite line 150
  17. theorem OAI.Invariant233.ProductModel.SamplingWeights.orbitPairMeasure_finite line 163
  18. theorem OAI.Invariant233.ProductModel.SamplingWeights.orbitAverageMeasure_finite line 171
  19. theorem OAI.Invariant233.ProductModel.SamplingWeights.manuscript_orbitWeight_construction line 185