OAI/NumberTheory/Ostmann/Characters/SparseResidueMatrix.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.sparseResidueMatrix line 10
2. def OAI.Ostmann.residuePointCoordinates line 17
3. theorem OAI.Ostmann.sparseResidueMatrix_energy_le line 22
4. theorem OAI.Ostmann.sparseResidueMatrix_point_identity line 39
5. theorem OAI.Ostmann.sparseResidueMatrix_contraction line 52

   Source documentation

   The sharper local estimate at (1,1) in the same finite matrix coordinates.

   theorem sparseResidueMatrix_contraction {p : ℕ} [Fact p.Prime]
       (S : Finset (ZMod p)) (hS : S.Nonempty) (hSp : S.card < p) (hp : (100 : ℝ) ≤ p)
       (hlo : (1 / 3 : ℝ) ≤ residueDensity S) (hhi : residueDensity S ≤ 2 / 3)
       (ε : ℝ) (hε : 0 ≤ ε) (hεsmall : ε ≤ 1 / 1000000)
       (hL1 : (p : ℝ)⁻¹ * ∑ b, ‖normalizedResidueTransform S b‖ ≤ ε ^ 2)
       (f : Option (ZMod p) → ℂ) :
       let E := largeTransformSpectrum (normalizedResidueTransform S)
   …

   Mentions: OAI.Ostmann.residueDensity, OAI.Ostmann.normalizedResidueTransform, OAI.Ostmann.largeTransformSpectrum