OAI/Analysis/RotationWeights/Rounding.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.CircleRounding.X line 84
  2. def OAI.CircleRounding.repr line 85
  3. lemma OAI.CircleRounding.repr_mem line 86
  4. lemma OAI.CircleRounding.coe_repr line 88
  5. lemma OAI.CircleRounding.repr_measurable line 90
  6. lemma OAI.CircleRounding.repr_mk line 91
  7. lemma OAI.CircleRounding.repr_zero line 94
  8. def OAI.CircleRounding.intervalRamp line 96
  9. lemma OAI.CircleRounding.intervalRamp_continuous line 97
  10. lemma OAI.CircleRounding.intervalRamp_monotone line 100
  11. lemma OAI.CircleRounding.intervalRamp_zero line 105
  12. lemma OAI.CircleRounding.intervalRamp_one line 110
  13. lemma OAI.CircleRounding.intervalRamp_bounds line 115
  14. lemma OAI.CircleRounding.intervalRamp_middle line 119
  15. def OAI.CircleRounding.periodicCorrector line 124
  16. lemma OAI.CircleRounding.periodicCorrector_continuous line 125
  17. lemma OAI.CircleRounding.periodicCorrector_repr line 129
  18. def OAI.CircleRounding.roundedFloor line 133
  19. lemma OAI.CircleRounding.roundedFloor_continuous line 134
  20. lemma OAI.CircleRounding.roundedFloor_add_one line 136
  21. def OAI.CircleRounding.roundedDrop line 140
  22. def OAI.CircleRounding.correction line 141
  23. lemma OAI.CircleRounding.roundedDrop_continuous line 142
  24. lemma OAI.CircleRounding.correction_measurable line 145
  25. lemma OAI.CircleRounding.repr_add line 147
  26. lemma OAI.CircleRounding.roundedDrop_formula line 152
  27. lemma OAI.CircleRounding.roundedDrop_coboundary line 159
  28. lemma OAI.CircleRounding.roundedDrop_nonneg line 163
  29. lemma OAI.CircleRounding.roundedDrop_zero line 183
  30. lemma OAI.CircleRounding.correction_support line 191
  31. lemma OAI.CircleRounding.roundedDrop_support line 198
  32. lemma OAI.CircleRounding.measure_repr_lower line 209
  33. lemma OAI.CircleRounding.measure_repr_upper line 226
  34. lemma OAI.CircleRounding.correction_measure line 243
  35. lemma OAI.CircleRounding.roundedDrop_measure line 249
  36. lemma OAI.CircleRounding.roundedDrop_integral line 255