WindowData.lean`

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem310.ValidWindowEdge line 10
Source documentation
An edge is identified with the nonempty path to its child.
```
def ValidWindowEdge {q : ℕ} (d : ℕ) (P : List (Fin q)) : Prop :=
…
```
structure OAI.Problem310.WindowData line 17
Source documentation
Deterministic window interface shared by the finite router and its geometric/probabilistic estimates. q is the TOTAL number of children. Only the two ordering comparisons actually used by routing are required; a preorder construction can supply them from its general rank gap bound.
```
structure WindowData (q d g r₀ : ℕ) where
…
```
abbrev OAI.Problem310.WindowData.length line 41
def OAI.Problem310.WindowData.window line 43
def OAI.Problem310.WindowData.testIndex line 45
lemma OAI.Problem310.WindowData.start_le_end line 47
lemma OAI.Problem310.WindowData.card_window line 52
lemma OAI.Problem310.WindowData.testIndex_mem line 59
lemma OAI.Problem310.WindowData.testIndex_three line 67
lemma OAI.Problem310.WindowData.testIndex_injective line 73
lemma OAI.Problem310.WindowData.testIndex_padding line 80
Source documentation
Every tested point sees at most 2*r+2 finest-grid exponent levels.
```
lemma testIndex_padding (P : List (Fin q)) (hP : ValidWindowEdge d P)
    (k : Fin (W.length P)) :
    W.bstar P + 2 ≤ W.testIndex P k + (2 * W.length P + 2) := by
…
```
Mentions: OAI.Problem310.ValidWindowEdge
def OAI.Problem310.WindowData.indices line 88
Source documentation
The global finite-index set may include every edge window.
```
def indices : Set ℕ := {n | ∃ P : List (Fin q), ValidWindowEdge d P ∧ n ∈ W.window P}
```
Mentions: OAI.Problem310.ValidWindowEdge
lemma OAI.Problem310.WindowData.indices_positive line 90