OAI/Analysis/RotationWeights/Main.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CircleSampling.blockLength_ge_index line 87
  2. lemma OAI.CircleSampling.blockH_zero_half line 91
  3. lemma OAI.CircleSampling.blockH_diverges_zero line 101
  4. def OAI.CircleSampling.finalWeight line 110
  5. lemma OAI.CircleSampling.finalWeight_bounds line 112
  6. lemma OAI.CircleSampling.finalWeight_zero line 114
  7. lemma OAI.CircleSampling.finalWeight_log line 115
  8. lemma OAI.CircleSampling.blockG_exponent line 130
  9. lemma OAI.CircleSampling.finalWeight_coboundary line 145
  10. def OAI.CircleSampling.modelBorel line 165
  11. lemma OAI.CircleSampling.modelBorel_field line 172
  12. lemma OAI.CircleSampling.modelAngle_ergodic line 183
  13. theorem OAI.CircleSampling.modelOperator_no_projection line 189
  14. theorem OAI.CircleSampling.continuousOperator_no_projection line 215
  15. lemma OAI.ContinuousCircleWeight.regular_isTracialRotation line 238
  16. lemma OAI.ContinuousCircleWeight.fiberConjugacy_cfc line 244
  17. lemma OAI.ContinuousCircleWeight.fiberConjugacy_weighted line 257
  18. theorem OAI.ContinuousCircleWeight.main_theorem line 267

    Distinct definitions of this name: ComparatorChallenges/ContinuousCircleWeight.lean:50 (same statement text; different proof or body). Qualify references as OAI.ContinuousCircleWeight.main_theorem@path.