OAI/Analysis/RotationWeights/Concentration.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.CircleConcentration.X line 84
  2. def OAI.CircleConcentration.orbitMin line 85
  3. lemma OAI.CircleConcentration.orbitMin_continuous line 87
  4. lemma OAI.CircleConcentration.orbitMin_nonneg line 90
  5. lemma OAI.CircleConcentration.orbitMin_le line 92
  6. lemma OAI.CircleConcentration.orbitMin_max line 94
  7. def OAI.CircleConcentration.orbitRadius line 97
  8. lemma OAI.CircleConcentration.orbitMin_le_radius line 98
  9. lemma OAI.CircleConcentration.orbitRadius_nonneg line 100
  10. lemma OAI.CircleConcentration.finite_orbit_cover line 101
  11. lemma OAI.CircleConcentration.orbitRadius_tendsto line 115
  12. def OAI.CircleConcentration.supportRadius line 125
  13. lemma OAI.CircleConcentration.orbitRadius_lt_supportRadius line 126
  14. lemma OAI.CircleConcentration.supportRadius_pos line 130
  15. lemma OAI.CircleConcentration.supportRadius_tendsto line 131
  16. def OAI.CircleConcentration.bump line 134
  17. lemma OAI.CircleConcentration.bump_continuous line 135
  18. lemma OAI.CircleConcentration.bump_nonneg line 136
  19. lemma OAI.CircleConcentration.bump_le_one line 137
  20. lemma OAI.CircleConcentration.bump_zero line 141
  21. lemma OAI.CircleConcentration.bump_eq_zero line 142
  22. lemma OAI.CircleConcentration.bump_pos line 146
  23. def OAI.CircleConcentration.partitionDenom line 151
  24. lemma OAI.CircleConcentration.partitionDenom_continuous line 152
  25. lemma OAI.CircleConcentration.partitionDenom_pos line 156
  26. lemma OAI.CircleConcentration.partitionDenom_le line 162
  27. def OAI.CircleConcentration.partition line 167
  28. lemma OAI.CircleConcentration.partition_continuous line 168
  29. lemma OAI.CircleConcentration.partition_nonneg line 170
  30. lemma OAI.CircleConcentration.partition_sum line 171
  31. lemma OAI.CircleConcentration.partition_zero_lower line 174
  32. def OAI.CircleConcentration.moveTerm line 182
  33. def OAI.CircleConcentration.movedDrop line 183
  34. def OAI.CircleConcentration.moveCorrection line 185
  35. lemma OAI.CircleConcentration.moveTerm_continuous line 187
  36. lemma OAI.CircleConcentration.movedDrop_continuous line 189
  37. lemma OAI.CircleConcentration.moveCorrection_continuous line 193
  38. lemma OAI.CircleConcentration.moveTerm_nonneg line 200
  39. lemma OAI.CircleConcentration.movedDrop_nonneg line 202
  40. lemma OAI.CircleConcentration.movedDrop_zero_off line 204
  41. lemma OAI.CircleConcentration.movedDrop_zero_lower line 208
  42. lemma OAI.CircleConcentration.moveTerm_sum line 214
  43. lemma OAI.CircleConcentration.moveCorrection_coboundary line 216
  44. lemma OAI.CircleConcentration.measurePreserving_sub line 234
  45. lemma OAI.CircleConcentration.integral_sub_circle line 236
  46. lemma OAI.CircleConcentration.moveTerm_integrable line 241
  47. lemma OAI.CircleConcentration.movedTerm_integrable line 244
  48. lemma OAI.CircleConcentration.movedDrop_integral line 247
  49. lemma OAI.CircleConcentration.moveCorrection_support line 257
  50. lemma OAI.CircleConcentration.moveCorrection_measure line 270