QuadraticPairCollision.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Coincidences between two monic split quadratics

Distinct unordered pairs give monic quadratics whose equality can hold at at most one point. This is the counting step in the fourth-moment estimate.

theorem OAI.Ostmann.quadraticPair_eq_of_two_points line 21

Source documentation

Equality at two distinct points forces equality of the unordered roots.

theorem quadraticPair_eq_of_two_points {K : Type*} [Field K]
    (b₁ b₂ b₃ b₄ a a' : K) (haa : a ≠ a')
    (ha : (a - b₁) * (a - b₂) = (a - b₃) * (a - b₄))
    (ha' : (a' - b₁) * (a' - b₂) = (a' - b₃) * (a' - b₄)) :
    (b₁ = b₃ ∧ b₂ = b₄) ∨ (b₁ = b₄ ∧ b₂ = b₃) := by
…

theorem OAI.Ostmann.quadraticPair_collision_card_le_one line 46

Source documentation

Off the two diagonals, there is at most one coincidence.

theorem quadraticPair_collision_card_le_one {K : Type*} [Field K] [Fintype K] [DecidableEq K]
    (b₁ b₂ b₃ b₄ : K)
    (hdiag : ¬ ((b₁ = b₃ ∧ b₂ = b₄) ∨ (b₁ = b₄ ∧ b₂ = b₃))) :
    (Finset.univ.filter (fun a : K =>
      (a - b₁) * (a - b₂) = (a - b₃) * (a - b₄))).card ≤ 1 := by
…

theorem OAI.Ostmann.quadraticPair_collision_count_le line 59

Source documentation

The two diagonal pairings account for every exceptional collision fiber.

theorem quadraticPair_collision_count_le {K : Type*} [Field K] [Fintype K] [DecidableEq K]
    (b₁ b₂ b₃ b₄ : K) :
    ((Finset.univ.filter (fun a : K =>
      (a - b₁) * (a - b₂) = (a - b₃) * (a - b₄))).card : ℝ) ≤
      1 + (Fintype.card K : ℝ) *
        ((if b₁ = b₃ ∧ b₂ = b₄ then 1 else 0) +
          (if b₁ = b₄ ∧ b₂ = b₃ then 1 else 0)) := by
…