RowData.lean`

34 declarations, 0 contain sorry, 0 declared as axioms

Sorted finite row data, column fibres, and cardinality bounds

def OAI.Nagata.Workers.W10.LocalTupleSort.graph line 36
Source documentation
graph f produces the finset of pairs (f i, i) equipped with the lexicographic order.
```
def graph (f : Fin n → α) : Finset (α ×ₗ Fin n) :=
…
```
def OAI.Nagata.Workers.W10.LocalTupleSort.graph.proj line 42
Source documentation
Given p : α ×ₗ (Fin n) := (f i, i) with p ∈ graph f, graph.proj p is defined to be f i.
```
def graph.proj {f : Fin n → α} : graph f → α := fun p => p.1.1
…
```
Mentions: OAI.Nagata.Workers.W10.LocalTupleSort.graph
theorem OAI.Nagata.Workers.W10.LocalTupleSort.graph.card line 44
def OAI.Nagata.Workers.W10.LocalTupleSort.graphEquiv₁ line 52
Source documentation
graphEquiv₁ f is the natural equivalence between Fin n and graph f, mapping i to (f i, i).
```
def graphEquiv₁ (f : Fin n → α) : Fin n ≃ graph f where
…
```
Mentions: OAI.Nagata.Workers.W10.LocalTupleSort.graph
theorem OAI.Nagata.Workers.W10.LocalTupleSort.proj_equiv₁' line 63
def OAI.Nagata.Workers.W10.LocalTupleSort.graphEquiv₂ line 68
Source documentation
graphEquiv₂ f is an equivalence between Fin n and graph f that respects the order.
```
def graphEquiv₂ (f : Fin n → α) : Fin n ≃o graph f :=
…
```
Mentions: OAI.Nagata.Workers.W10.LocalTupleSort.graph
def OAI.Nagata.Workers.W10.LocalTupleSort.sort line 72
Source documentation
sort f is the permutation that orders Fin n according to the order of the outputs of f.
```
def sort (f : Fin n → α) : Equiv.Perm (Fin n) :=
…
```
theorem OAI.Nagata.Workers.W10.LocalTupleSort.graphEquiv₂_apply line 75
theorem OAI.Nagata.Workers.W10.LocalTupleSort.self_comp_sort line 79
theorem OAI.Nagata.Workers.W10.LocalTupleSort.monotone_proj line 82
theorem OAI.Nagata.Workers.W10.LocalTupleSort.monotone_sort line 87

theorem OAI.Nagata.Workers.W10.initial_rows_le_distribution line 102

Source documentation

Every earlier row contributes to the distribution count at the current size.

theorem initial_rows_le_distribution (N : ℕ → ℕ) (s i : ℕ) (hi : i < s)
    (horder : ∀ j, j ≤ i → N i ≤ N j) :
    i + 1 ≤ ((Finset.range s).filter fun j => N i ≤ N j).card := by
…

theorem OAI.Nagata.Workers.W10.ordered_row_bound line 115

Source documentation

The distribution bounds imply the manuscript's ordered row bound.

theorem ordered_row_bound (N : ℕ → ℕ) (s q m : ℕ)
    (horder : ∀ i < s, ∀ j ≤ i, N i ≤ N j)
    (hpos : ∀ i < s, 1 ≤ N i)
    (hsize : ∀ i < s, N i ≤ m)
    (hdistribution : ∀ t, 1 ≤ t → t ≤ m →
      ((Finset.range s).filter fun j => t ≤ N j).card ≤ q * (m - t + 1))
    (i : ℕ) (hi : i < s) : i + 1 ≤ q * (m - N i + 1) :=
…

theorem OAI.Nagata.Workers.W10.correction_exponent_bound line 126

Source documentation

The ordered row bound puts every correction monomial inside the allowed region.

theorem correction_exponent_bound (q m n i b ell : ℕ)
    (hsize : n ≤ m) (horder : i + 1 ≤ q * (m - n + 1))
    (hb : b < n) (hell : ell ≤ i) : b < m ∧ ell < q * (m - b) := by
…

theorem OAI.Nagata.Workers.W10.distributed_correction_exponent_bound line 136

Source documentation

Combined form, ready for use by the row-by-row interpolation construction.

theorem distributed_correction_exponent_bound (N : ℕ → ℕ) (s q m : ℕ)
    (horder : ∀ i < s, ∀ j ≤ i, N i ≤ N j)
    (hpos : ∀ i < s, 1 ≤ N i)
    (hsize : ∀ i < s, N i ≤ m)
    (hdistribution : ∀ t, 1 ≤ t → t ≤ m →
      ((Finset.range s).filter fun j => t ≤ N j).card ≤ q * (m - t + 1))
    (i b ell : ℕ) (hi : i < s) (hb : b < N i) (hell : ell ≤ i) :
    b < m ∧ ell < q * (m - b) :=
…

theorem OAI.Nagata.Workers.W10.distribution_card_permutation line 150

Source documentation

Reordering the complete row set preserves every distribution count.

theorem distribution_card_permutation {s : ℕ} (N : Fin s → ℕ)
    (σ : Equiv.Perm (Fin s)) (t : ℕ) :
    (Finset.univ.filter fun i => t ≤ N (σ i)).card =
      (Finset.univ.filter fun i => t ≤ N i).card := by
…

theorem OAI.Nagata.Workers.W10.fin_ordered_row_bound line 159

Source documentation

The zero-based ordered row inequality on a finite index type.

theorem fin_ordered_row_bound {s : ℕ} (N : Fin s → ℕ) (q m : ℕ)
    (horder : Antitone N) (hpos : ∀ i, 1 ≤ N i) (hsize : ∀ i, N i ≤ m)
    (hdistribution : ∀ t, 1 ≤ t → t ≤ m →
      (Finset.univ.filter fun j => t ≤ N j).card ≤ q * (m - t + 1))
    (i : Fin s) : i.val + 1 ≤ q * (m - N i + 1) := by
…

def OAI.Nagata.Workers.W10.ColumnFiber line 177
instance OAI.Nagata.Workers.W10.columnFiberDecidableEq line 180
instance OAI.Nagata.Workers.W10.columnFiberFintype line 185
theorem OAI.Nagata.Workers.W10.column_first_bounds line 194
def OAI.Nagata.Workers.W10.columnFiberEquiv line 204
Source documentation
The finite coefficient-index family is equivalent to the exact literal columns.
```
def columnFiberEquiv (d m : ℤ) (a Δ : ℝ) (hm : 0 ≤ m) (hd : 3 * m < d) :
    (Σ j : Fin ((d / 3).toNat + 1), ColumnFiber d m a Δ (j.val : ℤ)) ≃
      Column d m a Δ where
…
```
Mentions: OAI.Nagata.Workers.W10.ColumnFiber
def OAI.Nagata.Workers.W10.zeroColumnFiberEquiv line 225
Source documentation
A degree-zero fiber contains exactly the retained K=0 column.
```
def zeroColumnFiberEquiv (d m j : ℤ) (a Δ : ℝ) (hj : m < j) (hz : d - 3 * j = 0) :
    ColumnFiber d m a Δ j ≃ PUnit where
…
```
Mentions: OAI.Nagata.Workers.W10.ColumnFiber

def OAI.Nagata.Workers.W10.firstColumnFiberEquiv line 238

Source documentation

The first coefficient fiber has exactly the source's theta residue indices.

def firstColumnFiberEquiv (d m j : ℤ) (a Δ : ℝ) (hj0 : 0 ≤ j) (hjm : j ≤ m)
    (hU : firstLower d m j a Δ ∉ Set.range (Int.cast : ℤ → ℝ)) :
    ColumnFiber d m a Δ j ≃ Nagata.W09.thetaIndices (firstLower d m j a Δ) (commonDegree d m) := by
…

Mentions: OAI.Nagata.Workers.W10.ColumnFiber, OAI.Nagata.W09.thetaIndices

def OAI.Nagata.Workers.W10.positiveColumnFiberEquiv line 253

Source documentation

The positive high coefficient fiber has exactly its source theta indices.

def positiveColumnFiberEquiv (d m j : ℤ) (a Δ : ℝ) (hmj : m < j)
    (hjd : j ≤ d / 3) (hn : 0 < d - 3 * j)
    (hU : secondLower d j a Δ ∉ Set.range (Int.cast : ℤ → ℝ)) :
    ColumnFiber d m a Δ j ≃ Nagata.W09.thetaIndices (secondLower d j a Δ) (sourceDegree d j) := by
…

Mentions: OAI.Nagata.Workers.W10.ColumnFiber, OAI.Nagata.W09.thetaIndices

def OAI.Nagata.Workers.W10.rowHeights line 275
Source documentation
The represented heights of a genuine finite plane set.
```
def rowHeights (S : Finset (α × β)) : Finset β := by
…
```
def OAI.Nagata.Workers.W10.rowXs line 280
Source documentation
The first coordinates of a represented horizontal row.
```
def rowXs (S : Finset (α × β)) (K : β) : Finset α := by
…
```
theorem OAI.Nagata.Workers.W10.mem_rowXs line 284
theorem OAI.Nagata.Workers.W10.rowXs_nonempty line 297
theorem OAI.Nagata.Workers.W10.snd_mem_rowHeights line 304

theorem OAI.Nagata.Workers.W10.row_distribution_card line 310

Source documentation

A finite enumeration of actual represented heights preserves the row counts.

theorem row_distribution_card (S : Finset (α × β))
    (e : Fin (rowHeights S).card ≃ rowHeights S) (t : ℕ) :
    (Finset.univ.filter fun i => t ≤ (rowXs S (e i).val).card).card =
      ((rowHeights S).filter fun K => t ≤ (rowXs S K).card).card := by
…

Mentions: OAI.Nagata.Workers.W10.rowHeights, OAI.Nagata.Workers.W10.rowXs

def OAI.Nagata.Workers.W10.descendingRowPermutation line 334
Source documentation
Sort row sizes in nonincreasing order, with no restriction on ties.
```
def descendingRowPermutation {s : ℕ} (N : Fin s → ℕ) : Equiv.Perm (Fin s) :=
…
```
theorem OAI.Nagata.Workers.W10.descendingRowPermutation_antitone line 337

theorem OAI.Nagata.Workers.W10.exists_ordered_rows line 343

Source documentation

Every finite row family satisfying the distribution hypotheses admits an ordering satisfying the precise inequality needed by constructive interpolation.

theorem exists_ordered_rows {s : ℕ} (N : Fin s → ℕ) (q m : ℕ)
    (hpos : ∀ i, 1 ≤ N i) (hsize : ∀ i, N i ≤ m)
    (hdistribution : ∀ t, 1 ≤ t → t ≤ m →
      (Finset.univ.filter fun j => t ≤ N j).card ≤ q * (m - t + 1)) :
    ∃ σ : Equiv.Perm (Fin s), Antitone (N ∘ σ) ∧
      ∀ i : Fin s, i.val + 1 ≤ q * (m - N (σ i) + 1) := by
…