CompositeSpectral.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem337.CompositeSpectral.sumTuples line 10

Source documentation

Ordered tuples with a prescribed sum in a finite cyclic group.

def sumTuples {q : ℕ} [NeZero q] {X : Type*} [Fintype X]
    (f : X → ZMod q) (k : ℕ) (t : ZMod q) : Finset (Fin k → X) := by
…

theorem OAI.Problem337.CompositeSpectral.sumTuples_fourier line 17
Source documentation
Exact Fourier inversion for an arbitrary tuple length and target. The modulus need not be prime, and the sample type can retain multiplicities.
```
theorem sumTuples_fourier {q : ℕ} [NeZero q] {X : Type*} [Fintype X]
    (f : X → ZMod q) (k : ℕ) (t : ZMod q) :
    (∑ r : ZMod q, ZMod.stdAddChar (-t * r) *
      (∑ x : X, ZMod.stdAddChar (f x * r)) ^ k) =
      (q : ℂ) * (sumTuples f k t).card := by
…
```
Mentions: OAI.Problem337.CompositeSpectral.sumTuples
theorem OAI.Problem337.CompositeSpectral.sumTuples_discrepancy_le line 41
Source documentation
The nontrivial Fourier frequencies control the discrepancy from the uniform tuple count. Keeping the sum, rather than using a worst frequency, allows different proper quotients of a composite modulus to be estimated separately.
```
theorem sumTuples_discrepancy_le {q : ℕ} [NeZero q]
    {X : Type*} [Fintype X] (f : X → ZMod q) (k : ℕ) (t : ZMod q) :
    |(q : ℝ) * (sumTuples f k t).card - (Fintype.card X : ℝ) ^ k| ≤
      ∑ r ∈ (Finset.univ : Finset (ZMod q)).erase 0,
        ‖∑ x : X, ZMod.stdAddChar (f x * r)‖ ^ k := by
…
```
Mentions: OAI.Problem337.CompositeSpectral.sumTuples

theorem OAI.Problem337.CompositeSpectral.sumTuples_lower_bound line 70

Source documentation

A frequency-by-frequency bound gives a quantitative lower bound for the number of tuples having any prescribed sum.

theorem sumTuples_lower_bound {q : ℕ} [NeZero q]
    {X : Type*} [Fintype X] (f : X → ZMod q) (k : ℕ) (t : ZMod q)
    (B : ZMod q → ℝ)
    (hB : ∀ r : ZMod q, r ≠ 0 →
      ‖∑ x : X, ZMod.stdAddChar (f x * r)‖ ≤ B r) :
    (Fintype.card X : ℝ) ^ k -
      (∑ r ∈ (Finset.univ : Finset (ZMod q)).erase 0, B r ^ k) ≤
        (q : ℝ) * (sumTuples f k t).card := by
…

Mentions: OAI.Problem337.CompositeSpectral.sumTuples

theorem OAI.Problem337.CompositeSpectral.exists_sum_of_character_bounds line 91

Source documentation

Summed spectral losses below the zero frequency force a tuple of the specified sum, without any prime-modulus hypothesis.

theorem exists_sum_of_character_bounds {q : ℕ} [NeZero q]
    {X : Type*} [Fintype X] (f : X → ZMod q) (k : ℕ) (t : ZMod q)
    (B : ZMod q → ℝ)
    (hB : ∀ r : ZMod q, r ≠ 0 →
      ‖∑ x : X, ZMod.stdAddChar (f x * r)‖ ≤ B r)
    (hbudget : (∑ r ∈ (Finset.univ : Finset (ZMod q)).erase 0, B r ^ k) <
      (Fintype.card X : ℝ) ^ k) :
    ∃ v : Fin k → X, ∑ i, f (v i) = t := by
…

Mentions: OAI.Problem337.v

theorem OAI.Problem337.CompositeSpectral.products_sum_of_character_bounds line 112

Source documentation

Product sums inherit the frequency-dependent criterion. This is the composite-modulus counterpart of the prime-field five-product extraction; the genuinely arithmetic spectral budget remains an explicit premise.

theorem products_sum_of_character_bounds {q : ℕ} [NeZero q]
    (H : Finset (ZMod q)) (k : ℕ) (t : ZMod q) (B : ZMod q → ℝ)
    (hB : ∀ r : ZMod q, r ≠ 0 →
      ‖∑ a ∈ H, ∑ b ∈ H, ZMod.stdAddChar (a * b * r)‖ ≤ B r)
    (hbudget : (∑ r ∈ (Finset.univ : Finset (ZMod q)).erase 0, B r ^ k) <
      (H.card : ℝ) ^ (2 * k)) :
    ∃ a b : Fin k → H, ∑ i, (a i : ZMod q) * (b i : ZMod q) = t := by
…