OAI/NumberTheory/Ostmann/Supply/BalancedKernelBlocks.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.balanced_uniform_norms line 11
2. theorem OAI.Ostmann.residue_side_norm_of_energy line 32
3. theorem OAI.Ostmann.residueProjection_side_norms line 43
4. theorem OAI.Ostmann.squareKernel_scalar_norm_le line 59

   Source documentation

   The squared kernel's scalar contribution is O(epsilon/p), rather than O(epsilon). This retains both uniform-support normalization factors.

   theorem squareKernel_scalar_norm_le {p : ℕ} [NeZero p]
       (S E : Finset (ZMod p)) (hS : S.Nonempty) (hSp : S.card < p)
       (hlo : (1 / 3 : ℝ) ≤ residueDensity S) (hhi : residueDensity S ≤ 2 / 3)
       (t ε : ℝ) (hε : 0 ≤ ε) (hE : (E.card : ℝ) ≤ ε * p) :
       ‖residueKernelScalar S (fun x => sparseAdditiveKernel E t x * sparseAdditiveKernel E t x)‖ ≤
         4 * t ^ 2 * ε / p := by
   …

   Mentions: OAI.Ostmann.residueDensity, OAI.Ostmann.residueKernelScalar, OAI.Ostmann.sparseAdditiveKernel