AnchorFrames.lean`

28 declarations, 0 contain sorry, 0 declared as axioms

Full row and column orders extending the variable order. The raw carrier is the anchor / variable / dummy sum.

abbrev OAI.Problem348.AnchorFrames.Raw line 14
abbrev OAI.Problem348.AnchorFrames.AnchorOrder line 15
abbrev OAI.Problem348.AnchorFrames.RowOrder line 16
abbrev OAI.Problem348.AnchorFrames.ColOrder line 17

def OAI.Problem348.AnchorFrames.rowKey line 20

Source documentation

Coordinates for the row order: anchors, variables, dummy.

def rowKey {M : Type uM} {V : Type uV} {O : Type uO} : Raw M V O → RowOrder M V O
  | .inl (t, u, x) => .inlₗ (toLex (t, toLex (u, x)))
  | .inr (.inl v) => .inrₗ (.inlₗ v)
  | .inr (.inr x) => .inrₗ (.inrₗ x)

/-- Coordinates for the column order: anchors, dummy, variables. -/

Mentions: OAI.Problem348.AnchorFrames.Raw, OAI.Problem348.AnchorFrames.RowOrder

def OAI.Problem348.AnchorFrames.colKey line 26

Source documentation

Coordinates for the column order: anchors, dummy, variables.

def colKey {M : Type uM} {V : Type uV} {O : Type uO} : Raw M V O → ColOrder M V O
  | .inl (t, u, x) => .inlₗ (toLex (t, toLex (u, x)))
  | .inr (.inl v) => .inrₗ (.inrₗ v)
  | .inr (.inr x) => .inrₗ (.inlₗ x)

Mentions: OAI.Problem348.AnchorFrames.Raw, OAI.Problem348.AnchorFrames.ColOrder

def OAI.Problem348.AnchorFrames.rowEquiv line 31
def OAI.Problem348.AnchorFrames.colEquiv line 39
abbrev OAI.Problem348.AnchorFrames.rowOrder line 53
Source documentation
The full raw row order, suitable for local instance installation.
```
abbrev rowOrder : LinearOrder (Raw M V O) := LinearOrder.lift' rowKey (rowEquiv M V O).injective
```
Mentions: OAI.Problem348.AnchorFrames.Raw, OAI.Problem348.AnchorFrames.rowKey, OAI.Problem348.AnchorFrames.rowEquiv
abbrev OAI.Problem348.AnchorFrames.colOrder line 56
Source documentation
The full raw column order, suitable for local instance installation.
```
abbrev colOrder : LinearOrder (Raw M V O) := LinearOrder.lift' colKey (colEquiv M V O).injective
```
Mentions: OAI.Problem348.AnchorFrames.Raw, OAI.Problem348.AnchorFrames.colKey, OAI.Problem348.AnchorFrames.colEquiv
theorem OAI.Problem348.AnchorFrames.row_anchor_strictMono line 59
Source documentation
Arbitrary offsets in successive groups give increasing selected anchors.
```
theorem row_anchor_strictMono (t : M) (a : Fin 64 → O) :
    StrictMono (fun u => rowKey (M := M) (V := V) (.inl (t, u, a u))) := by
…
```
Mentions: OAI.Problem348.AnchorFrames.rowKey
theorem OAI.Problem348.AnchorFrames.col_anchor_strictMono line 67
theorem OAI.Problem348.AnchorFrames.row_anchor_lt_nonanchor line 75
theorem OAI.Problem348.AnchorFrames.col_anchor_lt_nonanchor line 79
theorem OAI.Problem348.AnchorFrames.row_variable_lt_dummy line 83
theorem OAI.Problem348.AnchorFrames.col_dummy_lt_variable line 87
theorem OAI.Problem348.AnchorFrames.row_variable_lt_variable line 91
theorem OAI.Problem348.AnchorFrames.col_variable_lt_variable line 95
theorem OAI.Problem348.AnchorFrames.row_not_nonanchor_lt_anchor line 100
Source documentation
The anchor region is an initial segment of the complete row axis.
```
theorem row_not_nonanchor_lt_anchor (t : M) (u : Fin 64) (a : O) (x : V ⊕ O) :
    ¬ rowKey (.inr x) < rowKey (.inl (t,u,a)) :=
…
```
Mentions: OAI.Problem348.AnchorFrames.rowKey
theorem OAI.Problem348.AnchorFrames.col_not_nonanchor_lt_anchor line 105
Source documentation
The anchor region is also an initial segment of the complete column axis.
```
theorem col_not_nonanchor_lt_anchor (t : M) (u : Fin 64) (a : O) (x : V ⊕ O) :
    ¬ colKey (.inr x) < colKey (.inl (t,u,a)) :=
…
```
Mentions: OAI.Problem348.AnchorFrames.colKey
theorem OAI.Problem348.AnchorFrames.row_group_le_of_lt line 110
Source documentation
Within one mode, increasing selected anchors have nondecreasing group labels.
```
theorem row_group_le_of_lt (t : M) (u v : Fin 64) (a b : O)
    (hab : rowKey (V := V) (.inl (t,u,a)) < rowKey (.inl (t,v,b))) : u ≤ v := by
…
```
Mentions: OAI.Problem348.AnchorFrames.rowKey
theorem OAI.Problem348.AnchorFrames.col_group_le_of_lt line 116
def OAI.Problem348.AnchorFrames.selectedRows line 123
Source documentation
Selected anchor rows after the full axis has been enumerated by Fin n.
```
def selectedRows {n : ℕ} (e : Fin n ≃o RowOrder M V O)
    (t : M) (a : Fin 64 → O) : Fin 64 → Fin n :=
…
```
Mentions: OAI.Problem348.AnchorFrames.RowOrder
def OAI.Problem348.AnchorFrames.selectedCols line 128
Source documentation
Selected anchor columns after the full axis has been enumerated by Fin n.
```
def selectedCols {n : ℕ} (e : Fin n ≃o ColOrder M V O)
    (t : M) (a : Fin 64 → O) : Fin 64 → Fin n :=
…
```
Mentions: OAI.Problem348.AnchorFrames.ColOrder
theorem OAI.Problem348.AnchorFrames.selectedRows_strictMono line 132
theorem OAI.Problem348.AnchorFrames.selectedCols_strictMono line 136
theorem OAI.Problem348.AnchorFrames.selectedRows_lt_nonanchor line 140
theorem OAI.Problem348.AnchorFrames.selectedCols_lt_nonanchor line 145