PackedWindowSpan.lean`

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem310.WindowRecursion.packedSpan line 9
Source documentation
Length of a list of windows packed with a fixed gap between consecutive windows, with no leading or trailing gap.
```
def packedSpan (g : ℕ) (L : List ℕ) : ℕ := L.sum + (L.length - 1) * g
```
theorem OAI.Problem310.WindowRecursion.packedSpan_nil line 11
theorem OAI.Problem310.WindowRecursion.packedSpan_singleton line 14
theorem OAI.Problem310.WindowRecursion.packedSpan_append line 17
theorem OAI.Problem310.WindowRecursion.packedSpan_cons line 26
theorem OAI.Problem310.WindowRecursion.packedSpan_flatten_replicate line 30
def OAI.Problem310.WindowRecursion.preorderLengths line 46
Source documentation
The deterministic list of incoming-window lengths in full preorder.
```
def preorderLengths (M g r₀ : ℕ) : ℕ → List ℕ
  | 0 => []
  | h + 1 => (List.replicate M (length M g r₀ (h + 1) :: preorderLengths M g r₀ h)).flatten
```
Mentions: OAI.Problem310.WindowRecursion.length
theorem OAI.Problem310.WindowRecursion.preorderLengths_zero line 50
theorem OAI.Problem310.WindowRecursion.preorderLengths_succ line 52
theorem OAI.Problem310.WindowRecursion.preorderLengths_succ_ne_nil line 56
theorem OAI.Problem310.WindowRecursion.packedSpan_preorderLengths line 64
Source documentation
The numeric recursive span is exactly the actual packed span of the preorder list; it is not merely a formal upper bound.
```
theorem packedSpan_preorderLengths (M g r₀ h : ℕ) (hM : 1 ≤ M) :
    packedSpan g (preorderLengths M g r₀ h) = span M g r₀ h := by
…
```
Mentions: OAI.Problem310.WindowRecursion.packedSpan, OAI.Problem310.WindowRecursion.preorderLengths, OAI.Problem310.WindowRecursion.span
theorem OAI.Problem310.WindowRecursion.threshold_le_of_mem_preorderLengths line 79
Source documentation
Every emitted window is at least the chosen entropy threshold.
```
theorem threshold_le_of_mem_preorderLengths (M g r₀ h r : ℕ)
    (hr : r ∈ preorderLengths M g r₀ h) : r₀ ≤ r := by
…
```
Mentions: OAI.Problem310.WindowRecursion.preorderLengths