OAI/Analysis/RotationWeights/SamplingBounds.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CircleSampling.scaleEll line 38
  2. def OAI.CircleSampling.scaleAlpha line 39
  3. def OAI.CircleSampling.scaleDiscrepancy line 40
  4. def OAI.CircleSampling.offError line 41
  5. def OAI.CircleSampling.samplingError line 44
  6. lemma OAI.CircleSampling.rpow_scale_mul line 47
  7. lemma OAI.CircleSampling.rpow_scale_sq line 49
  8. lemma OAI.CircleSampling.scale_product line 51
  9. lemma OAI.CircleSampling.mass_offError line 54
  10. lemma OAI.CircleSampling.tendsto_nat_rpow_neg line 81
  11. lemma OAI.CircleSampling.tendsto_scaleEll line 84
  12. lemma OAI.CircleSampling.tendsto_scaleAlpha line 87
  13. lemma OAI.CircleSampling.tendsto_mass_offError line 89
  14. lemma OAI.CircleSampling.tendsto_mass_alpha line 107
  15. lemma OAI.CircleSampling.tendsto_samplingError line 114
  16. lemma OAI.CircleSampling.eventually_rpow_linear_gap line 130
  17. lemma OAI.CircleSampling.inv_scaleEll line 147
  18. lemma OAI.CircleSampling.inv_scaleAlpha line 152
  19. lemma OAI.CircleSampling.scaleAlpha_pos line 155
  20. lemma OAI.CircleSampling.diagonal_estimate line 158
  21. lemma OAI.CircleSampling.eventually_diagonal_small line 176
  22. lemma OAI.CircleSampling.sampling_discrepancy_numeric line 199
  23. lemma OAI.CircleSampling.sampling_phase_discrepancy line 237
  24. lemma OAI.CircleSampling.eventually_sampling_marginal line 259
  25. def OAI.CircleSampling.IdealNumerics line 301
  26. lemma OAI.CircleSampling.eventually_IdealNumerics line 307
  27. lemma OAI.CircleSampling.ideal_stage_error line 314
  28. lemma OAI.CircleSampling.measurable_idealAverage line 375
  29. lemma OAI.CircleSampling.idealAverage_bounds line 387
  30. def OAI.CircleSampling.idealEnergy line 404
  31. lemma OAI.CircleSampling.idealEnergy_nonneg line 408
  32. lemma OAI.CircleSampling.measurable_idealEnergy line 412
  33. lemma OAI.CircleSampling.idealEnergy_le line 417
  34. lemma OAI.CircleSampling.idealEnergy_integrable line 431
  35. def OAI.CircleSampling.phaseFailure line 443
  36. lemma OAI.CircleSampling.measurableSet_phaseFailure line 445
  37. lemma OAI.CircleSampling.phaseFailure_norm line 452
  38. lemma OAI.CircleSampling.interval_phase_ball_bound line 474
  39. lemma OAI.CircleSampling.phase_failure_probability line 491