OAI/MeasureTheory/DyadicAvoidance/WindowRecursion.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem310.WindowRecursion.span line 10

    Source documentation

    Total span occupied by the windows in a complete tree of the given height. At a bottom-level child there is no following subtree gap; at higher levels the incoming window is followed by one gap and the complete child subtree.

    def span (M g r₀ : ℕ) : ℕ → ℕ
  | 0 => 0
  | h + 1 =>
      M * (max r₀ (g + span M g r₀ h) +
        if h = 0 then 0 else g + span M g r₀ h) + (M - 1) * g

/-- Length of an incoming window whose parent has height `h + 1`.
The value at height zero is unused and is set equal to the threshold. -/
  2. def OAI.Problem310.WindowRecursion.length line 18

    Source documentation

    Length of an incoming window whose parent has height h + 1. The value at height zero is unused and is set equal to the threshold.

    def length (M g r₀ : ℕ) : ℕ → ℕ
  | 0 => r₀
  | h + 1 => max r₀ (g + span M g r₀ h)

/-- Span of one incoming-edge window and the subtree beneath that edge. -/

    Mentions: OAI.Problem310.WindowRecursion.span

  3. def OAI.Problem310.WindowRecursion.childSpan line 23

    Source documentation

    Span of one incoming-edge window and the subtree beneath that edge.

    def childSpan (M g r₀ h : ℕ) : ℕ :=
…
  4. theorem OAI.Problem310.WindowRecursion.span_zero line 26
  5. theorem OAI.Problem310.WindowRecursion.length_zero line 28
  6. theorem OAI.Problem310.WindowRecursion.length_succ line 30
  7. theorem OAI.Problem310.WindowRecursion.span_succ line 33
  8. theorem OAI.Problem310.WindowRecursion.childSpan_zero line 36
  9. theorem OAI.Problem310.WindowRecursion.span_one line 40
  10. theorem OAI.Problem310.WindowRecursion.childSpan_succ line 44
  11. theorem OAI.Problem310.WindowRecursion.span_succ_succ line 49
  12. theorem OAI.Problem310.WindowRecursion.threshold_le_length line 54
  13. theorem OAI.Problem310.WindowRecursion.gap_add_span_le_length line 59
  14. theorem OAI.Problem310.WindowRecursion.length_pos line 62
  15. theorem OAI.Problem310.WindowRecursion.length_le_childSpan line 65
  16. theorem OAI.Problem310.WindowRecursion.childSpan_le_twice_length line 70

    Source documentation

    The key padding estimate: an entire child block occupies no more than twice its incoming window length, independently of the size of the complete tree.

    theorem childSpan_le_twice_length (M g r₀ h : ℕ) :
    childSpan M g r₀ h ≤ 2 * length M g r₀ (h + 1) := by
…

    Mentions: OAI.Problem310.WindowRecursion.childSpan, OAI.Problem310.WindowRecursion.length

  17. theorem OAI.Problem310.WindowRecursion.childSpan_pos line 76
  18. theorem OAI.Problem310.WindowRecursion.childSpan_le_span line 80
  19. theorem OAI.Problem310.WindowRecursion.span_pos line 88
  20. theorem OAI.Problem310.WindowRecursion.span_le_length_succ line 92
  21. theorem OAI.Problem310.WindowRecursion.span_le_span_succ line 96
  22. theorem OAI.Problem310.WindowRecursion.monotone_span line 101
  23. theorem OAI.Problem310.WindowRecursion.monotone_length line 104