KernelCoordinateIdentity.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Exact identification of the centered-coordinate kernel matrix

theorem OAI.Ostmann.rawKernel_pairing_add line 10
theorem OAI.Ostmann.centeredSupportProjection_pairing_range line 21

theorem OAI.Ostmann.kernel_centered_coordinate_identity line 29

Source documentation

The four blocks really represent k(a-b) on the centered coordinates of the two residue points. This is the identity used before tensoring.

theorem kernel_centered_coordinate_identity {p : ℕ} [NeZero p]
    (S : Finset (ZMod p)) (k : ZMod p → ℂ)
    (hk : ∀ c, conj ((p : ℂ) * additiveFourier k c) = (p : ℂ) * additiveFourier k c)
    (a b : ZMod p) (ha : a ∈ S) (hb : b ∈ Finset.univ \ S) :
    k (a - b) = residueKernelScalar S k +
      (∑ x, conj (residueKernelSide (Finset.univ \ S) S k x) *
        centeredSupportProjection (Finset.univ \ S) (residuePointVector b) x) +
      (∑ x, conj (centeredSupportProjection S (residuePointVector a) x) *
        residueKernelSide S (Finset.univ \ S) k x) +
      (∑ x, conj (centeredSupportProjection S (residuePointVector a) x) *
        residueKernelLower S (Finset.univ \ S) k
          (centeredSupportProjection (Finset.univ \ S) (residuePointVector b)) x) := by
…

Mentions: OAI.Ostmann.additiveFourier, OAI.Ostmann.residueKernelScalar, OAI.Ostmann.residueKernelSide, OAI.Ostmann.centeredSupportProjection, OAI.Ostmann.residuePointVector, OAI.Ostmann.residueKernelLower