OAI/Analysis/RotationWeights/FourierSampling.lean

GitHub source file

59 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ContinuousCircleWeight.Sampling.geometricFourierSum line 34
  2. def OAI.ContinuousCircleWeight.Sampling.fejerKernel line 36
  3. lemma OAI.ContinuousCircleWeight.Sampling.geometricFourierSum_apply line 39
  4. lemma OAI.ContinuousCircleWeight.Sampling.fejerKernel_apply line 43
  5. lemma OAI.ContinuousCircleWeight.Sampling.fejerKernel_nonneg line 47
  6. lemma OAI.ContinuousCircleWeight.Sampling.integral_fourier_exact line 50
  7. lemma OAI.ContinuousCircleWeight.Sampling.fejerKernel_complex_expansion line 55
  8. lemma OAI.ContinuousCircleWeight.Sampling.integral_fejerKernel line 65
  9. lemma OAI.ContinuousCircleWeight.Sampling.fourier_nat_eq_pow line 83
  10. lemma OAI.ContinuousCircleWeight.Sampling.geometricFourierSum_mul line 89
  11. lemma OAI.ContinuousCircleWeight.Sampling.fejerKernel_mul_chord_sq_le line 94
  12. lemma OAI.ContinuousCircleWeight.Sampling.fourier_one_chord_lower line 106
  13. lemma OAI.ContinuousCircleWeight.Sampling.fejerKernel_le_of_norm_ge line 133
  14. lemma OAI.ContinuousCircleWeight.Sampling.fourier_eval_sub line 148
  15. lemma OAI.ContinuousCircleWeight.Sampling.fejerKernel_le line 153
  16. lemma OAI.ContinuousCircleWeight.Sampling.integrable_fejer_mul line 164
  17. def OAI.ContinuousCircleWeight.Sampling.fejerApprox line 172
  18. lemma OAI.ContinuousCircleWeight.Sampling.fejerApprox_complex_expansion line 175
  19. lemma OAI.ContinuousCircleWeight.Sampling.fejerApprox_nonneg line 197
  20. lemma OAI.ContinuousCircleWeight.Sampling.fejerApprox_le_one line 201
  21. lemma OAI.ContinuousCircleWeight.Sampling.fejerApprox_local_error line 215
  22. def OAI.ContinuousCircleWeight.Sampling.doubleFourier line 247
  23. lemma OAI.ContinuousCircleWeight.Sampling.doubleFourier_norm line 250
  24. lemma OAI.ContinuousCircleWeight.Sampling.integrable_doubleFourier line 254
  25. lemma OAI.ContinuousCircleWeight.Sampling.finite_doubleFourier_error line 259
  26. lemma OAI.ContinuousCircleWeight.Sampling.finite_product_fourier_error line 283
  27. lemma OAI.ContinuousCircleWeight.Sampling.fourierCoeff_norm_le_one line 311
  28. def OAI.ContinuousCircleWeight.Sampling.fejerFrequency line 322
  29. def OAI.ContinuousCircleWeight.Sampling.fejerCoefficient line 324
  30. lemma OAI.ContinuousCircleWeight.Sampling.fejerApprox_fin_expansion line 327
  31. lemma OAI.ContinuousCircleWeight.Sampling.fejerCoefficient_zero_sum line 345
  32. lemma OAI.ContinuousCircleWeight.Sampling.fejerCoefficient_norm_sum_le line 355
  33. lemma OAI.ContinuousCircleWeight.Sampling.fejerFrequency_abs_lt line 371
  34. lemma OAI.ContinuousCircleWeight.Sampling.fejer_product_fourier_error line 377
  35. lemma OAI.ContinuousCircleWeight.Sampling.continuous_fejerApprox line 408
  36. lemma OAI.ContinuousCircleWeight.Sampling.fejer_unsmoothed_error line 419
  37. def OAI.ContinuousCircleWeight.Sampling.arcBoundary line 500
  38. lemma OAI.ContinuousCircleWeight.Sampling.measurableSet_arcBoundary line 503
  39. lemma OAI.ContinuousCircleWeight.Sampling.haarAddCircle_one_eq_volume line 507
  40. lemma OAI.ContinuousCircleWeight.Sampling.arcBoundary_measure_le line 511
  41. lemma OAI.ContinuousCircleWeight.Sampling.arc_indicator_locally_constant line 521
  42. lemma OAI.ContinuousCircleWeight.Sampling.arc_rectangle_discrepancy line 541
  43. lemma OAI.ContinuousCircleWeight.Sampling.periodic_integral_bounds line 596
  44. def OAI.ContinuousCircleWeight.Sampling.intervalLaw line 621
  45. lemma OAI.ContinuousCircleWeight.Sampling.intervalLaw_probability line 624
  46. lemma OAI.ContinuousCircleWeight.Sampling.integral_intervalLaw line 631
  47. lemma OAI.ContinuousCircleWeight.Sampling.intervalIntegrable_circle_comp line 637
  48. lemma OAI.ContinuousCircleWeight.Sampling.circle_scaled_integral_bounds line 649
  49. def OAI.ContinuousCircleWeight.Sampling.phasePair line 672
  50. def OAI.ContinuousCircleWeight.Sampling.phasePairLaw line 675
  51. lemma OAI.ContinuousCircleWeight.Sampling.continuous_phasePair line 678
  52. lemma OAI.ContinuousCircleWeight.Sampling.phasePairLaw_probability line 682
  53. lemma OAI.ContinuousCircleWeight.Sampling.integral_phasePairLaw line 688
  54. lemma OAI.ContinuousCircleWeight.Sampling.phasePairLaw_marginal_fst line 694
  55. lemma OAI.ContinuousCircleWeight.Sampling.phasePairLaw_marginal_snd line 714
  56. lemma OAI.ContinuousCircleWeight.Sampling.phasePair_fourier line 734
  57. lemma OAI.ContinuousCircleWeight.Sampling.intervalLaw_exponential_bound line 742
  58. lemma OAI.ContinuousCircleWeight.Sampling.phasePairLaw_fourier_bound line 765
  59. lemma OAI.ContinuousCircleWeight.Sampling.separated_phase_rectangle_bound line 773