OrderedSampledSelection.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The sampled selection on increasing host enumerations

The ten order assumptions of the concrete sampler follow from the independent row and column enumerations. No order or entry certificate remains as a hypothesis of sampledSelection_valid.

theorem OAI.Problem348.OrderedHost.sampledAxisConditions line 21
Source documentation
The actual row and column enumerations meet every sampler order condition.
```
theorem sampledAxisConditions (h : ℕ) :
    SampledSelection.AxisConditions (rowIndex h) (columnIndex h) := by
…
```
Mentions: OAI.Problem348.OrderedHost.rowIndex, OAI.Problem348.OrderedHost.columnIndex
def OAI.Problem348.OrderedHost.sampledSelection line 46
Source documentation
The three-seed selection in the concrete matrix of the prescribed size.
```
def sampledSelection {h : ℕ} (hh : 1 ≤ h) (z u v : Fin (2 ^ h)) :
    GuardedPath.Selection (size h) :=
…
```
Mentions: OAI.Problem348.GuardedPath.Selection, OAI.Problem348.OrderedHost.size
theorem OAI.Problem348.OrderedHost.sampledSelection_valid line 52
Source documentation
The actual sampled path and anchor frames are valid without extra inputs.
```
theorem sampledSelection_valid {h : ℕ} (hh : 1 ≤ h) (z u v : Fin (2 ^ h)) :
    (sampledSelection hh z u v).Valid
      (SelectedAnchor.matrix (rowIndex h) (columnIndex h)) h :=
…
```
Mentions: OAI.Problem348.OrderedHost.sampledSelection, OAI.Problem348.OrderedHost.rowIndex, OAI.Problem348.OrderedHost.columnIndex