OAI/Analysis/FourierLLogL/Paths/Launch.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

The uniform output path

  1. def OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.Cast line 20

    Source documentation

    Path additionally follows birth rules.

    def Cast (j J : ℕ) (f : Grid M → ℝ) (s : Scene M) : Path M → Prop
| [] => s.Safe j J f
| b::l => b.pre=s ∧ (∃ k, Following j J f (ran b.pre b.post k)) ∧ Cast j J f (winds b) l

    Mentions: OAI.FourierLLogL.Dyadic.Grid, OAI.FourierLLogL.Dyadic.Procedure.Scene, OAI.FourierLLogL.Dyadic.Procedure.Paths.Path, OAI.FourierLLogL.Dyadic.Procedure.Paths.winds

  2. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.stream_cast line 24
  3. def OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.quarrel line 32
  4. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.quarrel_chart line 35
  5. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.quarrel_concat line 41
  6. def OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.oiled line 47
  7. def OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.heroPlot line 50
  8. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.oil_hero line 52
  9. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.still_head line 56
  10. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.oily_cons line 66
  11. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.birth_just line 73
  12. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.still_rec line 85
  13. def OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.ringing line 133
  14. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.live_rec line 136