OAI/Analysis/RotationWeights/LogarithmicDrops.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CircleSampling.roundingWidth line 90
  2. lemma OAI.CircleSampling.roundingWidth_pos line 91
  3. lemma OAI.CircleSampling.roundingWidth_lt_one line 95
  4. lemma OAI.CircleSampling.phase_width_bounds line 100
  5. def OAI.CircleSampling.smoothDrop line 114
  6. def OAI.CircleSampling.smoothCorrection line 117
  7. def OAI.CircleSampling.integerDrop line 119
  8. def OAI.CircleSampling.concentratedDrop line 121
  9. def OAI.CircleSampling.totalCorrection line 122
  10. def OAI.CircleSampling.blockH line 125
  11. def OAI.CircleSampling.blockG line 126
  12. def OAI.CircleSampling.blockW line 127
  13. lemma OAI.CircleSampling.smoothDrop_continuous line 129
  14. lemma OAI.CircleSampling.smoothDrop_nonneg line 131
  15. lemma OAI.CircleSampling.smoothCorrection_measurable line 134
  16. lemma OAI.CircleSampling.concentratedDrop_continuous line 136
  17. lemma OAI.CircleSampling.concentratedDrop_nonneg line 138
  18. lemma OAI.CircleSampling.totalCorrection_measurable line 140
  19. lemma OAI.CircleSampling.blockH_continuous line 142
  20. lemma OAI.CircleSampling.blockH_nonneg line 143
  21. lemma OAI.CircleSampling.blockW_measurable line 144
  22. lemma OAI.CircleSampling.blockH_support line 145
  23. lemma OAI.CircleSampling.blockH_locallyFinite line 147
  24. lemma OAI.CircleSampling.smoothDrop_coboundary line 153
  25. lemma OAI.CircleSampling.totalCorrection_coboundary line 162
  26. lemma OAI.CircleSampling.block_coboundary line 168
  27. lemma OAI.CircleSampling.smoothDrop_zero line 173
  28. lemma OAI.CircleSampling.blockH_zero_lower line 177
  29. lemma OAI.CircleSampling.smoothDrop_integral line 185
  30. lemma OAI.CircleSampling.blockH_integral_lower line 195
  31. lemma OAI.CircleSampling.measure_nonzero_sum line 209
  32. lemma OAI.CircleSampling.measure_nonzero_add line 217
  33. lemma OAI.CircleSampling.smoothCorrection_measure line 224
  34. lemma OAI.CircleSampling.smoothDrop_measure line 231
  35. lemma OAI.CircleSampling.integerDrop_measure line 238
  36. lemma OAI.CircleSampling.totalCorrection_measure line 245
  37. lemma OAI.CircleSampling.blockG_measure line 256
  38. lemma OAI.CircleSampling.blockW_measure line 266
  39. lemma OAI.CircleSampling.summable_blockW_bound line 287
  40. lemma OAI.CircleSampling.blockG_support_sum line 300
  41. lemma OAI.CircleSampling.blockW_support_sum line 306