OAI/NumberTheory/EgyptianFractions/CyclicKernel.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Problem337.CyclicSmoothing.conj_stdAddChar line 12
2. lemma OAI.Problem337.CyclicSmoothing.stdAddChar_pow line 18
3. lemma OAI.Problem337.CyclicSmoothing.cyclic_power_correlation line 22
4. theorem OAI.Problem337.CyclicSmoothing.sum_cyclic_kernel line 40

   Source documentation

   Exact mass of the cyclic Fejer kernel below the modulus.

   theorem sum_cyclic_kernel {q h : ℕ} [NeZero q] (hh : 0 < h) (hhq : h ≤ q) :
       (∑ x : ZMod q, GeometricKernel.kernel h (ZMod.stdAddChar x)) = (q : ℝ) := by
   …

   Mentions: OAI.Problem337.GeometricKernel.kernel

5. def OAI.Problem337.CyclicSmoothing.normalizedKernel line 68

   Source documentation

   The kernel normalized for counting measure on ZMod q.

   def normalizedKernel {q : ℕ} [NeZero q] (h : ℕ) (x : ZMod q) : ℝ :=
   …

6. lemma OAI.Problem337.CyclicSmoothing.normalizedKernel_nonneg line 71
7. lemma OAI.Problem337.CyclicSmoothing.sum_normalizedKernel line 75