OAI/Analysis/RotationWeights/ProductSampling.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ContinuousCircleWeight.Sampling.phasePairLaw_fst_ac line 33
  2. lemma OAI.ContinuousCircleWeight.Sampling.phasePairLaw_snd_ac line 44
  3. lemma OAI.ContinuousCircleWeight.Sampling.product_weight_discrepancy line 55
  4. def OAI.CircleSampling.orientedWeight line 100
  5. lemma OAI.CircleSampling.measurable_orientedWeight line 103
  6. lemma OAI.CircleSampling.orientedWeight_bounds line 107
  7. lemma OAI.CircleSampling.orientedWeight_isTwoArcs line 112
  8. lemma OAI.CircleSampling.orientedWeight_mean line 119
  9. lemma OAI.CircleSampling.orientedWeight_sq line 126
  10. lemma OAI.CircleSampling.orientedWeight_mean_sq line 134
  11. lemma OAI.CircleSampling.bounded_integrable line 149
  12. lemma OAI.CircleSampling.bounded_sq_integrable line 155
  13. lemma OAI.CircleSampling.bounded_pair_integrable line 161
  14. lemma OAI.CircleSampling.trial_mean_lower line 169
  15. lemma OAI.CircleSampling.trial_sq_upper line 197
  16. lemma OAI.CircleSampling.trial_pair_upper line 222
  17. def OAI.CircleSampling.productAverage line 281
  18. lemma OAI.CircleSampling.measurable_productTerm line 284
  19. lemma OAI.CircleSampling.integrable_productTerm line 288
  20. lemma OAI.CircleSampling.integral_productAverage line 297
  21. lemma OAI.CircleSampling.productAverage_sq line 308
  22. lemma OAI.CircleSampling.integral_productAverage_sq line 320
  23. lemma OAI.CircleSampling.productAverage_integrable line 347
  24. lemma OAI.CircleSampling.productAverage_sq_integrable line 353
  25. lemma OAI.CircleSampling.productAverage_first_bound line 367
  26. lemma OAI.CircleSampling.productAverage_second_bound line 378
  27. lemma OAI.CircleSampling.productAverage_error_bound line 407
  28. def OAI.CircleSampling.idealAverage line 432
  29. lemma OAI.CircleSampling.ideal_error_bound line 435