OAI/Analysis/FourierLLogL/Fourier/Haar.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

Delayed Haar shifts on real intervals

  1. def OAI.FourierLLogL.Period.box line 12
  2. def OAI.FourierLLogL.Period.haarH line 14
  3. def OAI.FourierLLogL.Period.haarG line 18
  4. lemma OAI.FourierLLogL.Period.measurableH line 20
  5. lemma OAI.FourierLLogL.Period.measurableG line 23
  6. lemma OAI.FourierLLogL.Period.H_of_left line 27
  7. lemma OAI.FourierLLogL.Period.H_of_right line 31
  8. lemma OAI.FourierLLogL.Period.H_outside line 35
  9. lemma OAI.FourierLLogL.Period.H_bound line 40
  10. lemma OAI.FourierLLogL.Period.G_outside line 47
  11. lemma OAI.FourierLLogL.Period.G_bound line 56
  12. def OAI.FourierLLogL.Period.side line 64
  13. lemma OAI.FourierLLogL.Period.side_pos line 66
  14. lemma OAI.FourierLLogL.Period.side_le line 68
  15. lemma OAI.FourierLLogL.Period.pow_mul_side line 70
  16. lemma OAI.FourierLLogL.Period.side_succ line 72
  17. def OAI.FourierLLogL.Period.lft line 74
  18. lemma OAI.FourierLLogL.Period.cell_in_top line 76
  19. lemma OAI.FourierLLogL.Period.norm_mem_box line 92
  20. def OAI.FourierLLogL.Period.coeffH line 100
  21. def OAI.FourierLLogL.Period.jump line 103
  22. def OAI.FourierLLogL.Period.haarLayer line 106
  23. def OAI.FourierLLogL.Period.shift line 109
  24. def OAI.FourierLLogL.Period.modρ line 112
  25. def OAI.FourierLLogL.Period.maxShift line 114
  26. def OAI.FourierLLogL.Period.density line 117
  27. def OAI.FourierLLogL.Period.usable line 119
  28. def OAI.FourierLLogL.Period.UnitTreeBound line 124

    Source documentation

    A cut dyadic statement on one top. Used only at levels B polynomial in log d.

    def UnitTreeBound : Prop :=
…
  29. lemma OAI.FourierLLogL.Period.jump_outside line 132
  30. lemma OAI.FourierLLogL.Period.shift_outside line 135
  31. lemma OAI.FourierLLogL.Period.measurable_mod line 141
  32. lemma OAI.FourierLLogL.Period.measurable_jump_comp line 148
  33. lemma OAI.FourierLLogL.Period.measurable_shift_comp line 157
  34. lemma OAI.FourierLLogL.Period.measurable_maxShift_comp line 163
  35. lemma OAI.FourierLLogL.Period.bounded_jump line 169
  36. lemma OAI.FourierLLogL.Period.bounded_haarLayer line 184
  37. lemma OAI.FourierLLogL.Period.bounded_shift line 191