Interpolation.lean`

27 declarations, 0 contain sorry, 0 declared as axioms

Constructive interpolation on finite horizontal rows

theorem OAI.Nagata.W01.RowLagrange.product_natDegree_le line 24
Source documentation
Degree bound for a finite product of ordinary linear factors.
```
theorem product_natDegree_le {ι : Type*} (s : Finset ι) (K : ι → F) :
    (∏ i ∈ s, (X - C (K i))).natDegree ≤ s.card := by
…
```
def OAI.Nagata.W01.RowLagrange.basis line 34
theorem OAI.Nagata.W01.RowLagrange.basis_eval_self line 37
theorem OAI.Nagata.W01.RowLagrange.basis_eval_other line 46
theorem OAI.Nagata.W01.RowLagrange.basis_natDegree_le line 54
def OAI.Nagata.W01.RowLagrange.interpolate line 58
theorem OAI.Nagata.W01.RowLagrange.interpolate_eval line 61
theorem OAI.Nagata.W01.RowLagrange.interpolate_degree_lt line 72
abbrev OAI.Nagata.W01.Plane line 99
def OAI.Nagata.W01.monomial line 101
def OAI.Nagata.W01.monomialSpace line 103
theorem OAI.Nagata.W01.monomial_mem line 106

theorem OAI.Nagata.W01.separable_mem line 111

Source documentation

A product of two univariate polynomials has the advertised monomial support.

theorem separable_mem {q m : ℕ} (p Q : ℂ[X])
    (h : ∀ b ∈ p.support, ∀ l ∈ Q.support, b < m ∧ l < q * (m-b)) :
    (fun z : Plane => p.eval z.1 * Q.eval z.2) ∈ monomialSpace q m := by
…

Mentions: OAI.Nagata.W01.Plane, OAI.Nagata.W01.monomialSpace

def OAI.Nagata.W01.rowPrefix line 133
theorem OAI.Nagata.W01.rowPrefix_eval line 136
theorem OAI.Nagata.W01.rowPrefix_eval_earlier line 140
theorem OAI.Nagata.W01.rowPrefix_eval_ne_zero line 145
theorem OAI.Nagata.W01.rowPrefix_natDegree_le line 150

theorem OAI.Nagata.W01.exists_row_polynomial line 155

Source documentation

Ordinary interpolation, with the degree bound retained even for an empty row.

theorem exists_row_polynomial (xs : Finset ℂ) (v : ℂ → ℂ) :
    ∃ p : ℂ[X], p.degree < xs.card ∧ ∀ x ∈ xs, p.eval x = v x := by
…

theorem OAI.Nagata.W01.correction_mem line 161

Source documentation

Each row correction belongs to the exact staircase of allowed monomials.

theorem correction_mem {q m n : ℕ} (K : ℕ → ℂ) (xs : Finset ℂ) (p : ℂ[X])
    (hp : p.degree < xs.card) (hcard : xs.card ≤ m)
    (horder : n + 1 ≤ q * (m - xs.card + 1)) :
    (fun z : Plane => p.eval z.1 * (rowPrefix K n).eval z.2) ∈ monomialSpace q m := by
…

Mentions: OAI.Nagata.W01.Plane, OAI.Nagata.W01.rowPrefix, OAI.Nagata.W01.monomialSpace

theorem OAI.Nagata.W01.interpolate_ordered_rows line 181

Source documentation

Constructive interpolation on finitely many ordered rows. The explicit ordered-row bound is derived from the manuscript row counts separately.

theorem interpolate_ordered_rows (q m s : ℕ) (K : ℕ → ℂ) (xs : ℕ → Finset ℂ)
    (hK : ∀ i < s, ∀ j < s, K i = K j → i = j)
    (hcard : ∀ i < s, (xs i).card ≤ m)
    (horder : ∀ i < s, i + 1 ≤ q * (m - (xs i).card + 1))
    (v : Plane → ℂ) :
    ∃ f ∈ monomialSpace q m, ∀ i < s, ∀ x ∈ xs i, f (x, K i) = v (x, K i) := by
…

Mentions: OAI.Nagata.W01.Plane, OAI.Nagata.W01.monomialSpace

theorem OAI.Nagata.W01.interpolate_fin_rows line 222

Source documentation

The same construction with rows indexed by Fin s.

theorem interpolate_fin_rows (q m s : ℕ) (K : Fin s → ℂ)
    (xs : Fin s → Finset ℂ) (hK : Function.Injective K)
    (hcard : ∀ i, (xs i).card ≤ m)
    (horder : ∀ i, i.val + 1 ≤ q * (m - (xs i).card + 1))
    (v : Plane → ℂ) :
    ∃ f ∈ monomialSpace q m, ∀ i, ∀ x ∈ xs i, f (x, K i) = v (x, K i) := by
…

Mentions: OAI.Nagata.W01.Plane, OAI.Nagata.W01.monomialSpace

def OAI.Nagata.W01.planeEval line 247
Source documentation
Evaluation in two actual polynomial indeterminates.
```
def planeEval (p : MvPolynomial (Fin 2) ℂ) : Plane → ℂ :=
…
```
Mentions: OAI.Nagata.W01.Plane
def OAI.Nagata.W01.polynomialSpace line 251
Source documentation
The corresponding subspace inside the actual bivariate polynomial ring.
```
def polynomialSpace (q m : ℕ) : Submodule ℂ (MvPolynomial (Fin 2) ℂ) :=
…
```
theorem OAI.Nagata.W01.exists_polynomialSpace_of_mem line 256
Source documentation
Realization preserves the exact span of permitted bivariate monomials.
```
theorem exists_polynomialSpace_of_mem {q m : ℕ} {f : Plane → ℂ}
    (hf : f ∈ monomialSpace q m) :
    ∃ p ∈ polynomialSpace q m, planeEval p = f := by
…
```
Mentions: OAI.Nagata.W01.Plane, OAI.Nagata.W01.monomialSpace, OAI.Nagata.W01.polynomialSpace, OAI.Nagata.W01.planeEval

theorem OAI.Nagata.W01.interpolate_fin_rows_polynomial line 277

Source documentation

Ordered-row interpolation inside the actual bivariate polynomial ring.

theorem interpolate_fin_rows_polynomial (q m s : ℕ) (K : Fin s → ℂ)
    (xs : Fin s → Finset ℂ) (hK : Function.Injective K)
    (hcard : ∀ i, (xs i).card ≤ m)
    (horder : ∀ i, i.val + 1 ≤ q * (m - (xs i).card + 1))
    (v : Plane → ℂ) :
    ∃ p ∈ polynomialSpace q m, ∀ i, ∀ x ∈ xs i,
      planeEval p (x, K i) = v (x, K i) := by
…

Mentions: OAI.Nagata.W01.Plane, OAI.Nagata.W01.polynomialSpace, OAI.Nagata.W01.planeEval

theorem OAI.Nagata.W01.exists_mvPolynomial_of_mem line 289
Source documentation
The function-space formulation has actual bivariate polynomial representatives.
```
theorem exists_mvPolynomial_of_mem {q m : ℕ} {f : Plane → ℂ}
    (hf : f ∈ monomialSpace q m) :
    ∃ p : MvPolynomial (Fin 2) ℂ, planeEval p = f := by
…
```
Mentions: OAI.Nagata.W01.Plane, OAI.Nagata.W01.monomialSpace, OAI.Nagata.W01.planeEval