OAI/Analysis/RotationWeights/OrbitBounds.lean

GitHub source file

68 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CircleSampling.modelAngle line 61
  2. def OAI.CircleSampling.modelGood line 62
  3. def OAI.CircleSampling.modelF line 63
  4. def OAI.CircleSampling.modelWeight line 64
  5. lemma OAI.CircleSampling.model_beta line 66
  6. lemma OAI.CircleSampling.model_beta_sum line 69
  7. lemma OAI.CircleSampling.model_good_ae line 73
  8. lemma OAI.CircleSampling.modelGood_measurable line 75
  9. lemma OAI.CircleSampling.modelF_measurable line 76
  10. lemma OAI.CircleSampling.modelF_pos line 77
  11. lemma OAI.CircleSampling.modelF_zero line 78
  12. lemma OAI.CircleSampling.modelF_antitone line 79
  13. lemma OAI.CircleSampling.modelWeight_bounds line 81
  14. lemma OAI.CircleSampling.modelF_add line 83
  15. lemma OAI.CircleSampling.modelGood_shift line 86
  16. lemma OAI.CircleSampling.modelF_ratio_ordered line 88
  17. lemma OAI.CircleSampling.modelF_ratio_tail line 92
  18. lemma OAI.CircleSampling.phase_orbit line 97
  19. lemma OAI.CircleSampling.model_coordinate_shift line 103
  20. def OAI.CircleSampling.weightedMeasure line 113
  21. lemma OAI.CircleSampling.weightedMeasure_finite line 115
  22. lemma OAI.CircleSampling.weightedMeasure_real_apply line 120
  23. lemma OAI.CircleSampling.weightedMeasure_integral line 126
  24. lemma OAI.CircleSampling.weightedMeasure_map_equiv line 133
  25. def OAI.CircleSampling.weightedGraph line 151
  26. lemma OAI.CircleSampling.weightedGraph_fst line 154
  27. lemma OAI.CircleSampling.weightedGraph_snd line 159
  28. lemma OAI.CircleSampling.weightedMeasure_add line 168
  29. lemma OAI.CircleSampling.weightedMeasure_mul line 174
  30. lemma OAI.CircleSampling.weightedMeasure_sum line 180
  31. lemma OAI.CircleSampling.map_finsetSum line 194
  32. def OAI.CircleSampling.finiteGraphAverage line 202
  33. def OAI.CircleSampling.finiteAverage line 205
  34. lemma OAI.CircleSampling.finiteGraphAverage_fst line 208
  35. lemma OAI.CircleSampling.finiteGraphAverage_snd line 218
  36. lemma OAI.CircleSampling.finiteGraphAverage_finite line 230
  37. lemma OAI.CircleSampling.finiteGraphAverage_ae line 239
  38. lemma OAI.CircleSampling.stageEll_pos line 262
  39. lemma OAI.CircleSampling.stageEll_lt line 264
  40. lemma OAI.CircleSampling.stageAlpha_pos line 268
  41. def OAI.CircleSampling.stageFactor line 271
  42. def OAI.CircleSampling.stageWeight line 275
  43. lemma OAI.CircleSampling.stageFactor_measurable line 278
  44. lemma OAI.CircleSampling.stageFactor_bounds line 281
  45. lemma OAI.CircleSampling.stageWeight_measurable line 285
  46. lemma OAI.CircleSampling.stageWeight_bounds line 288
  47. lemma OAI.CircleSampling.stageWeight_memLp line 296
  48. lemma OAI.CircleSampling.stage_frequency line 301
  49. lemma OAI.CircleSampling.stage_phase line 305
  50. lemma OAI.CircleSampling.stageFactor_model line 309
  51. lemma OAI.CircleSampling.stageWeight_negative line 314
  52. instance OAI.CircleSampling.stageSample_nonempty line 321
  53. def OAI.CircleSampling.stageDensity line 324
  54. lemma OAI.CircleSampling.stageDensity_measurable line 326
  55. lemma OAI.CircleSampling.stageDensity_nonneg line 330
  56. lemma OAI.CircleSampling.stageDensity_memLp line 334
  57. lemma OAI.CircleSampling.stageDensity_energy line 339
  58. def OAI.CircleSampling.sampleBound line 347
  59. def OAI.CircleSampling.oldGraphBad line 348
  60. def OAI.CircleSampling.tailGraphBad line 350
  61. def OAI.CircleSampling.graphBad line 352
  62. lemma OAI.CircleSampling.graphBad_measurable line 353
  63. lemma OAI.CircleSampling.sampleBound_pos line 356
  64. lemma OAI.CircleSampling.sample_bound line 358
  65. lemma OAI.CircleSampling.coordinate_add_nowrap line 364
  66. lemma OAI.CircleSampling.positive_weight_order line 372
  67. lemma OAI.CircleSampling.stageWeight_order line 389
  68. lemma OAI.CircleSampling.restricted_orbit_order line 399