OAI/Analysis/FourierLLogL/Fourier/Kappa.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

The translation-averaged Haar kernel

  1. def OAI.FourierLLogL.Period.kappa line 12
  2. lemma OAI.FourierLLogL.Period.kappa_eq_mean line 15
  3. def OAI.FourierLLogL.Period.Step line 21
  4. def OAI.FourierLLogL.Period.P line 22
  5. def OAI.FourierLLogL.Period.hatK line 24
  6. lemma OAI.FourierLLogL.Period.step_split line 26
  7. lemma OAI.FourierLLogL.Period.haarH_step line 32
  8. lemma OAI.FourierLLogL.Period.step_twice line 39
  9. lemma OAI.FourierLLogL.Period.haarG_step line 44
  10. lemma OAI.FourierLLogL.Period.step_trans line 52
  11. lemma OAI.FourierLLogL.Period.step_mul line 56
  12. lemma OAI.FourierLLogL.Period.integrable_step line 61
  13. lemma OAI.FourierLLogL.Period.integral_step line 65
  14. lemma OAI.FourierLLogL.Period.pair_id line 71
  15. lemma OAI.FourierLLogL.Period.integrable_pair line 75
  16. lemma OAI.FourierLLogL.Period.integral_pair line 79
  17. lemma OAI.FourierLLogL.Period.kappa_eq line 87
  18. lemma OAI.FourierLLogL.Period.hatK_cont line 116
  19. lemma OAI.FourierLLogL.Period.hatK_neg line 117
  20. lemma OAI.FourierLLogL.Period.hatK_bound line 118
  21. lemma OAI.FourierLLogL.Period.hatK_zero line 119
  22. lemma OAI.FourierLLogL.Period.kappa_cont line 121
  23. lemma OAI.FourierLLogL.Period.kappa_neg line 127
  24. lemma OAI.FourierLLogL.Period.kappa_outside line 133
  25. lemma OAI.FourierLLogL.Period.kappa_bound line 138
  26. lemma OAI.FourierLLogL.Period.hatK_integral line 147
  27. lemma OAI.FourierLLogL.Period.hatK_inside line 170
  28. lemma OAI.FourierLLogL.Period.hatK_outside line 178
  29. def OAI.FourierLLogL.Period.constK line 184
  30. lemma OAI.FourierLLogL.Period.kappa_integral line 186