EightProductConductor.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Eight products from a subuniform conductor collision bound

A collision exponent of 7/8, unlike exact equidistribution, is compatible with the rough-modulus exceptional-set construction. Eight products then produce a cubic conductor loss, controlled by the existing uniform 3/4 conductor budget. The index type retains all sample multiplicities.

theorem OAI.Problem337.CompositeSpectral.eight_products_of_conductor_power_bound line 21

Source documentation

A pointwise eighth-moment bound suffices for eight indexed products with any prescribed sum. This formulation avoids fractional powers in consumers.

theorem eight_products_of_conductor_power_bound
    {q : ℕ} [NeZero q] {ι : Type*} [Fintype ι] [Nonempty ι]
    (v : ι → ZMod q)
    (hchar : ∀ r : ZMod q, r ≠ 0 →
      ‖∑ i : ι, ∑ j : ι, ZMod.stdAddChar (v i * v j * r)‖ ^ 8 ≤
        (Fintype.card ι : ℝ) ^ 16 / (addOrderOf r : ℝ) ^ 3)
    (target : ZMod q) :
    ∃ a b : Fin 8 → ι, ∑ i, v (a i) * v (b i) = target := by
…

Mentions: OAI.Problem337.v

def OAI.Problem337.CompositeSpectral.remainderCollisionCount line 55
Source documentation
Ordered residue-collision pairs, expressed with natural remainders so no typeclass proof is part of the collision function's data.
```
def remainderCollisionCount {ι : Type*} [Fintype ι] (t : ι → ℕ) (d : ℕ) : ℕ :=
…
```
lemma OAI.Problem337.CompositeSpectral.remainderCollisionCount_eq_cast line 58

lemma OAI.Problem337.CompositeSpectral.bilinear_le_sqrt_order_mul_collisions line 67

Source documentation

Conductor-sensitive bilinear estimate in the natural-remainder convention.

lemma bilinear_le_sqrt_order_mul_collisions
    {q : ℕ} [NeZero q] {ι : Type*} [Fintype ι]
    (t : ι → ℕ) (r : ZMod q) :
    ‖∑ i : ι, ∑ j : ι,
      ZMod.stdAddChar ((t i : ZMod q) * (t j : ZMod q) * r)‖ ≤
        Real.sqrt (addOrderOf r : ℝ) * remainderCollisionCount t (addOrderOf r) := by
…

Mentions: OAI.Problem337.CompositeSpectral.remainderCollisionCount

theorem OAI.Problem337.CompositeSpectral.eight_products_of_collision_power_bound line 91

Source documentation

A purely polynomial collision hypothesis at every nontrivial divisor of q gives eight products with every prescribed residue. The hypothesis is the power-eight form of collision density at most d^(-7/8).

theorem eight_products_of_collision_power_bound
    {q : ℕ} [NeZero q] {ι : Type*} [Fintype ι] [Nonempty ι]
    (t : ι → ℕ)
    (hcollision : ∀ d : ℕ, 2 ≤ d → d ∣ q →
      (remainderCollisionCount t d : ℝ) ^ 8 * (d : ℝ) ^ 7 ≤
        (Fintype.card ι : ℝ) ^ 16)
    (target : ZMod q) :
    ∃ a b : Fin 8 → ι,
      ∑ i, (t (a i) : ZMod q) * (t (b i) : ZMod q) = target := by
…

Mentions: OAI.Problem337.CompositeSpectral.remainderCollisionCount

theorem OAI.Problem337.CompositeSpectral.eight_products_of_collision_rpow_bound line 127

Source documentation

The fractional-power form directly matches a collision exceptional-set threshold. The estimate is required only at divisors of the final modulus.

theorem eight_products_of_collision_rpow_bound
    {q : ℕ} [NeZero q] {ι : Type*} [Fintype ι] [Nonempty ι]
    (t : ι → ℕ)
    (hcollision : ∀ d : ℕ, 2 ≤ d → d ∣ q →
      (remainderCollisionCount t d : ℝ) ≤
        (Fintype.card ι : ℝ) ^ 2 / (d : ℝ) ^ ((7 : ℝ) / 8))
    (target : ZMod q) :
    ∃ a b : Fin 8 → ι,
      ∑ i, (t (a i) : ZMod q) * (t (b i) : ZMod q) = target := by
…

Mentions: OAI.Problem337.CompositeSpectral.remainderCollisionCount