GPY criterion: second moment exceeding first moment forces two primes in one translate
Provedgpy_exists_two_primes_of_secondMoment_gtnumber-theory
If the linear second moment over an interval exceeds the first moment over the same interval, some translate in the interval carries primes at two distinct coordinates. The weight, second moment, and prime indicator are written out in Mathlib terms.
Preamble
import Mathlib open Classical
Formal statement
theorem gpy_exists_two_primes_of_secondMoment_gt {k : ℕ} (h : Fin k → ℕ) (R : ℕ) (lam : (Fin k → ℕ) → ℝ) {x y : ℕ} (hgt : (∑ n ∈ Finset.Ioc x y, ((∑ d ∈ ((Fintype.piFinset (fun _ : Fin k => Finset.Icc 1 R)).filter (fun d => ∏ i, d i ≤ R)), if (∀ i, d i ∣ n + h i) then lam d else 0) ^ 2)) < (∑ n ∈ Finset.Ioc x y, (∑ i, (if Nat.Prime (n + h i) then (1 : ℝ) else 0)) * ((∑ d ∈ ((Fintype.piFinset (fun _ : Fin k => Finset.Icc 1 R)).filter (fun d => ∏ i, d i ≤ R)), if (∀ i, d i ∣ n + h i) then lam d else 0) ^ 2))) : ∃ n ∈ Finset.Ioc x y, ∃ i j, i ≠ j ∧ Nat.Prime (n + h i) ∧ Nat.Prime (n + h j) := by sorrySource
GPY ratio analysis: threshold, main-term approximations, and BV level cap