ReducedCollisionFourier.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem337.indexedResidueCollisionCount line 12
Source documentation
The number of ordered pairs in an indexed list with the same residue. The indices, rather than the image set, retain all multiplicities.
```
def indexedResidueCollisionCount {ι : Type*} [Fintype ι]
    {q : ℕ} [NeZero q] (f : ι → ZMod q) : ℕ :=
…
```

theorem OAI.Problem337.sum_sq_residue_fiber_card line 17

Source documentation

Squared fiber sizes exactly count pairs with equal images.

theorem sum_sq_residue_fiber_card {ι : Type*} [Fintype ι]
    {q : ℕ} [NeZero q] (f : ι → ZMod q) :
    (∑ x : ZMod q, ((Finset.univ.filter (fun i : ι => f i = x)).card : ℝ) ^ 2) =
      (indexedResidueCollisionCount f : ℝ) := by
…

Mentions: OAI.Problem337.indexedResidueCollisionCount

theorem OAI.Problem337.residue_fiber_double_sum line 40

Source documentation

Exact regrouping of an indexed bilinear sum, with multiplicities.

theorem residue_fiber_double_sum {ι : Type*} [Fintype ι]
    {q : ℕ} [NeZero q] (f : ι → ZMod q) (g : ZMod q → ZMod q → ℂ) :
    (∑ x : ZMod q, ∑ y : ZMod q,
      ((Finset.univ.filter (fun i : ι => f i = x)).card : ℂ) *
      ((Finset.univ.filter (fun i : ι => f i = y)).card : ℂ) * g x y) =
      ∑ i : ι, ∑ j : ι, g (f i) (f j) := by
…

theorem OAI.Problem337.indexed_residue_bilinear_bound line 60

Source documentation

The two-sided collision estimate at a primitive frequency. It uses the actual squared mass, not a maximum-atom estimate.

theorem indexed_residue_bilinear_bound {ι : Type*} [Fintype ι]
    {q : ℕ} [NeZero q] (f : ι → ZMod q) (c : (ZMod q)ˣ) :
    ‖∑ i : ι, ∑ j : ι,
      ZMod.stdAddChar ((c : ZMod q) * f i * f j)‖ ≤
      Real.sqrt (q : ℝ) * indexedResidueCollisionCount f := by
…

Mentions: OAI.Problem337.indexedResidueCollisionCount

theorem OAI.Problem337.reduced_indexed_bilinear_bound line 82

Source documentation

Nonprimitive frequencies reduce to their true conductor before applying both collision factors. In particular there is no spurious ambient sqrt(q) loss when the conductor is small.

theorem reduced_indexed_bilinear_bound {ι : Type*} [Fintype ι]
    (t : ι → ℕ) (a q : ℕ) (hq : 0 < q)
    [NeZero q] [NeZero (q / a.gcd q)] :
    ‖∑ i : ι, ∑ j : ι,
      ZMod.stdAddChar ((a * t i * t j : ℕ) : ZMod q)‖ ≤
      Real.sqrt ((q / a.gcd q : ℕ) : ℝ) *
        indexedResidueCollisionCount (fun i => (t i : ZMod (q / a.gcd q))) := by
…

Mentions: OAI.Problem337.indexedResidueCollisionCount

theorem OAI.Problem337.reduced_indexed_bilinear_average_bound line 101

Source documentation

Normalized form of the conductor-sensitive collision estimate. It also holds for an empty index type, under the usual zero-division convention.

theorem reduced_indexed_bilinear_average_bound {ι : Type*} [Fintype ι]
    (t : ι → ℕ) (a q : ℕ) (hq : 0 < q)
    [NeZero q] [NeZero (q / a.gcd q)] :
    ‖(∑ i : ι, ∑ j : ι,
      ZMod.stdAddChar ((a * t i * t j : ℕ) : ZMod q)) /
        (Fintype.card ι : ℂ) ^ 2‖ ≤
      Real.sqrt ((q / a.gcd q : ℕ) : ℝ) *
        (indexedResidueCollisionCount (fun i => (t i : ZMod (q / a.gcd q))) : ℝ) /
          (Fintype.card ι : ℝ) ^ 2 := by
…

Mentions: OAI.Problem337.indexedResidueCollisionCount