ReducedCharacter.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.Problem337.stdAddChar_natCast line 9

Source documentation

The standard additive character evaluated at a natural integer.

lemma stdAddChar_natCast {q : ℕ} [NeZero q] (z : ℕ) :
    ZMod.stdAddChar (z : ZMod q) =
      Complex.exp (2 * Real.pi * Complex.I * (z : ℂ) / (q : ℂ)) := by
…

lemma OAI.Problem337.stdAddChar_cancel_factor line 16

Source documentation

Cancelling an integer common factor in the numerator and modulus does not change the additive phase.

lemma stdAddChar_cancel_factor {g q : ℕ} [NeZero g] [NeZero q]
    [NeZero (g * q)] (c z : ℕ) :
    ZMod.stdAddChar ((g * c * z : ℕ) : ZMod (g * q)) =
      ZMod.stdAddChar ((c * z : ℕ) : ZMod q) := by
…

lemma OAI.Problem337.reduced_modulus_pos line 27
def OAI.Problem337.reducedFrequency line 32
Source documentation
After cancelling the gcd, the numerator is an invertible residue class.
```
def reducedFrequency (a u : ℕ) (hu : 0 < u) : (ZMod (u / a.gcd u))ˣ :=
…
```
lemma OAI.Problem337.reducedFrequency_coe line 36

theorem OAI.Problem337.stdAddChar_reduced line 42

Source documentation

Exact phase reduction to a primitive (unit-frequency) character. This also covers a = 0, where the reduced modulus is 1.

theorem stdAddChar_reduced (a u z : ℕ) (hu : 0 < u)
    [NeZero u] [NeZero (u / a.gcd u)] :
    ZMod.stdAddChar ((a * z : ℕ) : ZMod u) =
      ZMod.stdAddChar ((reducedFrequency a u hu : ZMod (u / a.gcd u)) *
        (z : ZMod (u / a.gcd u))) := by
…

Mentions: OAI.Problem337.reducedFrequency