The explicit terms of the joined retained-prefix estimate

These are exactly the mass and three expressions in direct_retained_prefix_three_terms, exposed for separate scalar payment.

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.directJoinedMass (ρ Couter x T : ℝ) (j : Fin 5 → ℕ) : ℝ

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.directJoinedMass ρ Couter x T j = Couter * x ^ ρ * (8 * 2 ^ j 1 * 2 ^ j 3 * T)

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.directJoinedZero (ε ρ Czero Ccoeff x : ℝ) (K : WExtractedKey) (F : ℕ) (j : Fin 5 → ℕ) : ℝ

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.directJoinedZero ε ρ Czero Ccoeff x K F j = (Ccoeff * x ^ ρ * (Ccoeff * x ^ ρ)) ^ 2 * ↑(2 ^ j 1) * Czero * ↑(MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramResonanceScaleBoxCard K F j) * MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramResonanceScaleEnvelope K F j ε

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.directJoinedSecondary (κ δ ρ Cnonzero Csecondary Ccoeff x : ℝ) (a : ℤ) (R S : ℝ) (K : WExtractedKey) (F : ℕ) (j cap : Fin 5 → ℕ) : ℝ

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.directJoinedSecondary κ δ ρ Cnonzero Csecondary Ccoeff x a R S K F j cap = MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramSecondaryBaseCountBound K F j * ((Ccoeff * x ^ ρ * (Ccoeff * x ^ ρ)) ^ 2 * MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramSecondaryScaleEnvelope κ δ Cnonzero Csecondary a R S K F j cap)

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

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.directJoinedMain κ δ ρ Cnonzero Cτ Cjoint Ca Ccoeff x a R S K F j cap = (Ccoeff * x ^ ρ * (Ccoeff * x ^ ρ)) ^ 2 * MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramDirectMainSubpowerFactor κ δ Cnonzero Ca a R S K j cap * MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramMainJointMean δ Cτ Cjoint a K F j