noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.directPayMainLoss (κ δ ρ Cnonzero Cτ Cjoint Ca Ccoeff x : ℝ) (a : ℤ) (K : WExtractedKey) (F : ℕ) (j : Fin 5 → ℕ) : ℝ

The explicit arithmetic loss; this is not an input bound on the energy.

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.directPayMainLoss κ δ ρ Cnonzero Cτ Cjoint Ca Ccoeff x a K F j = (Ccoeff * x ^ ρ * (Ccoeff * x ^ ρ)) ^ 2 * (Cnonzero * (Ca * ↑a.natAbs ^ δ)) * (16 * 2 ^ j 2 * 2 ^ j 3 * (2 ^ j 4) ^ 2) ^ κ * √(Cτ * Cjoint) * ↑(MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.mainRestrictedMax a K.1.2.1 (2 ^ (j 2 + 1)) (F / K.1.1) (2 ^ (j 0 + 1)) (2 ^ (j 4 + 1))) ^ δ * √(1 + Real.log (2 ^ (j 4 + 1)))

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.directPayMainLoss_nonneg (κ δ ρ Cnonzero Cτ Cjoint Ca Ccoeff x : ℝ) (a : ℤ) (K : WExtractedKey) (F : ℕ) (j : Fin 5 → ℕ) (hC : 0 ≤ Cnonzero) (hCa : 0 ≤ Ca) : 0 ≤ directPayMainLoss κ δ ρ Cnonzero Cτ Cjoint Ca Ccoeff x a K F j

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.directPayMain_mean_le (δ Cτ Cjoint : ℝ) (a : ℤ) (K : WExtractedKey) (F : ℕ) (j : Fin 5 → ℕ) {T : ℝ} (hCτ : 0 ≤ Cτ) (hCjoint : 0 ≤ Cjoint) (_hT : 0 ≤ T) (hF : ↑F ≤ 2 * T) : wGramMainJointMean δ Cτ Cjoint a K F j ≤ 64 * 2 ^ j 3 * 2 ^ j 2 * T ^ 2 * (2 ^ j 4) ^ 2 * (2 ^ j 0) ^ 2 * √(Cτ * Cjoint) * ↑(mainRestrictedMax a K.1.2.1 (2 ^ (j 2 + 1)) (F / K.1.1) (2 ^ (j 0 + 1)) (2 ^ (j 4 + 1))) ^ δ * √(1 + Real.log (2 ^ (j 4 + 1)))

The literal joint mean pays the entire coefficient-pair length using F≤2T.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.directPayMain_qpow (κ : ℝ) (hκ : 0 ≤ κ) (j : Fin 5 → ℕ) : ↑(2 ^ (j 2 + 1) * (2 ^ (j 3 + 1) - 1) * 2 ^ (j 4 + 1) * 2 ^ (j 4 + 1)) ^ (1 / 2 + κ) ≤ 4 * (2 ^ j 2) ^ (1 / 2) * (2 ^ j 3) ^ (1 / 2) * 2 ^ j 4 * (16 * 2 ^ j 2 * 2 ^ j 3 * (2 ^ j 4) ^ 2) ^ κ

The q^(1/2+κ) factor is genuinely split, retaining q^κ in the explicit loss.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.directPayMain_energy_le (κ δ ρ Cnonzero Cτ Cjoint Ca Ccoeff x : ℝ) (a : ℤ) (R S : ℝ) (K : WExtractedKey) (F : ℕ) (j cap : Fin 5 → ℕ) {T : ℝ} (hκ : 0 ≤ κ) (hC : 0 ≤ Cnonzero) (hCa : 0 ≤ Ca) (hCτ : 0 ≤ Cτ) (hCjoint : 0 ≤ Cjoint) (hT : 0 ≤ T) (hF : ↑F ≤ 2 * T) : directJoinedMain κ δ ρ Cnonzero Cτ Cjoint Ca Ccoeff x a R S K F j cap ≤ 256 * directPayMainLoss κ δ ρ Cnonzero Cτ Cjoint Ca Ccoeff x a K F j * (2 ^ j 0) ^ 2 * (2 ^ j 2) ^ (3 / 2) * T ^ 2 * (2 ^ j 3) ^ (3 / 2) * (2 ^ j 4) ^ 3 * (↑K.D' + 2 * 2 ^ j 1 / (2 ^ j 2 * 2 ^ j 3 * (2 ^ j 4) ^ 2))

Fully expanded actual energy. Both completion terms remain visible.