Second-moment approximation against its singular-sum main term

import Mathlib
open Classical

theorem gpy_secondMoment_approx_singSum {k : ℕ} (h : Fin k → ℕ) (R deg : ℕ) (hR : 2 ≤ R) (li : ℝ → ℝ) {x y : ℕ} (hxy : x ≤ y) (wit : (Fin k → ℕ) → (Fin k → ℕ) → Fin k → ℕ) (hwit : ∀ d e i, (∃ w, (∀ j, Nat.lcm (d j) (e j) ∣ w + h j) ∧ Nat.Coprime (w + h i) (Finset.lcm Finset.univ (fun j => Nat.lcm (d j) (e j)))) → (∀ j, Nat.lcm (d j) (e j) ∣ wit d e i + h j) ∧ Nat.Coprime (wit d e i + h i) (Finset.lcm Finset.univ (fun j => Nat.lcm (d j) (e j)))) (mainMono errMono : Fin k → ℕ → ℕ → ℝ) (E : ℕ → ℝ) (hMono : ∀ i, ∀ a ∈ Finset.range (deg + 1), ∀ b ∈ Finset.range (deg + 1), abs ((∑ d ∈ ((Fintype.piFinset (fun _ : Fin k => Finset.Icc 1 R)).filter (fun d => ∏ i, d i ≤ R)), ∑ e ∈ ((Fintype.piFinset (fun _ : Fin k => Finset.Icc 1 R)).filter (fun d => ∏ i, d i ≤ R)), if (∃ w, (∀ j, Nat.lcm (d j) (e j) ∣ w + h j) ∧ Nat.Coprime (w + h i) (Finset.lcm Finset.univ (fun j => Nat.lcm (d j) (e j)))) then (ArithmeticFunction.moebius (∏ j, d j) : ℝ) * (ArithmeticFunction.moebius (∏ j, e j) : ℝ) * (-(Real.log ((∏ j, d j : ℕ) : ℝ) / Real.log R)) ^ a * (-(Real.log ((∏ j, e j : ℕ) : ℝ) / Real.log R)) ^ b / ((Nat.totient (Finset.lcm Finset.univ (fun j => Nat.lcm (d j) (e j))) : ℕ) : ℝ) else 0) - mainMono i a b) ≤ errMono i a b) (hDiv : ∀ i, (∑ L ∈ Finset.range (R ^ 2 + 1), (((Fintype.piFinset (fun _ : Fin (k + 1) => Finset.Icc 1 L)).filter (fun d => ∏ i, d i = L)).card : ℝ) ^ 2 * (if hne : (((Finset.range L).filter (fun r => Nat.Coprime r L)).image (fun r => abs ((((Finset.range ((y + h i) + 1)).filter (fun p => Nat.Prime p ∧ p ≡ r [MOD L])).card : ℝ) - li ((y + h i : ℕ) : ℝ) / ((Nat.totient L : ℕ) : ℝ)))).Nonempty then (((Finset.range L).filter (fun r => Nat.Coprime r L)).image (fun r => abs ((((Finset.range ((y + h i) + 1)).filter (fun p => Nat.Prime p ∧ p ≡ r [MOD L])).card : ℝ) - li ((y + h i : ℕ) : ℝ) / ((Nat.totient L : ℕ) : ℝ)))).max' hne else 0)) ≤ E (y + h i) ∧ (∑ L ∈ Finset.range (R ^ 2 + 1), (((Fintype.piFinset (fun _ : Fin (k + 1) => Finset.Icc 1 L)).filter (fun d => ∏ i, d i = L)).card : ℝ) ^ 2 * (if hne : (((Finset.range L).filter (fun r => Nat.Coprime r L)).image (fun r => abs ((((Finset.range ((x + h i) + 1)).filter (fun p => Nat.Prime p ∧ p ≡ r [MOD L])).card : ℝ) - li ((x + h i : ℕ) : ℝ) / ((Nat.totient L : ℕ) : ℝ)))).Nonempty then (((Finset.range L).filter (fun r => Nat.Coprime r L)).image (fun r => abs ((((Finset.range ((x + h i) + 1)).filter (fun p => Nat.Prime p ∧ p ≡ r [MOD L])).card : ℝ) - li ((x + h i : ℕ) : ℝ) / ((Nat.totient L : ℕ) : ℝ)))).max' hne else 0)) ≤ E (x + h i)) : abs ((∑ 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 (if ∏ i, d i ≤ R then (ArithmeticFunction.moebius (∏ i, d i) : ℝ) * (1 - Real.log ((∏ i, d i : ℕ) : ℝ) / Real.log R) ^ deg else 0) else 0) ^ 2)) - ∑ i, (li ((y + h i : ℕ) : ℝ) - li ((x + h i : ℕ) : ℝ)) * (∑ d ∈ ((Fintype.piFinset (fun _ : Fin k => Finset.Icc 1 R)).filter (fun d => ∏ i, d i ≤ R)), ∑ e ∈ ((Fintype.piFinset (fun _ : Fin k => Finset.Icc 1 R)).filter (fun d => ∏ i, d i ≤ R)), if (∃ w, (∀ j, Nat.lcm (d j) (e j) ∣ w + h j) ∧ Nat.Coprime (w + h i) (Finset.lcm Finset.univ (fun j => Nat.lcm (d j) (e j)))) then (if ∏ i, d i ≤ R then (ArithmeticFunction.moebius (∏ i, d i) : ℝ) * (1 - Real.log ((∏ i, d i : ℕ) : ℝ) / Real.log R) ^ deg else 0) * (if ∏ i, e i ≤ R then (ArithmeticFunction.moebius (∏ i, e i) : ℝ) * (1 - Real.log ((∏ i, e i : ℕ) : ℝ) / Real.log R) ^ deg else 0) / ((Nat.totient (Finset.lcm Finset.univ (fun j => Nat.lcm (d j) (e j))) : ℕ) : ℝ) else 0)) ≤ (∑ i, (E (y + h i) + E (x + h i))) + (∑ d ∈ ((Fintype.piFinset (fun _ : Fin k => Finset.Icc 1 R)).filter (fun d => ∏ i, d i ≤ R)), ∑ e ∈ ((Fintype.piFinset (fun _ : Fin k => Finset.Icc 1 R)).filter (fun d => ∏ i, d i ≤ R)), abs ((if ∏ i, d i ≤ R then (ArithmeticFunction.moebius (∏ i, d i) : ℝ) * (1 - Real.log ((∏ i, d i : ℕ) : ℝ) / Real.log R) ^ deg else 0) * (if ∏ i, e i ≤ R then (ArithmeticFunction.moebius (∏ i, e i) : ℝ) * (1 - Real.log ((∏ i, e i : ℕ) : ℝ) / Real.log R) ^ deg else 0))) * (k : ℝ) + 2 * ∑ i, abs (li ((y + h i : ℕ) : ℝ) - li ((x + h i : ℕ) : ℝ)) * (∑ a ∈ Finset.range (deg + 1), ∑ b ∈ Finset.range (deg + 1), (deg.choose a : ℝ) * (deg.choose b : ℝ) * errMono i a b) := by sorry