Fourier.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Finite root-of-unity filters

Averaging the integer powers of a primitive root over one period detects exactly the exponents divisible by that period. This is the finite Fourier filter used for auxiliary separation.

lemma OAI.MatrixMultiplication.AuxiliarySeparation.sum_pow_root_of_unity line 19
Source documentation
The sum over a complete period of a root of unity is zero unless the root is one.
```
lemma sum_pow_root_of_unity (z : ℂ) (L : ℕ) (hz : z ^ L = 1) :
    (∑ r ∈ Finset.range L, z ^ r) = if z = 1 then (L : ℂ) else 0 := by
…
```

theorem OAI.MatrixMultiplication.AuxiliarySeparation.sum_zpow_primitive_root line 28

Source documentation

An unnormalized finite Fourier filter, with an integer exponent.

theorem sum_zpow_primitive_root {ζ : ℂ} {L : ℕ}
    (hζ : IsPrimitiveRoot ζ L) (e : ℤ) :
    (∑ r ∈ Finset.range L, ζ ^ ((r : ℤ) * e)) =
      if (L : ℤ) ∣ e then (L : ℂ) else 0 := by
…

theorem OAI.MatrixMultiplication.AuxiliarySeparation.normalized_sum_zpow_primitive_root line 41

Source documentation

Averaging over a primitive root's period selects exactly its divisible exponents.

theorem normalized_sum_zpow_primitive_root {ζ : ℂ} {L : ℕ}
    (hL : L ≠ 0) (hζ : IsPrimitiveRoot ζ L) (e : ℤ) :
    (L : ℂ)⁻¹ * (∑ r ∈ Finset.range L, ζ ^ ((r : ℤ) * e)) =
      if (L : ℤ) ∣ e then 1 else 0 := by
…

lemma OAI.MatrixMultiplication.AuxiliarySeparation.int_dvd_iff_eq_zero_of_abs_lt line 49
Source documentation
Divisibility by a positive period is exact equality to zero inside one period.
```
lemma int_dvd_iff_eq_zero_of_abs_lt {L : ℕ} {e : ℤ} (he : |e| < (L : ℤ)) :
    (L : ℤ) ∣ e ↔ e = 0 := by
…
```

theorem OAI.MatrixMultiplication.AuxiliarySeparation.normalized_sum_zpow_primitive_root_of_abs_lt line 60

Source documentation

Within one period, the finite Fourier filter selects exactly exponent zero.

theorem normalized_sum_zpow_primitive_root_of_abs_lt {ζ : ℂ} {L : ℕ} {e : ℤ}
    (hL : L ≠ 0) (hζ : IsPrimitiveRoot ζ L) (he : |e| < (L : ℤ)) :
    (L : ℂ)⁻¹ * (∑ r ∈ Finset.range L, ζ ^ ((r : ℤ) * e)) =
      if e = 0 then 1 else 0 := by
…