CompositeConductorBudget.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem337.CompositeSpectral.reciprocal_square_Icc_bound line 10
Source documentation
A finite reciprocal-square tail with a uniform strict margin below one.
```
theorem reciprocal_square_Icc_bound (N : ℕ) (hN : 2 ≤ N) :
    (∑ d ∈ Finset.Icc 2 N, (1 : ℝ) / (d : ℝ) ^ 2) ≤
      3 / 4 - 1 / (N : ℝ) := by
…
```
theorem OAI.Problem337.CompositeSpectral.order_fiber_card_le line 30
Source documentation
At most d residues have additive order d, including orders which do not divide the modulus. For divisors, the exact count is Euler's totient.
```
theorem order_fiber_card_le (q d : ℕ) [NeZero q] :
    ((Finset.univ : Finset (ZMod q)).filter (fun r => addOrderOf r = d)).card ≤ d := by
…
```
theorem OAI.Problem337.CompositeSpectral.conductor_cube_sum_le line 51
Source documentation
The total cubic reciprocal-conductor mass is uniformly at most 3/4. This controls the sixth moment when the normalized character bound at conductor d is 1 / sqrt d.
```
theorem conductor_cube_sum_le (q : ℕ) [NeZero q] :
    (∑ r ∈ (Finset.univ : Finset (ZMod q)).erase 0,
      (1 : ℝ) / (addOrderOf r : ℝ) ^ 3) ≤ 3 / 4 := by
…
```
theorem OAI.Problem337.CompositeSpectral.order_eq_reduced_modulus line 101
Source documentation
Additive order is exactly the conductor obtained by cancelling the frequency against the modulus.
```
theorem order_eq_reduced_modulus {q : ℕ} [NeZero q] (r : ZMod q) :
    addOrderOf r = q / r.val.gcd q := by
…
```

theorem OAI.Problem337.CompositeSpectral.six_products_of_conductor_bound line 109

Source documentation

A pointwise inverse-square-root conductor estimate supplies six products with every target sum. No residue-distribution hypothesis is silently assumed: the actual character estimate is a premise of this theorem.

theorem six_products_of_conductor_bound {q : ℕ} [NeZero q]
    (H : Finset (ZMod q)) (hH : H.Nonempty)
    (hchar : ∀ r : ZMod q, r ≠ 0 →
      ‖∑ a ∈ H, ∑ b ∈ H, ZMod.stdAddChar (a * b * r)‖ ≤
        (H.card : ℝ) ^ 2 / Real.sqrt (addOrderOf r : ℝ))
    (t : ZMod q) :
    ∃ a b : Fin 6 → H, ∑ i, (a i : ZMod q) * (b i : ZMod q) = t := by
…