ExponentMatrices.lean`

20 declarations, 0 contain sorry, 0 declared as axioms

Exponent evaluation matrices, row spans, and rank

theorem OAI.Nagata.Workers.W12.span_restrictions_eq_top line 20

Source documentation

Surjectivity of evaluation from a span gives spanning evaluation rows.

theorem span_restrictions_eq_top {X : Type*} (g : I → X → R) (point : S → X)
    (hinterp : ∀ target : S → R, ∃ f : X → R,
      f ∈ Submodule.span R (Set.range g) ∧ (fun s => f (point s)) = target) :
    Submodule.span R (Set.range (fun i s => g i (point s))) = ⊤ := by
…

theorem OAI.Nagata.Workers.W12.mulVec_injective_of_span_rows_top line 58
Source documentation
A rectangular matrix whose row vectors span the column-coordinate space has injective multiplication on column vectors. The row set need not be finite.
```
theorem mulVec_injective_of_span_rows_top (A : Matrix I S R)
    (hspan : Submodule.span R (Set.range A) = ⊤) :
    Function.Injective A.mulVec := by
…
```

theorem OAI.Nagata.Workers.W12.evaluation_mulVec_injective line 82

Source documentation

Exact finite-matrix consequence of interpolation in the span of a family of functions. This applies to the monomial family of Section 04.

theorem evaluation_mulVec_injective {X : Type*} (g : I → X → R) (point : S → X)
    (hinterp : ∀ target : S → R, ∃ f : X → R,
      f ∈ Submodule.span R (Set.range g) ∧ (fun s => f (point s)) = target) :
    Function.Injective (Matrix.mulVec (fun i s => g i (point s))) :=
…

theorem OAI.Nagata.Workers.W12.evaluation_mulVec_injective_of_set_interpolation line 90

Source documentation

Set-indexed form, matching a polynomial space given as the span of an explicit set of monomials.

theorem evaluation_mulVec_injective_of_set_interpolation {X : Type*}
    (monomials : Set (X → R)) (point : S → X)
    (hinterp : ∀ target : S → R, ∃ f : X → R,
      f ∈ Submodule.span R monomials ∧ (fun s => f (point s)) = target) :
    Function.Injective
      (Matrix.mulVec (fun (f : monomials) s => (f : X → R) (point s))) := by
…

theorem OAI.Nagata.Workers.W12.planeEval_mem_monomialSpace line 114
Source documentation
A bivariate polynomial in the exact source span evaluates to a function in that same monomial span. This is a genuine polynomial-to-function bridge.
```
theorem planeEval_mem_monomialSpace {q m : ℕ} {p : MvPolynomial (Fin 2) ℂ}
    (hp : p ∈ polynomialSpace q m) : planeEval p ∈ monomialSpace q m := by
…
```
def OAI.Nagata.Workers.W12.B0 line 159
Source documentation
Literal matrix in eq:limiting-matrix: row (ell,b), column (j,K), entry K^ell*j^b. Both index types are the finite source constructions.
```
def B0 (d : ℤ) (q m : ℕ) (a delta : ℝ) :
    Matrix (JetIndex q m) (Column d (m : ℤ) a delta) ℂ :=
…
```
theorem OAI.Nagata.Workers.W12.B0_apply line 163

theorem OAI.Nagata.Workers.W12.B0_column_nonempty line 171

Source documentation

Under the source's positive degree and nonintegral endpoint conditions, the actual matrix has a column. This is proved from the integer interval itself.

theorem B0_column_nonempty (d : ℤ) (m : ℕ) (a delta : ℝ)
    (hd : 3 * (m : ℤ) < d)
    (hU : firstLower d (m : ℤ) 0 a delta ∉ Set.range (Int.cast : ℤ → ℝ)) :
    Nonempty (Column d (m : ℤ) a delta) := by
…

def OAI.Nagata.Workers.W12.columnToComplex line 179
Source documentation
Inclusion of a genuine exponent column into the coordinatewise complex image.
```
def columnToComplex (d m : ℤ) (a delta : ℝ) (col : Column d m a delta) :
    Nagata.W29.complexSet (exponentSet d m a delta) := by
…
```
Mentions: OAI.Nagata.W29.complexSet
theorem OAI.Nagata.Workers.W12.columnToComplex_bijective line 186
Source documentation
Standard complex inclusion gives a bijection, not a quotient losing columns.
```
theorem columnToComplex_bijective (d m : ℤ) (a delta : ℝ) :
    Function.Bijective (columnToComplex d m a delta) := by
…
```
Mentions: OAI.Nagata.Workers.W12.columnToComplex
def OAI.Nagata.Workers.W12.columnComplexEquiv line 200
Source documentation
Explicit equivalence between the genuine integer columns and interpolation's complex finite set. Its map is the ordinary ℤ²→ℂ² inclusion.
```
def columnComplexEquiv (d m : ℤ) (a delta : ℝ) :
    Column d m a delta ≃ Nagata.W29.complexSet (exponentSet d m a delta) :=
…
```
Mentions: OAI.Nagata.W29.complexSet
theorem OAI.Nagata.Workers.W12.columnComplexEquiv_val line 205

theorem OAI.Nagata.Workers.W12.B0_mulVec_apply line 224

Source documentation

Actual matrix multiplication is the coefficient-weighted monomial sum.

theorem B0_mulVec_apply (d : ℤ) (q m : ℕ) (a delta : ℝ)
    (v : Column d (m : ℤ) a delta → ℂ) (row : JetIndex q m) :
    (B0 d q m a delta).mulVec v row =
      ∑ col : Column d (m : ℤ) a delta,
        v col * ((col.val.2 : ℂ) ^ row.2.val * (col.val.1 : ℂ) ^ row.1.val) := by
…

Mentions: OAI.Nagata.Workers.W12.B0

theorem OAI.Nagata.Workers.W12.B0_mulVec_eq_zero_iff line 236

Source documentation

Vanishing of the actual matrix map is exactly the entire finite family of coefficient equations, with no rows or degree-zero columns dropped.

theorem B0_mulVec_eq_zero_iff (d : ℤ) (q m : ℕ) (a delta : ℝ)
    (v : Column d (m : ℤ) a delta → ℂ) :
    (B0 d q m a delta).mulVec v = 0 ↔
      ∀ row : JetIndex q m,
        (∑ col : Column d (m : ℤ) a delta,
          v col * ((col.val.2 : ℂ) ^ row.2.val * (col.val.1 : ℂ) ^ row.1.val)) = 0 := by
…

Mentions: OAI.Nagata.Workers.W12.B0

theorem OAI.Nagata.Workers.W12.exists_common_small_parameter line 264

Source documentation

Two eventual properties near zero from the right hold simultaneously at some positive parameter below any prescribed positive bound.

theorem exists_common_small_parameter (P Q : ℝ → Prop)
    (hP : ∀ᶠ τ in 𝓝[>] (0 : ℝ), P τ)
    (hQ : ∀ᶠ τ in 𝓝[>] (0 : ℝ), Q τ)
    {epsilon : ℝ} (hepsilon : 0 < epsilon) :
    ∃ τ : ℝ, 0 < τ ∧ τ < epsilon ∧ P τ ∧ Q τ := by
…

theorem OAI.Nagata.Workers.W12.coefficient_kernel_contradiction line 278

Source documentation

A genuine coefficient vector cannot be both nonzero in the kernel and subject to injectivity at the same sufficiently small positive parameter.

theorem coefficient_kernel_contradiction
    (d : ℤ) (q m : ℕ) (a delta : ℝ)
    (B : ℝ → Matrix (JetIndex q m) (Column d (m : ℤ) a delta) ℂ)
    (hinjective : ∀ᶠ τ in 𝓝[>] (0 : ℝ), Function.Injective (B τ).mulVec)
    (hkernel : ∀ᶠ τ in 𝓝[>] (0 : ℝ),
      ∃ v : Column d (m : ℤ) a delta → ℂ,
        v ≠ 0 ∧ (B τ).mulVec v = 0) : False := by
…

theorem OAI.Nagata.Workers.W12.jet_monomial_range line 304

Source documentation

The finite jet row labels enumerate exactly the monomials of P_{q,m}.

theorem jet_monomial_range (q m : ℕ) :
    Set.range (fun row : JetIndex q m => monomial row.1.val row.2.val) =
      {f | ∃ b < m, ∃ l < q * (m - b), f = monomial b l} := by
…

theorem OAI.Nagata.Workers.W12.B0_eq_evaluationMatrix line 316
Source documentation
Entrywise identification with evaluation rows, including the source order K^ell*j^b rather than the polynomial-function convention j^b*K^ell.
```
theorem B0_eq_evaluationMatrix (d : ℤ) (q m : ℕ) (a delta : ℝ) :
    B0 d q m a delta =
      (fun row col => monomial row.1.val row.2.val
        (Nagata.W29.complexPoint col.val)) := by
…
```
Mentions: OAI.Nagata.Workers.W12.B0, OAI.Nagata.W29.complexPoint

theorem OAI.Nagata.Workers.W12.B0_mulVec_injective_of_interpolation line 324

Source documentation

Interpolation on the exponent column set implies injectivity of the matrix action.

theorem B0_mulVec_injective_of_interpolation (d : ℤ) (q m : ℕ) (a delta : ℝ)
    (hinterp : ∀ v : Nagata.W29.complexSet (exponentSet d (m : ℤ) a delta) → ℂ,
      ∃ p ∈ polynomialSpace q m,
        ∀ z : Nagata.W29.complexSet (exponentSet d (m : ℤ) a delta),
          planeEval p z.val = v z) :
    Function.Injective (B0 d q m a delta).mulVec := by
…

Mentions: OAI.Nagata.W29.complexSet, OAI.Nagata.Workers.W12.B0

theorem OAI.Nagata.Workers.W12.B0_mulVec_injective line 364

Source documentation

Full column rank of the actual finite exponent matrix, assuming only the numeric parameter hypotheses used in the manuscript's polygon and integer count. There is no interpolation, rank, span, geometric, or arbitrary-set hypothesis.

theorem B0_mulVec_injective (d : ℤ) (q m : ℕ) (rho a delta lam : ℝ)
    (ha : 0 < a) (hm : 0 < m) (hrho : 0 ≤ rho) (hdelta : 0 ≤ delta)
    (hlam : 0 < lam) (hlam1 : lam < 1)
    (hratio : 3 * ((d : ℝ) - 3 * (m : ℝ)) = (m : ℝ) * rho)
    (hslack : rho + delta * rho / 9 < lam * a - 9 * (1 - lam))
    (hcoef : 2 * a + a ^ 2 / 9 = (q : ℝ))
    (hmargin : 1 ≤ (q : ℝ) * (1 - lam) * m) :
    Function.Injective (B0 d q m a delta).mulVec := by
…

Mentions: OAI.Nagata.Workers.W12.B0