Rows.lean`

31 declarations, 0 contain sorry, 0 declared as axioms

Integer and complex rows, slices, and exponent interpolation; Ordered integer rows of finite sets

def OAI.Nagata.W29.rowPositions line 14
def OAI.Nagata.W29.rowHeights line 17
def OAI.Nagata.W29.largeRows line 19
theorem OAI.Nagata.W29.mem_rowPositions line 22
theorem OAI.Nagata.W29.rowPositions_eq_empty_of_not_mem line 30
theorem OAI.Nagata.W29.mem_largeRows line 39
Source documentation
Positive threshold rows automatically have a represented height. This identifies the finite filter with the manuscript's quantification over all ℤ.
```
@[simp] theorem mem_largeRows (S : Finset (ℤ × ℤ)) (t : ℕ) (ht : 1 ≤ t)
    (K : ℤ) : K ∈ largeRows S t ↔ t ≤ (rowPositions S K).card := by
…
```
Mentions: OAI.Nagata.W29.largeRows, OAI.Nagata.W29.rowPositions

theorem OAI.Nagata.W29.row_card_le line 52

Source documentation

A slice of width at most m λ < m contains at most m integer positions.

theorem row_card_le (S : Finset (ℤ × ℤ)) (m : ℕ) (lam : ℝ)
    (hm : 0 < m) (hlam : lam < 1) (lo hi : ℤ → ℝ)
    (hinterval : ∀ K ∈ rowHeights S, lo K ≤ hi K)
    (hcontain : ∀ K, ∀ j ∈ rowPositions S K,
      lo K ≤ (j : ℝ) ∧ (j : ℝ) ≤ hi K)
    (hwidth : ∀ K ∈ rowHeights S, hi K - lo K ≤ (m : ℝ) * lam)
    (K : ℤ) : (rowPositions S K).card ≤ m := by
…

Mentions: OAI.Nagata.W29.rowHeights, OAI.Nagata.W29.rowPositions

theorem OAI.Nagata.W29.largeRows_card_le line 68

Source documentation

The spare endpoint in the lattice count is absorbed by q(1-λ)m ≥ 1.

theorem largeRows_card_le (S : Finset (ℤ × ℤ)) (q m : ℕ)
    (lam U A B : ℝ) (hA : 0 ≤ A) (hB : 0 ≤ B)
    (hAB : A + B = (q : ℝ))
    (hmargin : 1 ≤ (q : ℝ) * (1 - lam) * m)
    (lo hi : ℤ → ℝ)
    (hinterval : ∀ K ∈ rowHeights S, lo K ≤ hi K)
    (hcontain : ∀ K, ∀ j ∈ rowPositions S K,
      lo K ≤ (j : ℝ) ∧ (j : ℝ) ≤ hi K)
    (hwidth : ∀ K ∈ rowHeights S, hi K - lo K ≤ (m : ℝ) * lam)
    (hprofile : ∀ s : ℝ, 0 ≤ s → s ≤ (m : ℝ) * lam →
      ∀ K ∈ rowHeights S, s ≤ hi K - lo K →
        U - A * ((m : ℝ) * lam - s) ≤ (K : ℝ) ∧
…

Mentions: OAI.Nagata.W29.rowHeights, OAI.Nagata.W29.rowPositions

theorem OAI.Nagata.W29.integer_rows_of_polygon line 137

Source documentation

Both integer-row estimates for a finite set enclosed in the translated polygon. a is the manuscript's ρ_*; its defining numerical identity is the explicit hypothesis hcoef. No row-count hypothesis occurs.

theorem integer_rows_of_polygon (S : Finset (ℤ × ℤ)) (q m : ℕ)
    (a lam U : ℝ) (ha : 0 < a) (hm : 0 < m)
    (hlam : 0 < lam) (hlam1 : lam < 1)
    (hcoef : 2 * a + a ^ 2 / 9 = (q : ℝ))
    (hmargin : 1 ≤ (q : ℝ) * (1 - lam) * m)
    (hpolygon : ∀ p ∈ S,
      Nagata.W04.InPolygon a ((m : ℝ) * lam) (p.1 : ℝ) ((p.2 : ℝ) - U)) :
    (∀ K : ℤ, (rowPositions S K).card ≤ m) ∧
    (∀ t : ℕ, 1 ≤ t → t ≤ m → (largeRows S t).card ≤ q * (m - t + 1)) := by
…

Mentions: OAI.Nagata.W04.InPolygon, OAI.Nagata.W29.rowPositions, OAI.Nagata.W29.largeRows

def OAI.Nagata.W29.complexPoint line 194
Source documentation
Coordinatewise standard inclusion ℤ² → ℂ².
```
def complexPoint (p : ℤ × ℤ) : ℂ × ℂ := ((p.1 : ℂ), (p.2 : ℂ))
```
def OAI.Nagata.W29.complexSet line 196
theorem OAI.Nagata.W29.complexPoint_injective line 200
theorem OAI.Nagata.W29.complexSet_card line 211
Source documentation
The standard inclusion preserves the entire finite column count.
```
theorem complexSet_card (S : Finset (ℤ × ℤ)) : (complexSet S).card = S.card := by
…
```
Mentions: OAI.Nagata.W29.complexSet
def OAI.Nagata.W29.complexColumnEquiv line 216
Source documentation
Actual exponent columns and their complex-image columns are equivalent.
```
def complexColumnEquiv (S : Finset (ℤ × ℤ)) : S ≃ complexSet S := by
…
```
Mentions: OAI.Nagata.W29.complexSet
theorem OAI.Nagata.W29.complexColumnEquiv_val line 229
theorem OAI.Nagata.W29.rowHeights_complexSet line 232
theorem OAI.Nagata.W29.rowXs_complexSet line 239
theorem OAI.Nagata.W29.row_card_complexSet line 260
theorem OAI.Nagata.W29.distribution_card_complexSet line 269
Source documentation
The threshold distributions agree, including threshold zero when restricted to represented heights as in both finite-set definitions.
```
theorem distribution_card_complexSet (S : Finset (ℤ × ℤ)) (t : ℕ) :
    ((Nagata.Workers.W10.rowHeights (complexSet S)).filter
      fun K => t ≤ (Nagata.Workers.W10.rowXs (complexSet S) K).card).card =
    (largeRows S t).card := by
…
```
Mentions: OAI.Nagata.Workers.W10.rowHeights, OAI.Nagata.W29.complexSet, OAI.Nagata.Workers.W10.rowXs, OAI.Nagata.W29.largeRows
theorem OAI.Nagata.W29.polygon_dilation line 305
Source documentation
Positive dilation of the actual enclosing polygon, retaining arbitrary λ.
```
theorem polygon_dilation (a lam c x y : ℝ) (hc : 0 < c) :
    Nagata.W04.InPolygon a (c * lam) (c * x) (c * y) ↔
      Nagata.W04.InPolygon a lam x y :=
…
```
Mentions: OAI.Nagata.W04.InPolygon

theorem OAI.Nagata.W29.integer_rows_of_raw_exponents line 313

Source documentation

Any finite set satisfying the explicit exponent interval conditions obeys both manuscript row estimates. This is independent of the analytic/geometric claim that those intervals index a basis of the required section space.

theorem integer_rows_of_raw_exponents (S : Finset (ℤ × ℤ)) (q m : ℕ)
    (d h rho a delta lam : ℝ)
    (ha : 0 < a) (hm : 0 < m) (hrho : 0 ≤ rho) (hdelta : 0 ≤ delta)
    (hlam : 0 < lam) (hlam1 : lam < 1)
    (hdegree : h = 3 * (d - 3 * (m : ℝ))) (hratio : h = (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)
    (hexponent : ∀ p ∈ S, Nagata.ExponentEnclosure.rawExponent
      d (m : ℝ) h a delta (p.1 : ℝ) (p.2 : ℝ)) :
    (∀ K : ℤ, (rowPositions S K).card ≤ m) ∧
    (∀ t : ℕ, 1 ≤ t → t ≤ m → (largeRows S t).card ≤ q * (m - t + 1)) := by
…

Mentions: OAI.Nagata.ExponentEnclosure.rawExponent, OAI.Nagata.W29.rowPositions, OAI.Nagata.W29.largeRows

theorem OAI.Nagata.Workers.W10.interpolate_finset_plane_data line 355

Source documentation

Interpolation of plane-valued data on a genuine finite plane set.

theorem interpolate_finset_plane_data (q m : ℕ) (S : Finset Plane)
    (hsize : ∀ K ∈ rowHeights S, (rowXs S K).card ≤ m)
    (hdistribution : ∀ t, 1 ≤ t → t ≤ m →
      ((rowHeights S).filter fun K => t ≤ (rowXs S K).card).card ≤ q * (m - t + 1))
    (v : Plane → ℂ) :
    ∃ p ∈ polynomialSpace q m, ∀ z ∈ S, planeEval p z = v z := by
…

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

theorem OAI.Nagata.Workers.W10.interpolate_finset_polynomial line 388

Source documentation

Every function on the actual finite set has a permitted polynomial extension.

theorem interpolate_finset_polynomial (q m : ℕ) (S : Finset Plane)
    (hsize : ∀ K ∈ rowHeights S, (rowXs S K).card ≤ m)
    (hdistribution : ∀ t, 1 ≤ t → t ≤ m →
      ((rowHeights S).filter fun K => t ≤ (rowXs S K).card).card ≤ q * (m - t + 1))
    (v : S → ℂ) :
    ∃ p ∈ polynomialSpace q m, ∀ z : S, planeEval p z.val = v z := by
…

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

theorem OAI.Nagata.W29.finite_exponent_rows line 410

theorem OAI.Nagata.W29.interpolate_integer_finset line 440

Source documentation

Genuine integer-point row bounds imply interpolation after the standard coordinatewise inclusion in the complex affine plane.

theorem interpolate_integer_finset (q m : ℕ) (S : Finset (ℤ × ℤ))
    (hsize : ∀ K, (rowPositions S K).card ≤ m)
    (hdistribution : ∀ t, 1 ≤ t → t ≤ m →
      (largeRows S t).card ≤ q * (m - t + 1))
    (v : complexSet S → ℂ) :
    ∃ p ∈ Nagata.W01.polynomialSpace q m,
      ∀ z : complexSet S, Nagata.W01.planeEval p z.val = v z := by
…

Mentions: OAI.Nagata.W29.rowPositions, OAI.Nagata.W29.largeRows, OAI.Nagata.W29.complexSet, OAI.Nagata.W01.polynomialSpace, OAI.Nagata.W01.planeEval

def OAI.Nagata.W29.sourceOffsets line 471
Source documentation
The exponents in Θ(τ^(x₀−x_i)e^x), not the point exponents x_i themselves.
```
noncomputable def sourceOffsets (x : Fin 9 → ℝ) : Fin 9 → ℝ := fun i => 1 / 2 - x i
```
theorem OAI.Nagata.W29.sourceOffsets_injective line 473
theorem OAI.Nagata.W29.sourceOffsets_bounds line 480
theorem OAI.Nagata.W29.sourceOffsets_sum line 488

theorem OAI.Nagata.W29.finite_exponent_interpolation line 507

Source documentation

Section 4's interpolation conclusion on the actual finite integer exponent set, viewed through the usual embedding in ℂ². All parameter hypotheses remain explicit, and no geometric jet-space hypothesis is hidden in the statement.

theorem finite_exponent_interpolation (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)
    (v : complexSet (Nagata.FiniteExponents.exponentSet d (m : ℤ) a delta) → ℂ) :
    ∃ p ∈ Nagata.W01.polynomialSpace q m,
      ∀ z : complexSet (Nagata.FiniteExponents.exponentSet d (m : ℤ) a delta),
        Nagata.W01.planeEval p z.val = v z := by
…

Mentions: OAI.Nagata.W29.complexSet, OAI.Nagata.FiniteExponents.exponentSet, OAI.Nagata.W01.polynomialSpace, OAI.Nagata.W01.planeEval

theorem OAI.Nagata.W29.affinePolynomialGradient_surjective line 536