OAI/NumberTheory/Ostmann/Characters/CRTFourier.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.stdAddChar_mul_factor line 11
2. theorem OAI.Ostmann.crt_fst line 26
3. theorem OAI.Ostmann.crt_snd line 32
4. theorem OAI.Ostmann.crt_stdAddChar line 38
5. theorem OAI.Ostmann.additiveFourier_crt line 86

   Source documentation

   Probability normalization makes the coprime Fourier transform a product.

   theorem additiveFourier_crt {m n : ℕ} [NeZero m] [NeZero n]
       (h : m.Coprime n) (f : ZMod m → ℂ) (g : ZMod n → ℂ) (u : ZMod (m * n)) :
       additiveFourier (fun x => f ((ZMod.chineseRemainder h) x).1 *
         g ((ZMod.chineseRemainder h) x).2) u =
         additiveFourier f ((n : ZMod m)⁻¹ * ((ZMod.chineseRemainder h) u).1) *
         additiveFourier g ((m : ZMod n)⁻¹ * ((ZMod.chineseRemainder h) u).2) := by
   …

   Mentions: OAI.Ostmann.additiveFourier

6. theorem OAI.Ostmann.additiveFourier_translate line 122

   Source documentation

   Translation contributes its additive character with the negative Fourier sign.

   theorem additiveFourier_translate {N : ℕ} [NeZero N]
       (f : ZMod N → ℂ) (t u : ZMod N) :
       additiveFourier (fun x => f (x - t)) u =
         ZMod.stdAddChar (-(t * u)) * additiveFourier f u := by
   …

   Mentions: OAI.Ostmann.additiveFourier