OAI/Analysis/RotationWeights/NestedAngles.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CircleSampling.enumeratedRat line 55
  2. lemma OAI.CircleSampling.enumeratedRat_encode line 56
  3. lemma OAI.CircleSampling.closed_interval_avoiding line 59
  4. lemma OAI.CircleSampling.irrational_in_nested_intervals line 69
  5. lemma OAI.CircleSampling.exists_recursive_chain line 83
  6. lemma OAI.CircleSampling.prefix_persistent line 94
  7. lemma OAI.CircleSampling.diagonal_prefix_eq line 101
  8. lemma OAI.CircleSampling.endpoints_sum line 108
  9. lemma OAI.CircleSampling.endpoints_growth line 114
  10. def OAI.CircleSampling.extendPrefix line 124
  11. lemma OAI.CircleSampling.extendPrefix_old line 126
  12. lemma OAI.CircleSampling.extendPrefix_block line 128
  13. lemma OAI.CircleSampling.extendPrefix_pos line 133
  14. lemma OAI.CircleSampling.extendPrefix_dvd line 139
  15. lemma OAI.CircleSampling.extendPrefix_lt line 149
  16. def OAI.CircleSampling.positiveArc line 163
  17. lemma OAI.CircleSampling.positiveArc_open line 165
  18. lemma OAI.CircleSampling.positiveArc_nonempty line 167
  19. lemma OAI.CircleSampling.positiveArc_mem line 172
  20. structure OAI.CircleSampling.ScaleState line 180
  21. structure OAI.CircleSampling.ScaleState.Valid line 190
  22. def OAI.CircleSampling.gridTolerance line 201
  23. def OAI.CircleSampling.gridPoint line 203
  24. def OAI.CircleSampling.CoefficientBudget line 205
  25. structure OAI.CircleSampling.ScaleStep line 213
  26. def OAI.CircleSampling.ScaleStep.C line 252
  27. def OAI.CircleSampling.ScaleStep.next line 254
  28. lemma OAI.CircleSampling.ScaleStep.mpos line 264
  29. lemma OAI.CircleSampling.ScaleStep.qstrict line 267
  30. lemma OAI.CircleSampling.ScaleStep.next_valid line 275
  31. lemma OAI.CircleSampling.exists_scale_step line 294
  32. def OAI.CircleSampling.initialScaleState line 322
  33. lemma OAI.CircleSampling.initialScaleState_valid line 331
  34. def OAI.CircleSampling.chosenScaleStep line 334
  35. def OAI.CircleSampling.scaleState line 336
  36. def OAI.CircleSampling.scaleStep line 339
  37. lemma OAI.CircleSampling.scaleState_succ line 340
  38. lemma OAI.CircleSampling.exists_global_angle line 342
  39. structure OAI.CircleSampling.BlockPartition line 355
  40. lemma OAI.CircleSampling.BlockPartition.strictMono line 362
  41. lemma OAI.CircleSampling.BlockPartition.ge line 364
  42. lemma OAI.CircleSampling.BlockPartition.exists_unique line 369
  43. def OAI.CircleSampling.BlockPartition.number line 391
  44. lemma OAI.CircleSampling.BlockPartition.number_spec line 392
  45. lemma OAI.CircleSampling.BlockPartition.number_eq line 394
  46. def OAI.CircleSampling.BlockPartition.position line 397
  47. def OAI.CircleSampling.BlockPartition.equiv line 400
  48. lemma OAI.CircleSampling.BlockPartition.equiv_apply line 415
  49. lemma OAI.CircleSampling.BlockPartition.number_mono line 417
  50. lemma OAI.CircleSampling.BlockPartition.number_tendsto line 426