CoefficientBlocks.lean`

28 declarations, 0 contain sorry, 0 declared as axioms

Parameterized coefficient blocks, their bases, evaluation, and interpolation

abbrev OAI.Nagata.Workers.W10.tauPower line 21
Source documentation
Positive real powers embedded into the actual complex multiplier field.
```
abbrev tauPower (τ s : ℝ) : ℂ := ((τ ^ s : ℝ) : ℂ)
```
theorem OAI.Nagata.Workers.W10.tauPower_ne_zero line 23
theorem OAI.Nagata.Workers.W10.tauPower_add line 26
theorem OAI.Nagata.Workers.W10.tauPower_zpow line 30
theorem OAI.Nagata.Workers.W10.tauPower_div line 35

theorem OAI.Nagata.Workers.W10.normalMinusMarkedMultiplier_source line 40

Source documentation

The displayed multiplier of A is exactly minus tau to rho.

theorem normalMinusMarkedMultiplier_source {τ : ℝ} (hτ : 0 < τ) (s ρ : ℝ) :
    normalMinusMarkedMultiplier (tauPower τ ((s + ρ) / 3)) (-tauPower τ s) =
      -tauPower τ ρ := by
…

Mentions: OAI.Nagata.Workers.W10.tauPower

theorem OAI.Nagata.Workers.W10.firstSourceMultiplier line 55

Source documentation

Literal low-branch multiplier and exponent, including its sign character.

theorem firstSourceMultiplier {τ : ℝ} (hτ : 0 < τ) (s ρ : ℝ) (d m j : ℤ) :
    tauPower τ ((s + ρ) / 3) ^ (d - 3 * m) *
      normalMinusMarkedMultiplier (tauPower τ ((s + ρ) / 3)) (-tauPower τ s) ^ (m - j) =
    (-1 : ℂ) ^ (m - j) *
      tauPower τ (((d - 3 * m : ℤ) : ℝ) * ((s + ρ) / 3) + ((m - j : ℤ) : ℝ) * ρ) := by
…

Mentions: OAI.Nagata.Workers.W10.tauPower

theorem OAI.Nagata.Workers.W10.secondSourceMultiplier line 66

Source documentation

The high-branch source multiplier has no sign character.

theorem secondSourceMultiplier {τ : ℝ} (hτ : 0 < τ) (s ρ : ℝ) (d j : ℤ) :
    tauPower τ ((s + ρ) / 3) ^ (d - 3 * j) =
      tauPower τ (((d - 3 * j : ℤ) : ℝ) * ((s + ρ) / 3)) :=
…

Mentions: OAI.Nagata.Workers.W10.tauPower

theorem OAI.Nagata.Workers.W10.firstSourceEndpoint line 71
theorem OAI.Nagata.Workers.W10.secondSourceEndpoint line 77

theorem OAI.Nagata.Workers.W10.interpolate_distributed_rows line 95

Source documentation

Interpolation after sorting the represented rows by decreasing size. Each represented row is required to be nonempty, as in the manuscript.

theorem interpolate_distributed_rows (q m s : ℕ) (K : Fin s → ℂ)
    (xs : Fin s → Finset ℂ) (hK : Function.Injective K)
    (hpos : ∀ i, 1 ≤ (xs i).card) (hsize : ∀ i, (xs i).card ≤ m)
    (hdistribution : ∀ t, 1 ≤ t → t ≤ m →
      (Finset.univ.filter fun i => t ≤ (xs i).card).card ≤ q * (m - t + 1))
    (v : Nagata.W01.Plane → ℂ) :
    ∃ f ∈ Nagata.W01.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

theorem OAI.Nagata.Workers.W10.interpolate_distributed_rows_polynomial line 113

Source documentation

The interpolating function has a genuine bivariate polynomial representative.

theorem interpolate_distributed_rows_polynomial (q m s : ℕ) (K : Fin s → ℂ)
    (xs : Fin s → Finset ℂ) (hK : Function.Injective K)
    (hpos : ∀ i, 1 ≤ (xs i).card) (hsize : ∀ i, (xs i).card ≤ m)
    (hdistribution : ∀ t, 1 ≤ t → t ≤ m →
      (Finset.univ.filter fun i => t ≤ (xs i).card).card ≤ q * (m - t + 1))
    (v : Nagata.W01.Plane → ℂ) :
    ∃ p ∈ Nagata.W01.polynomialSpace q m,
      ∀ i, ∀ x ∈ xs i, Nagata.W01.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.Workers.W10.sourceCoefficientEquiv_apply line 137

def OAI.Nagata.Workers.W10.firstSourceThetaEquiv line 160

Source documentation

Low blocks use the exact centered theta multiplier, including the sign.

def firstSourceThetaEquiv {τ : ℝ} (hτ : 0 < τ) (s ρ Δ x₀ : ℝ)
    (d m j : ℤ) (hs : s = 9 * x₀ - Δ) (hj : j ≤ m) :
    sourceBlock (τ : ℂ) (tauPower τ ((s + ρ) / 3)) (-tauPower τ s) d m j ≃ₗ[ℂ]
    automorphicSections (τ : ℂ) (commonDegree d m)
      ((-1 : ℂ) ^ (m - j) * tauPower τ (firstLower d m j ρ Δ + x₀ * (commonDegree d m : ℝ))) :=
…

Mentions: OAI.Nagata.Workers.W10.sourceBlock, OAI.Nagata.Workers.W10.tauPower

def OAI.Nagata.Workers.W10.secondSourceThetaEquiv line 176

Source documentation

Positive high blocks have the exact centered theta multiplier with epsilon1.

def secondSourceThetaEquiv {τ : ℝ} (hτ : 0 < τ) (s ρ Δ x₀ : ℝ)
    (d m j : ℤ) (hs : s = 9 * x₀ - Δ) (hj : m < j) :
    sourceBlock (τ : ℂ) (tauPower τ ((s + ρ) / 3)) (-tauPower τ s) d m j ≃ₗ[ℂ]
    automorphicSections (τ : ℂ) (sourceDegree d j)
      ((1 : ℂ) * tauPower τ (secondLower d j ρ Δ + x₀ * (sourceDegree d j : ℝ))) :=
…

Mentions: OAI.Nagata.Workers.W10.sourceBlock, OAI.Nagata.Workers.W10.tauPower

def OAI.Nagata.Workers.W10.zeroSourceThetaEquiv line 190

Source documentation

The literal degree-zero tip is exactly the genuine constant section space.

def zeroSourceThetaEquiv (τ s ρ : ℝ) (d m j : ℤ) (hj : m < j) (hz : d - 3 * j = 0) :
    sourceBlock (τ : ℂ) (tauPower τ ((s + ρ) / 3)) (-tauPower τ s) d m j ≃ₗ[ℂ]
      automorphicSections (τ : ℂ) 0 1 :=
…

Mentions: OAI.Nagata.Workers.W10.sourceBlock, OAI.Nagata.Workers.W10.tauPower

def OAI.Nagata.Workers.W10.polynomialBasisFromSourceBases line 218

theorem OAI.Nagata.Workers.W10.polynomialBasisFromSourceBases_local line 226

Source documentation

Explicit local expression after both the section-image equivalence and literal-column reindexing. The only piecewise factor is the actual Pi power.

theorem polynomialBasisFromSourceBases_local
    (j : Fin ((d / 3).toNat + 1)) (K : ColumnFiber d (m : ℤ) a Δ (j.val : ℤ))
    (z₀ x y : ℂ) :
    Nagata.W20.localScalar
      (polynomialBasisFromSourceBases τ γL γP d m a Δ P hd hP hPfin b
        (columnFiberEquiv d (m : ℤ) a Δ (Int.natCast_nonneg m) hd ⟨j, K⟩)) z₀ x y =
      (if (j.val : ℤ) ≤ (m : ℤ) then (b j K).val (z₀ * Complex.exp x)
        else P (z₀ * Complex.exp x) ^ ((j.val : ℤ) - (m : ℤ)).toNat *
          (b j K).val (z₀ * Complex.exp x)) * Complex.exp ((j.val : ℂ) * y) := by
…

Mentions: OAI.Nagata.Workers.W10.ColumnFiber, OAI.Nagata.W20.localScalar, OAI.Nagata.Workers.W10.polynomialBasisFromSourceBases, OAI.Nagata.Workers.W10.columnFiberEquiv

def OAI.Nagata.Workers.W10.zeroSourceBlockBasis line 252
theorem OAI.Nagata.Workers.W10.zeroSourceBlockBasis_apply line 260
def OAI.Nagata.Workers.W10.firstSourceBlockBasis line 289
def OAI.Nagata.Workers.W10.positiveSourceBlockBasis line 298

theorem OAI.Nagata.Workers.W10.firstSourceBlockBasis_local line 308

Source documentation

The low source basis is exactly the source normalized theta family.

theorem firstSourceBlockBasis_local (hd : 3 * m < d) (hj0 : 0 ≤ j) (hj : j ≤ m)
    (hU : firstLower d m j ρ Δ ∉ Set.range (Int.cast : ℤ → ℝ))
    (K : ColumnFiber d m ρ Δ j) (x : ℂ) :
    (firstSourceBlockBasis hτ hτone hC s ρ Δ x₀ d m j hs hd hj0 hj hU K).val
      (tauPower τ x₀ * Complex.exp x) =
      Nagata.W22.normalizedThetaSeries (commonDegree d m : ℝ)
        ((K.val : ℝ) - firstLower d m j ρ Δ) (K.val : ℝ) ((-1 : ℂ) ^ (m - j)) τ x := by
…

Mentions: OAI.Nagata.Workers.W10.ColumnFiber, OAI.Nagata.Workers.W10.firstSourceBlockBasis, OAI.Nagata.Workers.W10.tauPower, OAI.Nagata.W22.normalizedThetaSeries

theorem OAI.Nagata.Workers.W10.positiveSourceBlockBasis_local line 321

Source documentation

The positive high source basis is its exact untwisted theta family.

theorem positiveSourceBlockBasis_local (hj : m < j) (hjd : j ≤ d / 3) (hn : 0 < d - 3 * j)
    (hU : secondLower d j ρ Δ ∉ Set.range (Int.cast : ℤ → ℝ))
    (K : ColumnFiber d m ρ Δ j) (x : ℂ) :
    (positiveSourceBlockBasis hτ hτone hC s ρ Δ x₀ d m j hs hj hjd hn hU K).val
      (tauPower τ x₀ * Complex.exp x) =
      Nagata.W22.normalizedThetaSeries (sourceDegree d j : ℝ)
        ((K.val : ℝ) - secondLower d j ρ Δ) (K.val : ℝ) 1 τ x := by
…

Mentions: OAI.Nagata.Workers.W10.ColumnFiber, OAI.Nagata.Workers.W10.positiveSourceBlockBasis, OAI.Nagata.Workers.W10.tauPower, OAI.Nagata.W22.normalizedThetaSeries

def OAI.Nagata.Workers.W10.allSourceBlockBases line 356
theorem OAI.Nagata.Workers.W10.allSourceBlockBases_local line 370
def OAI.Nagata.Workers.W10.actualSourceBlockBases line 411
theorem OAI.Nagata.Workers.W10.actualSourceBlockBases_local line 417