OAI/Analysis/IrrationalRotation/Sampling/ScalarSamplingVariation.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Invariant233.ScalarSampling.antitone_variation_Icc_le line 11
  2. theorem OAI.Invariant233.ScalarSampling.interval_indicator_variation_le line 36
  3. theorem OAI.Invariant233.ScalarSampling.rawKernel_le_height line 82
  4. theorem OAI.Invariant233.ScalarSampling.rawKernel_variation_le line 94
  5. theorem OAI.Invariant233.ScalarSampling.rawKernel_boundedVariation line 117
  6. theorem OAI.Invariant233.ScalarSampling.rawKernel_height_add_variation_le line 121
  7. lemma OAI.Invariant233.ScalarSampling.rawKernel_zero line 129
  8. lemma OAI.Invariant233.ScalarSampling.rawKernel_one line 133
  9. lemma OAI.Invariant233.ScalarSampling.circleKernel_eq_raw_on_unit line 146
  10. theorem OAI.Invariant233.ScalarSampling.circleKernel_variation_le line 155
  11. lemma OAI.Invariant233.ScalarSampling.manuscript_reciprocal_height line 162
  12. theorem OAI.Invariant233.ScalarSampling.manuscriptKernel_variation_le line 172
  13. theorem OAI.Invariant233.ScalarSampling.manuscriptKernel_le_height line 179
  14. theorem OAI.Invariant233.ScalarSampling.manuscriptKernel_height_add_variation_le line 185
  15. theorem OAI.Invariant233.ScalarSampling.manuscriptKernel_sup_le line 193
  16. theorem OAI.Invariant233.ScalarSampling.manuscriptKernel_BV_bound line 205
  17. theorem OAI.Invariant233.ScalarSampling.manuscriptKernel_BV_bound_ten line 217