OAI/NumberTheory/Ostmann/Characters/PolynomialKernelCoordinates.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Exact polynomial kernel entries in centered residue coordinates

  1. def OAI.Ostmann.localPairing line 11
  2. theorem OAI.Ostmann.localPairing_left line 14
  3. theorem OAI.Ostmann.localPairing_right line 25
  4. theorem OAI.Ostmann.polynomial_kernel_coordinate_identity line 37

    Source documentation

    The matrix bounded on the polydisc has precisely the desired entries (1+u*b(a-b))*(1+v*b(a-b)), including its constant mode.

    theorem polynomial_kernel_coordinate_identity {p : ℕ} [NeZero p]
    (S E : Finset (ZMod p)) (a b : ZMod p) (ha : a ∈ S) (hb : b ∈ Finset.univ \ S)
    (u v : ℂ) :
    (1 + u * localSparseKernel E (a - b)) * (1 + v * localSparseKernel E (a - b)) =
      polydiscSparseScalar S E (u + v) (u * v) +
      (∑ x, conj (polydiscSparseSide (Finset.univ \ S) S E (conj (u + v)) (conj (u * v)) x) *
        centeredSupportProjection (Finset.univ \ S) (residuePointVector b) x) +
      (∑ x, conj (centeredSupportProjection S (residuePointVector a) x) *
        polydiscSparseSide S (Finset.univ \ S) E (u + v) (u * v) x) +
      (∑ x, conj (centeredSupportProjection S (residuePointVector a) x) *
        polydiscSparseLower S (Finset.univ \ S) E (u + v) (u * v)
          (centeredSupportProjection (Finset.univ \ S) (residuePointVector b)) x) := by
…

    Mentions: OAI.Ostmann.localSparseKernel, OAI.Ostmann.polydiscSparseScalar, OAI.Ostmann.polydiscSparseSide, OAI.Ostmann.centeredSupportProjection, OAI.Ostmann.residuePointVector, OAI.Ostmann.polydiscSparseLower