OAI/Analysis/FourierLLogL/Paths/Ribbon.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

The uniform output path

  1. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Beam.yield_zero line 17
  2. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Beam.yield_pos line 18
  3. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Beam.yield_add line 19
  4. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Beam.yield_sub line 22
  5. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Beam.single_yield line 26
  6. def OAI.FourierLLogL.Dyadic.Procedure.Paths.Run.Streak.weave line 39

    Source documentation

    One parity of output, sum of odd-numbered positions.

    def weave (x u : Grid M) : Path M → Paths.Vector M
  | [] => 0
  | [b] => duties x u b
  | b::_c::l => duties x u b + weave x u l

    Mentions: OAI.FourierLLogL.Dyadic.Grid, OAI.FourierLLogL.Dyadic.Procedure.Paths.Path, OAI.FourierLLogL.Dyadic.Procedure.Paths.Vector, OAI.FourierLLogL.Dyadic.Procedure.Paths.Run.Streak.b, OAI.FourierLLogL.Dyadic.Procedure.Paths.duties

  7. def OAI.FourierLLogL.Dyadic.Procedure.Paths.Run.Streak.hem line 44
  8. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Run.Streak.ribbon_eq line 47
  9. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Run.Streak.count_both line 58
  10. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Run.Streak.write_down line 66
  11. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Run.Streak.ribbon_pref line 98
  12. def OAI.FourierLLogL.Dyadic.Procedure.Paths.Run.Streak.bling line 143
  13. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Run.Streak.bling_share line 145
  14. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Run.Streak.bling_mean line 157
  15. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Run.Streak.ribbon_bound line 162