OAI/Analysis/IrrationalRotation/Sampling/ScalarSampling.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Invariant233.ScalarSampling.delta_nonneg line 12
  2. lemma OAI.Invariant233.ScalarSampling.delta_le_half line 15
  3. lemma OAI.Invariant233.ScalarSampling.cutoff_iff line 21
  4. lemma OAI.Invariant233.ScalarSampling.rawKernel_nonneg line 25
  5. lemma OAI.Invariant233.ScalarSampling.integral_rawKernel line 32
  6. lemma OAI.Invariant233.ScalarSampling.integral_sq_rawKernel line 43
  7. lemma OAI.Invariant233.ScalarSampling.rawKernel_eq_zero_of_not_mem_unit line 60
  8. theorem OAI.Invariant233.ScalarSampling.interval_integral_rawKernel line 74
  9. theorem OAI.Invariant233.ScalarSampling.interval_integral_sq_rawKernel line 83
  10. theorem OAI.Invariant233.ScalarSampling.integral_integral_rawKernel line 92
  11. theorem OAI.Invariant233.ScalarSampling.integral_inv_delta line 112
  12. theorem OAI.Invariant233.ScalarSampling.integral_integral_sq_rawKernel line 156
  13. theorem OAI.Invariant233.ScalarSampling.double_interval_integral_rawKernel line 178
  14. theorem OAI.Invariant233.ScalarSampling.double_interval_integral_sq_rawKernel line 192
  15. theorem OAI.Invariant233.ScalarSampling.interval_integral_circleKernel line 208
  16. theorem OAI.Invariant233.ScalarSampling.double_interval_integral_circleKernel line 222
  17. theorem OAI.Invariant233.ScalarSampling.double_interval_integral_sq_circleKernel line 236
  18. theorem OAI.Invariant233.ScalarSampling.averaged_circleKernel_bounds line 252
  19. theorem OAI.Invariant233.ScalarSampling.integral_sq_averaged_circleKernel line 259
  20. lemma OAI.Invariant233.ScalarSampling.manuscript_parameters line 273
  21. theorem OAI.Invariant233.ScalarSampling.manuscriptKernel_mass line 284
  22. theorem OAI.Invariant233.ScalarSampling.manuscriptKernel_secondMoment line 291
  23. lemma OAI.Invariant233.ScalarSampling.triangularKernel_sq line 301
  24. theorem OAI.Invariant233.ScalarSampling.interval_integral_triangularKernel line 305
  25. theorem OAI.Invariant233.ScalarSampling.triangularKernel_mass line 320
  26. theorem OAI.Invariant233.ScalarSampling.triangularKernel_secondMoment line 334
  27. theorem OAI.Invariant233.ScalarSampling.triangularKernel_averaged_secondMoment line 339