Interpolation.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

Exact interpolation away from zero

The coefficient-extraction theorem already proved for matrix multiplication is used here with the nonzero nodes 1, ..., D + 1. In particular a polynomial degeneration can be recovered by a finite sum of its ordinary restrictions at nonzero parameters, with the leading power divided out at each parameter.

def OAI.MatrixMultiplication.AuxiliarySeparation.interpolationNode line 23
Source documentation
An explicit set of D + 1 nonzero complex interpolation parameters.
```
def interpolationNode (D : ℕ) (i : Fin (D + 1)) : ℂ := (i.val + 1 : ℕ)
```
theorem OAI.MatrixMultiplication.AuxiliarySeparation.interpolationNode_injective line 25
theorem OAI.MatrixMultiplication.AuxiliarySeparation.interpolationNode_ne_zero line 31
def OAI.MatrixMultiplication.AuxiliarySeparation.constantInterpolationWeight line 37
Source documentation
The constant-coefficient functional expressed in the Lagrange basis.
```
def constantInterpolationWeight {ι : Type*} [Fintype ι] [DecidableEq ι]
    (nodes : ι → ℂ) (i : ι) : ℂ :=
…
```

theorem OAI.MatrixMultiplication.AuxiliarySeparation.constant_eq_sum_eval line 42

Source documentation

Exact constant recovery; this specializes the existing coefficient theorem.

theorem constant_eq_sum_eval {ι : Type*} [Fintype ι] [DecidableEq ι]
    (nodes : ι → ℂ) (hinj : Function.Injective nodes) (p : Polynomial ℂ)
    (hdegree : p.degree < Fintype.card ι) :
    p.coeff 0 = ∑ i, constantInterpolationWeight nodes i * p.eval (nodes i) := by
…

Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.constantInterpolationWeight

theorem OAI.MatrixMultiplication.AuxiliarySeparation.constant_eq_sum_nonzero_eval line 50
Source documentation
A degree-D polynomial is recovered at zero using only nonzero parameters.
```
theorem constant_eq_sum_nonzero_eval (D : ℕ) (p : Polynomial ℂ)
    (hdegree : p.degree ≤ D) :
    p.coeff 0 = ∑ i, constantInterpolationWeight (interpolationNode D) i *
      p.eval (interpolationNode D i) := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.constantInterpolationWeight, OAI.MatrixMultiplication.AuxiliarySeparation.interpolationNode

theorem OAI.MatrixMultiplication.AuxiliarySeparation.leading_eq_sum_normalized_eval line 60

Source documentation

Removing a leading power before interpolation only requires evaluations at nonzero nodes. The degree bound is on the normalized polynomial.

theorem leading_eq_sum_normalized_eval {ι : Type*} [Fintype ι] [DecidableEq ι]
    (nodes : ι → ℂ) (hinj : Function.Injective nodes)
    (hnonzero : ∀ i, nodes i ≠ 0) (p q : Polynomial ℂ) (d : ℕ)
    (hp : p = Polynomial.X ^ d * q) (hdegree : q.degree < Fintype.card ι) :
    p.coeff d = ∑ i, constantInterpolationWeight nodes i *
      (nodes i ^ d)⁻¹ * p.eval (nodes i) := by
…

Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.constantInterpolationWeight

theorem OAI.MatrixMultiplication.AuxiliarySeparation.leading_eq_sum_nonzero_eval line 83
Source documentation
A leading coefficient is a finite linear combination of normalized evaluations, assuming all lower coefficients vanish.
```
theorem leading_eq_sum_nonzero_eval (D d : ℕ) (p : Polynomial ℂ)
    (hvanish : ∀ j < d, p.coeff j = 0) (hdegree : p.degree ≤ D) :
    p.coeff d = ∑ i, constantInterpolationWeight (interpolationNode D) i *
      (interpolationNode D i ^ d)⁻¹ * p.eval (interpolationNode D i) := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.constantInterpolationWeight, OAI.MatrixMultiplication.AuxiliarySeparation.interpolationNode

theorem OAI.MatrixMultiplication.AuxiliarySeparation.restrictionDegeneration_eval line 105

Source documentation

Evaluating the polynomial restriction evaluates its three local maps.

theorem restrictionDegeneration_eval
    (L : Tensor.PolynomialRestrictionDegeneration T U k Lx Ly Lz)
    (t : ℂ) (x' : X') (y' : Y') (z' : Z') :
    (L.basePolynomial x' y' z').eval t =
      Tensor.restrict (fun a x => (L.leftMap a x).eval t)
        (fun b y => (L.middleMap b y).eval t)
        (fun c z => (L.rightMap c z).eval t) T x' y' z' := by
…

theorem OAI.MatrixMultiplication.AuxiliarySeparation.restrictionDegeneration_degree line 117

Source documentation

The degree of a polynomial restriction is bounded by the sum of the degrees of its three local maps.

theorem restrictionDegeneration_degree
    (L : Tensor.PolynomialRestrictionDegeneration T U k Lx Ly Lz)
    (x' : X') (y' : Y') (z' : Z') :
    (L.basePolynomial x' y' z').degree ≤ (Lx + Ly + Lz : ℕ) := by
…

def OAI.MatrixMultiplication.AuxiliarySeparation.restrictionDegeneration_approximation line 139
Source documentation
The existing polynomial-approximation API applies to a polynomial restriction as soon as the source tensor has a rank bound.
```
def restrictionDegeneration_approximation
    (L : Tensor.PolynomialRestrictionDegeneration T U k Lx Ly Lz)
    {r : ℕ} (hT : Tensor.RankAtMost T r) :
    Tensor.PolynomialApproximation U r k (Lx + Ly + Lz) where
…
```
theorem OAI.MatrixMultiplication.AuxiliarySeparation.restrictionDegeneration_power_rankAtMost line 151
Source documentation
Interpolation after tensor powering has a linear degree overhead, rather than raising the single-copy interpolation overhead to the tensor power.
```
theorem restrictionDegeneration_power_rankAtMost
    (L : Tensor.PolynomialRestrictionDegeneration T U k Lx Ly Lz)
    {r : ℕ} (hT : Tensor.RankAtMost T r) (n : ℕ) :
    Tensor.RankAtMost (Tensor.power U n) (((Lx + Ly + Lz) * n + 1) * r ^ n) :=
…
```

theorem OAI.MatrixMultiplication.AuxiliarySeparation.restrictionDegeneration_recovery line 159

Source documentation

A polynomial degeneration yields an exact finite sum of ordinary restrictions at nonzero parameters. There are Lx + Ly + Lz + 1 terms.

theorem restrictionDegeneration_recovery
    (L : Tensor.PolynomialRestrictionDegeneration T U k Lx Ly Lz)
    (x' : X') (y' : Y') (z' : Z') :
    U x' y' z' = ∑ i,
      constantInterpolationWeight (interpolationNode (Lx + Ly + Lz)) i *
      (interpolationNode (Lx + Ly + Lz) i ^ k)⁻¹ *
      Tensor.restrict
        (fun a x => (L.leftMap a x).eval (interpolationNode (Lx + Ly + Lz) i))
        (fun b y => (L.middleMap b y).eval (interpolationNode (Lx + Ly + Lz) i))
        (fun c z => (L.rightMap c z).eval (interpolationNode (Lx + Ly + Lz) i))
        T x' y' z' := by
…

Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.constantInterpolationWeight, OAI.MatrixMultiplication.AuxiliarySeparation.interpolationNode

theorem OAI.MatrixMultiplication.AuxiliarySeparation.restrictionDegeneration_rankAtMost line 179
Source documentation
Finite interpolation converts a polynomial degeneration into an exact rank bound with its explicit number of evaluation parameters.
```
theorem restrictionDegeneration_rankAtMost
    (L : Tensor.PolynomialRestrictionDegeneration T U k Lx Ly Lz)
    {r : ℕ} (hT : Tensor.RankAtMost T r) :
    Tensor.RankAtMost U ((Lx + Ly + Lz + 1) * r) := by
…
```