SparseMatrixPolynomial.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The bilinear polynomial of a local sparse residue matrix

theorem OAI.Ostmann.sparseResidueMatrix_polynomial line 11

Source documentation

Four evaluations recover the four bilinear coefficients exactly.

theorem sparseResidueMatrix_polynomial {p : ℕ} [NeZero p]
    (S E : Finset (ZMod p)) (u v : ℂ) (x y : Option (ZMod p)) :
    sparseResidueMatrix S E u v x y =
      sparseResidueMatrix S E 0 0 x y +
      u * (sparseResidueMatrix S E 1 0 x y - sparseResidueMatrix S E 0 0 x y) +
      v * (sparseResidueMatrix S E 0 1 x y - sparseResidueMatrix S E 0 0 x y) +
      u * v * (sparseResidueMatrix S E 1 1 x y - sparseResidueMatrix S E 1 0 x y -
        sparseResidueMatrix S E 0 1 x y + sparseResidueMatrix S E 0 0 x y) := by
…

Mentions: OAI.Ostmann.sparseResidueMatrix