OAI/Analysis/FourierLLogL/Paths/Checkpoint.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The uniform output path

  1. def OAI.FourierLLogL.Dyadic.Procedure.Paths.Run.Streak.wave line 19
  2. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Run.Streak.wave_combine line 22
  3. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Run.Streak.wave_bling line 28
  4. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Run.Streak.holds_tail line 40
  5. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Run.Streak.holds_inner line 88
  6. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Run.Streak.possible line 118