OAI/Analysis/FourierLLogL/Paths/Flash.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

The uniform output path

  1. structure OAI.FourierLLogL.Dyadic.Procedure.Paths.Beam.Lamp line 19

    Source documentation

    Camera anchored at a jumping post.

    structure Lamp (M : ℕ) where
…
  2. def OAI.FourierLLogL.Dyadic.Procedure.Paths.Beam.Lamp.glint line 26
  3. def OAI.FourierLLogL.Dyadic.Procedure.Paths.Beam.Lamp.first line 28
  4. def OAI.FourierLLogL.Dyadic.Procedure.Paths.Beam.Lamp.second line 30
  5. def OAI.FourierLLogL.Dyadic.Procedure.Paths.Beam.Lamp.start line 32
  6. def OAI.FourierLLogL.Dyadic.Procedure.Paths.Beam.Lamp.delayed line 33
  7. def OAI.FourierLLogL.Dyadic.Procedure.Paths.Beam.Lamp.carry line 36

    Source documentation

    update of accumulated same-parity output.

    def carry (e : Lamp M) (r t : Bool) (z : Grid M) :=
…

    Mentions: OAI.FourierLLogL.Dyadic.Procedure.Paths.Beam.Lamp, OAI.FourierLLogL.Dyadic.Grid

  8. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Beam.Lamp.flash_cell line 39
  9. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Beam.Lamp.flash line 120
  10. def OAI.FourierLLogL.Dyadic.Procedure.Paths.Beam.Lamp.lit line 149
  11. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Beam.Lamp.start_cost line 151
  12. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Beam.Lamp.delayed_cost line 170