OAI/Analysis/FourierLLogL/Paths/Tilt.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

The uniform output path

  1. abbrev OAI.FourierLLogL.Dyadic.Procedure.Paths.Face line 18
  2. def OAI.FourierLLogL.Dyadic.Procedure.Paths.part line 19
  3. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.part_bounded line 20
  4. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.part_zero line 23
  5. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.part_add line 24
  6. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.part_diff line 26
  7. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.part_mul line 28
  8. def OAI.FourierLLogL.Dyadic.Procedure.Paths.slide line 32

    Source documentation

    Local Huber function on a window of length 10 b.

    private def slide (w x : ℝ) := if x < -w then -w else if w < x then w else x
  9. def OAI.FourierLLogL.Dyadic.Procedure.Paths.smooth line 33
  10. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.slide_range line 35
  11. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.slide_inner line 39
  12. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.smooth_inner line 43
  13. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.slide_pay line 46
  14. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.smooth_mid line 54
  15. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.smooth_nonneg line 60
  16. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.smooth_lip line 64
  17. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.sq_lip line 78
  18. def OAI.FourierLLogL.Dyadic.Procedure.Paths.tilt line 84
  19. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.tilt_lip line 85
  20. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.tilt_bounds line 96
  21. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.tilt_rise line 104
  22. def OAI.FourierLLogL.Dyadic.Procedure.Paths.guarded line 119
  23. def OAI.FourierLLogL.Dyadic.Procedure.Paths.prize line 122
  24. def OAI.FourierLLogL.Dyadic.Procedure.Paths.frosty line 123
  25. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.prize_norm line 125
  26. structure OAI.FourierLLogL.Dyadic.Procedure.Paths.Lens line 132

    Source documentation

    analyzing scalar path with a chosen signed component

    structure Lens (M : ℕ) where
…
  27. def OAI.FourierLLogL.Dyadic.Procedure.Paths.Lens.dot line 137
  28. def OAI.FourierLLogL.Dyadic.Procedure.Paths.Lens.cash line 138
  29. def OAI.FourierLLogL.Dyadic.Procedure.Paths.Lens.coin line 139
  30. def OAI.FourierLLogL.Dyadic.Procedure.Paths.Lens.hero line 140
  31. def OAI.FourierLLogL.Dyadic.Procedure.Paths.Lens.flow line 141
  32. def OAI.FourierLLogL.Dyadic.Procedure.Paths.Lens.swing line 143
  33. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Lens.hero_walk line 146
  34. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Lens.dot_walk line 151
  35. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Lens.dot_limit line 155
  36. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Lens.hero_limit line 158
  37. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Lens.coin_flow line 162
  38. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Lens.swing_flow line 178
  39. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Lens.hero_drain line 193