OAI/NumberTheory/Ostmann/Supply/ResidueProjectionScalar.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.uniformResidueVector line 10
2. theorem OAI.Ostmann.uniformResidueVector_affine line 13
3. theorem OAI.Ostmann.uniformResidueVector_compl_affine line 28
4. theorem OAI.Ostmann.finiteSpectralProjection_affine_pairing line 51
5. theorem OAI.Ostmann.residueProjection_scalar line 73

   Source documentation

   The raw projection's scalar block is negative with the exact coefficient -1/p^2 appearing in the proof of Lemma 5.2.

   theorem residueProjection_scalar {p : ℕ} [NeZero p]
       (S E : Finset (ZMod p)) (hS : S.Nonempty) (hSp : S.card < p) (hE : 0 ∉ E) :
       (∑ x, conj (uniformResidueVector S x) *
         finiteSpectralProjection E (uniformResidueVector (Finset.univ \ S)) x) =
         -((p : ℂ) ^ 2)⁻¹ *
           ((∑ x, ‖finiteSpectralProjection E (normalizedResidueIndicator S) x‖ ^ 2 : ℝ) : ℂ) := by
   …

   Mentions: OAI.Ostmann.uniformResidueVector, OAI.Ostmann.finiteSpectralProjection, OAI.Ostmann.normalizedResidueIndicator