WindowPlacement.lean`

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem310.WindowPlacement.start line 12
Source documentation
Place windows in preorder, reserving g unused indices after each window.
```
def start (len : ℕ → ℕ) (g : ℕ) : ℕ → ℕ
  | 0 => 3
  | i + 1 => start len g i + len i + g
```
def OAI.Problem310.WindowPlacement.finish line 16
def OAI.Problem310.WindowPlacement.window line 18
def OAI.Problem310.WindowPlacement.lengthAt line 22
Source documentation
Extract a window length from a finite preorder list, using zero outside the list.
```
def lengthAt (L : List ℕ) (i : ℕ) : ℕ := L[i]?.getD 0
```
theorem OAI.Problem310.WindowPlacement.lengthAt_map_of_getElem? line 24
theorem OAI.Problem310.WindowPlacement.lengthAt_map_idxOf line 29
theorem OAI.Problem310.WindowPlacement.lengthAt_pos line 34
theorem OAI.Problem310.WindowPlacement.sum_lengthAt line 39
theorem OAI.Problem310.WindowPlacement.lengthAt_segment line 50
theorem OAI.Problem310.WindowPlacement.sum_lengthAt_segment line 59
Source documentation
Translate a consecutive preorder block's list sum into the prefix-sum interface used by the endpoint and resolution lemmas.
```
theorem sum_lengthAt_segment (pre block post : List ℕ) (g : ℕ) :
    (∑ k ∈ Finset.range block.length,
      (lengthAt (pre ++ block ++ post) (pre.length + k) + g)) =
      (block.map (fun r => r + g)).sum := by
…
```
Mentions: OAI.Problem310.WindowPlacement.lengthAt
theorem OAI.Problem310.WindowPlacement.start_zero line 80
theorem OAI.Problem310.WindowPlacement.start_succ line 82
theorem OAI.Problem310.WindowPlacement.start_mono line 85
theorem OAI.Problem310.WindowPlacement.three_le_start line 91
theorem OAI.Problem310.WindowPlacement.finish_add_one line 94
theorem OAI.Problem310.WindowPlacement.finish_mono line 101
Source documentation
Endpoints are nondecreasing even if some windows have length zero.
```
theorem finish_mono (len : ℕ → ℕ) (g : ℕ) : Monotone (finish len g) := by
…
```
Mentions: OAI.Problem310.WindowPlacement.finish
theorem OAI.Problem310.WindowPlacement.consecutive_gap line 109
theorem OAI.Problem310.WindowPlacement.gap_of_lt line 116
Source documentation
Every later window starts strictly beyond the earlier endpoint and its gap.
```
theorem gap_of_lt (len : ℕ → ℕ) (g : ℕ) {i j : ℕ} (hij : i < j) :
    finish len g i + g < start len g j := by
…
```
Mentions: OAI.Problem310.WindowPlacement.finish, OAI.Problem310.WindowPlacement.start
theorem OAI.Problem310.WindowPlacement.finish_lt_start line 122
theorem OAI.Problem310.WindowPlacement.start_le_finish line 127
theorem OAI.Problem310.WindowPlacement.finish_lt_of_lt line 132
theorem OAI.Problem310.WindowPlacement.finish_le_of_le line 136
theorem OAI.Problem310.WindowPlacement.finish_strictMono line 142
theorem OAI.Problem310.WindowPlacement.mem_window line 145
theorem OAI.Problem310.WindowPlacement.three_le_of_mem line 149
theorem OAI.Problem310.WindowPlacement.indices_separated line 153
theorem OAI.Problem310.WindowPlacement.disjoint_windows line 160
theorem OAI.Problem310.WindowPlacement.card_window line 170
theorem OAI.Problem310.WindowPlacement.card_windows line 177
Source documentation
Disjoint windows contribute exactly the sum of their lengths.
```
theorem card_windows (len : ℕ → ℕ) (g : ℕ) (S : Finset ℕ) :
    (S.biUnion (window len g)).card = ∑ i ∈ S, len i := by
…
```
Mentions: OAI.Problem310.WindowPlacement.window
theorem OAI.Problem310.WindowPlacement.card_equal_windows line 184
theorem OAI.Problem310.WindowPlacement.start_add line 193
Source documentation
Prefix-sum formula relative to any incoming edge.
```
theorem start_add (len : ℕ → ℕ) (g i m : ℕ) :
    start len g (i + m) = start len g i +
      ∑ k ∈ Finset.range m, (len (i + k) + g) := by
…
```
Mentions: OAI.Problem310.WindowPlacement.start
theorem OAI.Problem310.WindowPlacement.block_endpoint line 203
Source documentation
A consecutive child block's endpoint is exactly its total window and gap budget.
```
theorem block_endpoint (len : ℕ → ℕ) (g i m : ℕ) :
    finish len g (i + m) + g + 1 = start len g i +
      ∑ k ∈ Finset.range (m + 1), (len (i + k) + g) := by
…
```
Mentions: OAI.Problem310.WindowPlacement.finish, OAI.Problem310.WindowPlacement.start
theorem OAI.Problem310.WindowPlacement.block_endpoint_le line 209
theorem OAI.Problem310.WindowPlacement.local_endpoint_bound line 217
Source documentation
An endpoint anywhere in a child block satisfies the same padding bound; no positivity assumptions on individual list entries are necessary.
```
theorem local_endpoint_bound {len : ℕ → ℕ} {g i m r j : ℕ}
    (hbudget : (∑ k ∈ Finset.range (m + 1), (len (i + k) + g)) ≤ 2 * r + g)
    (hj : j ≤ i + m) :
    finish len g j + 1 ≤ start len g i + 2 * r := by
…
```
Mentions: OAI.Problem310.WindowPlacement.finish, OAI.Problem310.WindowPlacement.start
theorem OAI.Problem310.WindowPlacement.block_padding line 227
Source documentation
Convert a bound on the sum of a child block's padded lengths into the subtree-resolution bound used by the scale discretization.
```
theorem block_padding {len : ℕ → ℕ} {g i m r : ℕ}
    (hlen : 0 < len (i + m))
    (hbudget : (∑ k ∈ Finset.range (m + 1), (len (i + k) + g)) ≤ 2 * r + g) :
    finish len g (i + m) - start len g i + 1 ≤ 2 * r := by
…
```
Mentions: OAI.Problem310.WindowPlacement.finish, OAI.Problem310.WindowPlacement.start
theorem OAI.Problem310.WindowPlacement.local_resolution_bound line 238
Source documentation
Every grid in a child block has resolution controlled by the incoming window. This is in the additive form required by the common-representative bound.
```
theorem local_resolution_bound {len : ℕ → ℕ} {g i m r j n : ℕ}
    (hlen : 0 < len (i + m))
    (hbudget : (∑ k ∈ Finset.range (m + 1), (len (i + k) + g)) ≤ 2 * r + g)
    (hj : j ≤ i + m) (hn : start len g i ≤ n) :
    finish len g j + 2 ≤ n + (2 * r + 2) := by
…
```
Mentions: OAI.Problem310.WindowPlacement.start, OAI.Problem310.WindowPlacement.finish