OAI/Analysis/RotationWeights/WeakSampling.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.ContinuousCircleWeight.compactMap_integrable line 36
  2. theorem OAI.ContinuousCircleWeight.probability_integral_lipschitz line 41
  3. theorem OAI.ContinuousCircleWeight.probability_tendsto_of_dense_span line 50
  4. lemma OAI.ContinuousCircleWeight.not_mem_frontier_ge_of_continuousAt line 86
  5. lemma OAI.ContinuousCircleWeight.ae_null_frontier_ge line 102
  6. theorem OAI.ContinuousCircleWeight.tendsto_integral_nn_of_weak_of_ae_continuous line 117
  7. theorem OAI.ContinuousCircleWeight.tendsto_integral_of_weak_of_ae_continuous line 149
  8. theorem OAI.ContinuousCircleWeight.tendsto_integral_complex_of_weak_of_ae_continuous line 173
  9. def OAI.ContinuousCircleWeight.withParameter line 201
  10. theorem OAI.ContinuousCircleWeight.integral_withParameter line 206
  11. theorem OAI.ContinuousCircleWeight.probability_tendsto_withParameter line 214
  12. abbrev OAI.ContinuousCircleWeight.Sampling.CircleX line 243
  13. def OAI.ContinuousCircleWeight.Sampling.torusFourier line 248
  14. theorem OAI.ContinuousCircleWeight.Sampling.torusFourier_apply line 252
  15. theorem OAI.ContinuousCircleWeight.Sampling.torusFourier_zero line 255
  16. theorem OAI.ContinuousCircleWeight.Sampling.torusFourier_add line 259
  17. theorem OAI.ContinuousCircleWeight.Sampling.torusFourier_neg line 265
  18. def OAI.ContinuousCircleWeight.Sampling.torusFourierSubalgebra line 271
  19. theorem OAI.ContinuousCircleWeight.Sampling.torusFourierSubalgebra_coe line 280
  20. theorem OAI.ContinuousCircleWeight.Sampling.torusFourier_single line 290
  21. theorem OAI.ContinuousCircleWeight.Sampling.torusFourierSubalgebra_separatesPoints line 298
  22. theorem OAI.ContinuousCircleWeight.Sampling.span_torusFourier_closure_eq_top line 310
  23. theorem OAI.ContinuousCircleWeight.Sampling.integral_fourier line 317
  24. def OAI.ContinuousCircleWeight.Sampling.circleHaar line 322
  25. def OAI.ContinuousCircleWeight.Sampling.torusHaar line 325
  26. theorem OAI.ContinuousCircleWeight.Sampling.integral_torusFourier line 328
  27. theorem OAI.ContinuousCircleWeight.Sampling.fourier_sum line 344
  28. def OAI.ContinuousCircleWeight.Sampling.characterCurve line 351
  29. theorem OAI.ContinuousCircleWeight.Sampling.torusFourier_curve line 355
  30. def OAI.ContinuousCircleWeight.Sampling.curveLaw line 362
  31. theorem OAI.ContinuousCircleWeight.Sampling.integral_curveLaw line 365
  32. theorem OAI.ContinuousCircleWeight.Sampling.integral_curveLaw_torusFourier line 371
  33. theorem OAI.ContinuousCircleWeight.Sampling.eventually_sum_ne_zero_of_separated line 378
  34. theorem OAI.ContinuousCircleWeight.Sampling.curveLaw_tendsto_of_nonresonance line 409
  35. theorem OAI.ContinuousCircleWeight.Sampling.curveLaw_tendsto_of_separated line 425
  36. theorem OAI.ContinuousCircleWeight.Sampling.separated_of_successive line 447
  37. theorem OAI.ContinuousCircleWeight.Sampling.curveLaw_tendsto_of_successiveRatios line 468
  38. theorem OAI.ContinuousCircleWeight.Sampling.circle_approximation_with_parameters line 481