OAI/Analysis/FourierLLogL/Edges/Fringe.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

Thin parts of a grid interval

  1. def OAI.FourierLLogL.Dyadic.Procedure.reach line 14
  2. def OAI.FourierLLogL.Dyadic.Procedure.gateWidth line 15
  3. lemma OAI.FourierLLogL.Dyadic.Procedure.reach_pos line 17
  4. lemma OAI.FourierLLogL.Dyadic.Procedure.gate_pos line 18
  5. def OAI.FourierLLogL.Dyadic.Procedure.extreme line 21

    Source documentation

    all b steps child

    def extreme (p : Node) (b : Bool) : ℕ → Node
| 0 => p
| m+1 => (extreme p b m).child b

    Mentions: OAI.FourierLLogL.Dyadic.Node

  6. lemma OAI.FourierLLogL.Dyadic.Procedure.child_depth line 25
  7. lemma OAI.FourierLLogL.Dyadic.Procedure.extreme_depth line 27
  8. lemma OAI.FourierLLogL.Dyadic.Procedure.extreme_length line 34
  9. lemma OAI.FourierLLogL.Dyadic.Procedure.extreme_below line 37
  10. lemma OAI.FourierLLogL.Dyadic.Procedure.extreme_valid line 42
  11. lemma OAI.FourierLLogL.Dyadic.Procedure.extreme_left line 48
  12. lemma OAI.FourierLLogL.Dyadic.Procedure.extreme_right line 55
  13. def OAI.FourierLLogL.Dyadic.Procedure.strip line 65

    Source documentation

    strips of width 2^-l p about the two edges of both children of p; empty if the strip width needs more bits than available.

    def strip (p : Node) (i : ℕ) (b c : Bool) :=
…

    Mentions: OAI.FourierLLogL.Dyadic.Node

  14. lemma OAI.FourierLLogL.Dyadic.Procedure.strip_depth line 68
  15. lemma OAI.FourierLLogL.Dyadic.Procedure.strip_valid line 70
  16. lemma OAI.FourierLLogL.Dyadic.Procedure.strip_below_child line 73
  17. lemma OAI.FourierLLogL.Dyadic.Procedure.strip_below line 75
  18. lemma OAI.FourierLLogL.Dyadic.Procedure.strip_length line 78
  19. def OAI.FourierLLogL.Dyadic.Procedure.flanked line 81
  20. def OAI.FourierLLogL.Dyadic.Procedure.lanes line 84
  21. def OAI.FourierLLogL.Dyadic.Procedure.edgeW line 86
  22. def OAI.FourierLLogL.Dyadic.Procedure.hazard line 90
  23. def OAI.FourierLLogL.Dyadic.Procedure.surcharge line 92
  24. lemma OAI.FourierLLogL.Dyadic.Procedure.surcharge_nonneg line 95
  25. lemma OAI.FourierLLogL.Dyadic.Procedure.flank_in line 101
  26. def OAI.FourierLLogL.Dyadic.Procedure.spotted line 106

    Source documentation

    A property measurable in depth l. Does not require l≤M.

    def spotted (p : Grid M → Prop) (l : ℕ) :=
…

    Mentions: OAI.FourierLLogL.Dyadic.Grid

  27. lemma OAI.FourierLLogL.Dyadic.Procedure.flanked_at line 109
  28. lemma OAI.FourierLLogL.Dyadic.Procedure.prob_under line 118
  29. lemma OAI.FourierLLogL.Dyadic.Procedure.flank_prob line 131
  30. lemma OAI.FourierLLogL.Dyadic.Procedure.hazard_rule line 151