WindowDataExistence.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem310.WindowConstruction.lengths line 15
Source documentation
Actual window lengths, in the finite tree preorder.
```
def lengths (q d g r₀ : ℕ) : List ℕ :=
…
```
def OAI.Problem310.WindowConstruction.lengthAt line 18
lemma OAI.Problem310.WindowConstruction.lengthAt_edgeRank line 20
lemma OAI.Problem310.WindowConstruction.length_preorderLengths line 27

theorem OAI.Problem310.WindowConstruction.descendant_endpoint_bound line 33

Source documentation

Every descendant endpoint lies within twice the incoming window length.

theorem descendant_endpoint_bound {q d g r₀ : ℕ} (hq : 1 ≤ q)
    {P Q : List (Fin q)} (hP : ValidWindowEdge d P) (hQ : ValidWindowEdge d Q)
    (hpref : P.IsPrefix Q) :
    finish (lengthAt q d g r₀) g (edgeRank d Q) + 1 ≤
      start (lengthAt q d g r₀) g (edgeRank d P) +
        2 * WindowRecursion.length q g r₀ (d + 1 - P.length) := by
…

Mentions: OAI.Problem310.ValidWindowEdge, OAI.Problem310.WindowConstruction.lengthAt, OAI.Problem310.WindowRecursion.length

def OAI.Problem310.WindowConstruction.windowData line 75
Source documentation
The complete deterministic windows exist with any prescribed positive uniform threshold and gap.
```
def windowData (q d g r₀ : ℕ) (hq : 1 ≤ q) (hr₀ : 1 ≤ r₀) :
    WindowData q d g r₀ where
…
```
Mentions: OAI.Problem310.WindowData
theorem OAI.Problem310.WindowConstruction.exists_windowData line 106