OAI/Analysis/FourierLLogL/Paths/Trip.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.FourierLLogL.Dyadic.Procedure.Paths.Path line 16
2. def OAI.FourierLLogL.Dyadic.Procedure.Paths.winds line 18
3. def OAI.FourierLLogL.Dyadic.Procedure.Paths.curl line 19
4. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.curl_unit line 21
5. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.curl_sq line 22
6. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.fair_av line 23
7. structure OAI.FourierLLogL.Dyadic.Procedure.Paths.Fit line 27
8. structure OAI.FourierLLogL.Dyadic.Procedure.Paths.Climb line 32
9. structure OAI.FourierLLogL.Dyadic.Procedure.Paths.Ideal line 37
10. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.jump_ideal line 42
11. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Climb.child line 49
12. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Ideal.kill_eq line 54
13. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Ideal.kill_nonneg line 57
14. def OAI.FourierLLogL.Dyadic.Procedure.Paths.Trip line 62

    Source documentation

    deterministic integrity along a plateau list.

    def Trip (x : Grid M) (s : Scene M) : Path M → Prop
      | [] => Fit s ∧ x∈s.here.block M
      | b::l =>
        b.pre=s ∧ Ideal b.pre b.post ∧ Trip x (winds b) l

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

15. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.trip_head line 67
16. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.stream_child line 78
17. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.trip_stream line 89
18. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.trip_cut line 98
19. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.heav_bit line 107
20. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Gi_half line 110
21. def OAI.FourierLLogL.Dyadic.Procedure.Paths.blow line 120
22. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.trip_delay line 122
23. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.trip_final line 132
24. def OAI.FourierLLogL.Dyadic.Procedure.Paths.subtotal line 144
25. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.subtotal_nil line 146
26. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.subtotal_cons line 147
27. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.subtotal_app line 149
28. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.trip_subtotal line 152
29. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.trip_nonneg line 158
30. def OAI.FourierLLogL.Dyadic.Procedure.Paths.fullKills line 165
31. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.trip_K line 167