RationalPhaseCharacter.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem337.stdAddChar_of_val_div line 9

Source documentation

The standard character is the circle exponential of a normalized residue.

theorem stdAddChar_of_val_div {q : ℕ} [NeZero q] (y : ZMod q) (x : ℝ)
    (hx : (y.val : ℝ) / q = x) :
    ZMod.stdAddChar y = (Circle.exp (2 * Real.pi * x) : ℂ) := by
…

theorem OAI.Problem337.stdAddChar_frequency_of_val_div line 15

Source documentation

Frequency multiplication becomes the ordinary natural power of the phase.

theorem stdAddChar_frequency_of_val_div {q : ℕ} [NeZero q]
    (y : ZMod q) (x : ℝ) (hx : (y.val : ℝ) / q = x) (l : ℕ) :
    ZMod.stdAddChar ((l : ZMod q) * y) = (Circle.exp (2 * Real.pi * x) : ℂ) ^ l := by
…

theorem OAI.Problem337.stdAddChar_frequency_exp_of_val_div line 21

Source documentation

Equivalent exponential form of the frequency identity.

theorem stdAddChar_frequency_exp_of_val_div {q : ℕ} [NeZero q]
    (y : ZMod q) (x : ℝ) (hx : (y.val : ℝ) / q = x) (l : ℕ) :
    ZMod.stdAddChar ((l : ZMod q) * y) =
      (Circle.exp (2 * Real.pi * (l : ℝ) * x) : ℂ) := by
…

theorem OAI.Problem337.stdAddChar_sum_of_val_div line 32

Source documentation

Fourier sums transfer without any loss, also for repeated indexed samples.

theorem stdAddChar_sum_of_val_div {ι : Type*} {q : ℕ} [NeZero q]
    (s : Finset ι) (y : ι → ZMod q) (x : ι → ℝ)
    (hx : ∀ i ∈ s, ((y i).val : ℝ) / q = x i) (l : ℕ) :
    (∑ i ∈ s, ZMod.stdAddChar ((l : ZMod q) * y i)) =
      ∑ i ∈ s, (Circle.exp (2 * Real.pi * x i) : ℂ) ^ l := by
…

theorem OAI.Problem337.stdAddChar_frequency_of_rational_val_div line 40

Source documentation

Rational common-denominator identities specialize the real-valued phase identity.

theorem stdAddChar_frequency_of_rational_val_div {q : ℕ} [NeZero q]
    (y : ZMod q) (x : ℚ) (hx : (y.val : ℚ) / q = x) (l : ℕ) :
    ZMod.stdAddChar ((l : ZMod q) * y) =
      (Circle.exp (2 * Real.pi * (x : ℝ)) : ℂ) ^ l := by
…