ThreePrimeMinorEnergy.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem337.ThreePrimeMinorEnergy.sum_dft_mul line 12
Source documentation
Transposition for the unnormalized discrete Fourier transform.
```
theorem sum_dft_mul (f g : ZMod q → ℂ) :
    (∑ k, ZMod.dft f k * g k) = ∑ x, f x * ZMod.dft g x := by
…
```
theorem OAI.Problem337.ThreePrimeMinorEnergy.dft_conj line 24
Source documentation
Complex conjugation reverses the Fourier frequency.
```
theorem dft_conj (f : ZMod q → ℂ) (k : ZMod q) :
    ZMod.dft (fun x => conj (f x)) k = conj (ZMod.dft f (-k)) := by
…
```
theorem OAI.Problem337.ThreePrimeMinorEnergy.dft_parseval line 34
Source documentation
Exact Parseval identity, retaining the factor q for counting measure.
```
theorem dft_parseval (f : ZMod q → ℂ) :
    (∑ k, ‖ZMod.dft f k‖ ^ 2) = (q : ℝ) * ∑ x, ‖f x‖ ^ 2 := by
…
```

theorem OAI.Problem337.ThreePrimeMinorEnergy.minor_cubic_bound line 62

Source documentation

The cubic contribution of any frequency set is controlled by its supremum Fourier bound and the exact input energy. The phase may be any function of modulus at most one, so either Fourier sign convention is allowed.

theorem minor_cubic_bound (f phase : ZMod q → ℂ) (minor : Finset (ZMod q))
    (B : ℝ) (hB : 0 ≤ B)
    (hminor : ∀ k ∈ minor, ‖ZMod.dft f k‖ ≤ B)
    (hphase : ∀ k ∈ minor, ‖phase k‖ ≤ 1) :
    ‖(q : ℂ)⁻¹ * ∑ k ∈ minor, ZMod.dft f k ^ 3 * phase k‖ ≤
      B * ∑ x, ‖f x‖ ^ 2 := by
…