FourierFrequencyGap.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem337.modulus_gt_low_frequency_range line 10

Source documentation

Nontrivial cancellation at all prescribed low frequencies forces the modulus itself to lie beyond that range.

theorem modulus_gt_low_frequency_range {q : ℕ} [NeZero q]
    {ι : Type*} (I : Finset ι) (hI : I.Nonempty) (x : ι → ZMod q)
    (H : ℕ) (ε : ℝ) (hε : ε < 1)
    (hfourier : ∀ ℓ : ℕ, 1 ≤ ℓ → ℓ ≤ H →
      ‖(∑ i ∈ I, ZMod.stdAddChar ((ℓ : ZMod q) * x i)) / (I.card : ℂ)‖ ≤ ε) :
    H < q := by
…

theorem OAI.Problem337.low_frequency_gap_scale line 28
Source documentation
The frequency range needed for localization also guarantees that the cyclic interval contains many integer representatives.
```
theorem low_frequency_gap_scale (δ : ℝ) (q : ℕ)
    (hδ : 0 < δ) (hsmall : δ ≤ 1 / 65536)
    (hgap : ⌊1 / δ ^ 4⌋₊ < q) : 128 ≤ δ * q := by
…
```

theorem OAI.Problem337.negative_character_average_norm line 44

Source documentation

Conjugating all phases does not change the normalized Fourier modulus.

theorem negative_character_average_norm {G ι : Type*} [Finite G] [AddCommGroup G]
    (ψ : AddChar G ℂ) (I : Finset ι) (x : ι → G) :
    ‖(∑ i ∈ I, ψ (-x i)) / (I.card : ℂ)‖ =
      ‖(∑ i ∈ I, ψ (x i)) / (I.card : ℂ)‖ := by
…

theorem OAI.Problem337.difference_frequency_average_bound line 55

Source documentation

Positive-frequency bounds control every off-diagonal difference in a short geometric kernel.

theorem difference_frequency_average_bound {q : ℕ} [NeZero q]
    {ι : Type*} (I : Finset ι) (x : ι → ZMod q) (H : ℕ) (ε : ℝ)
    (hfourier : ∀ ℓ : ℕ, 1 ≤ ℓ → ℓ ≤ H →
      ‖(∑ i ∈ I, ZMod.stdAddChar ((ℓ : ZMod q) * x i)) / (I.card : ℂ)‖ ≤ ε)
    (a b : ℕ) (ha : a ≤ H) (hb : b ≤ H) (hab : a ≠ b) :
    ‖(∑ i ∈ I, ZMod.stdAddChar (((a : ZMod q) - (b : ZMod q)) * x i)) / (I.card : ℂ)‖ ≤ ε := by
…