OAI/Analysis/FourierLLogL/Fourier/Dirichlet.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Comparing the Fourier projections to the averaged Haar kernel

  1. def OAI.FourierLLogL.Period.centerWin line 12
  2. def OAI.FourierLLogL.Period.ang line 14
  3. lemma OAI.FourierLLogL.Period.phase_trig line 16
  4. lemma OAI.FourierLLogL.Period.phase_sub line 21
  5. def OAI.FourierLLogL.Period.dirichlet line 27
  6. lemma OAI.FourierLLogL.Period.dirichlet_cont line 30
  7. lemma OAI.FourierLLogL.Period.dirichlet_bound line 34
  8. lemma OAI.FourierLLogL.Period.dirichlet_succ line 40
  9. lemma OAI.FourierLLogL.Period.dirichlet_sin line 62
  10. lemma OAI.FourierLLogL.Period.sin_posabs line 74
  11. lemma OAI.FourierLLogL.Period.dirichlet_id line 81
  12. lemma OAI.FourierLLogL.Period.cot_error line 97
  13. def OAI.FourierLLogL.Period.κfactor line 122
  14. lemma OAI.FourierLLogL.Period.κfactor_bound line 124
  15. def OAI.FourierLLogL.Period.diffK line 132

    Source documentation

    Dirichlet profile minus rescaled approximate Hilbert profile modulated by sine.

    def diffK (δ : ℝ) (N : ℕ) (t : ℝ) : ℂ :=
…
  16. theorem OAI.FourierLLogL.Period.diffK_major line 136