OAI/NumberTheory/Ostmann/QuadraticCenter/WeightedQuadraticCollisions.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Weighted coincidences of split quadratics

The two diagonal pairings contribute the squared second moment; every other quadruple has at most one collision. This proves the counting inequality underlying the character fourth moment in Section 6.

  1. theorem OAI.Ostmann.sum_four_weights line 18
  2. theorem OAI.Ostmann.sum_paired_weights line 24
  3. theorem OAI.Ostmann.sum_crossed_weights line 43
  4. theorem OAI.Ostmann.weighted_quadratic_collisions_le line 63

    Source documentation

    The weighted collision count is at most 2 |K| r² + J⁴.

    theorem weighted_quadratic_collisions_le {K : Type*} [Field K] [Fintype K] [DecidableEq K]
    (w : K → ℝ) (hw : ∀ b, 0 ≤ w b) :
    (∑ b₁ : K, ∑ b₂ : K, ∑ b₃ : K, ∑ b₄ : K,
      w b₁ * w b₂ * w b₃ * w b₄ *
        ((Finset.univ.filter (fun a : K =>
          (a - b₁) * (a - b₂) = (a - b₃) * (a - b₄))).card : ℝ)) ≤
      2 * (Fintype.card K : ℝ) * (∑ b : K, w b ^ 2) ^ 2 + (∑ b : K, w b) ^ 4 := by
…