OAI/Analysis/FourierLLogL/Paths/Frost.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

The uniform output path

  1. def OAI.FourierLLogL.Dyadic.Procedure.Paths.Lens.quest line 21
  2. def OAI.FourierLLogL.Dyadic.Procedure.Paths.Lens.dusk line 24
  3. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Lens.stipend line 27
  4. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Lens.dusk_tally line 52
  5. def OAI.FourierLLogL.Dyadic.Procedure.Paths.Lens.ease line 66
  6. def OAI.FourierLLogL.Dyadic.Procedure.Paths.Lens.shifted line 67
  7. def OAI.FourierLLogL.Dyadic.Procedure.Paths.Lens.enters line 70
  8. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Lens.last_lag line 74
  9. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Lens.face_fire line 113
  10. def OAI.FourierLLogL.Dyadic.Procedure.Paths.coldScore line 146
  11. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.cold_share line 149
  12. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.cold_one line 161
  13. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.cold_mean line 167
  14. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.fire_pref line 185
  15. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.frosty_portion line 214