theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.directPayMain_n_le {H : ℕ → ℕ → ℕ} {N Q : Finset ℕ} (hN : ∀ n ∈ N, 0 < n) (hQ : ∀ q ∈ Q, 0 < q) {a : ℤ} {P : WOriginalTuple → Prop} {R S ξ T : ℝ} {b : ℕ} {K : WExtractedKey} {j : Fin 5 → ℕ} {positive : Bool} {t : WExtractedTuple × ℤ} (ht : t ∈ wAnalyticDyadicBlock (wExtractedKeyFiber H N Q a P R S ξ b K) j positive) (hNT : ∀ n ∈ N, ↑n ≤ 2 * T) : 2 ^ j 2 ≤ 2 * T

Extract the upper n-scale from the actual block, not from a replacement n=T.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.directPayMain_geometry {x η M T R S : ℝ} (hx : 4 ≤ x) (_hη : 0 ≤ η) (hη1 : η ≤ 1) (hM : 1 ≤ M) (hT : 1 ≤ T) (hxMT : x = 4 * M * T) (hR : 1 ≤ R) (hS : 1 ≤ S) (hRS : R * S ≤ x) {N : Finset ℕ} (hN : ∀ n ∈ N, 0 < n) (hNT : ∀ n ∈ N, ↑n ≤ 2 * T) {a : ℤ} {b : ℕ} {K : WExtractedKey} (hK : K ∈ wExtractedKeyBox (x ^ η)) {j : Fin 5 → ℕ} {positive : Bool} {t : WExtractedTuple × ℤ} (ht : t ∈ wAnalyticDyadicBlock (wExtractedKeyFiber (wFloorCutoff M (x ^ η)) N (Finset.Ioc 0 ⌊R * S⌋₊) a (c2FiveSmallMask x η) R S (highOmegaCutoff x) b K) j positive) : T ≤ x ∧ 2 ^ j 2 ≤ 2 * x ∧ 2 ^ j 3 ≤ x ∧ 2 ^ j 4 ≤ x ∧ ↑K.1.2.1 ≤ x ∧ 2 ^ j 0 ≤ 32 * x ^ 7

Actual floor geometry gives a polynomial cap for every arithmetic loss argument.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.directPayMain_max_le {x : ℝ} (hx : 1 ≤ x) (a : ℤ) (K : WExtractedKey) (F : ℕ) (j : Fin 5 → ℕ) (ha : ↑a.natAbs ≤ x) (hd : ↑K.1.2.1 ≤ x) (hF : ↑F ≤ 2 * x) (hn : 2 ^ j 2 ≤ 2 * x) (hs : 2 ^ j 4 ≤ x) (hH : 2 ^ j 0 ≤ 32 * x ^ 7) : ↑(mainRestrictedMax a K.1.2.1 (2 ^ (j 2 + 1)) (F / K.1.1) (2 ^ (j 0 + 1)) (2 ^ (j 4 + 1))) ≤ 3072 * x ^ 12

A concrete cap for the actual joint-arithmetic maximum.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.directPayMain_log_le {x s δ : ℝ} (hx : 1 ≤ x) (hs : 1 ≤ s) (hsx : s ≤ x) (hδ : 0 < δ) : √(1 + Real.log (2 * s)) ≤ (1 + 2 ^ δ / δ) * x ^ δ

Logarithm is paid with an arbitrary positive divisor exponent.

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.directPayMainLossConstant (κ δ Cnonzero Cτ Cjoint Ca Ccoeff : ℝ) : ℝ

Uniform fixed constant for the complete arithmetic loss.

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.directPayMainLossConstant κ δ Cnonzero Cτ Cjoint Ca Ccoeff = Ccoeff ^ 4 * Cnonzero * Ca * 32 ^ κ * √(Cτ * Cjoint) * 3072 ^ δ * (1 + 2 ^ δ / δ)

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.directPayMain_loss_le (κ δ ρ Cnonzero Cτ Cjoint Ca Ccoeff : ℝ) {x : ℝ} (hx : 1 ≤ x) (hκ : 0 ≤ κ) (hδ : 0 < δ) (hC : 0 ≤ Cnonzero) (hCa : 0 ≤ Ca) (a : ℤ) (K : WExtractedKey) (F : ℕ) (j : Fin 5 → ℕ) (ha : ↑a.natAbs ≤ x) (hd : ↑K.1.2.1 ≤ x) (hF : ↑F ≤ 2 * x) (hn : 2 ^ j 2 ≤ 2 * x) (hr : 2 ^ j 3 ≤ x) (hs : 2 ^ j 4 ≤ x) (hH : 2 ^ j 0 ≤ 32 * x ^ 7) : directPayMainLoss κ δ ρ Cnonzero Cτ Cjoint Ca Ccoeff x a K F j ≤ directPayMainLossConstant κ δ Cnonzero Cτ Cjoint Ca Ccoeff * x ^ (4 * ρ + 14 * δ + 4 * κ)

The true q^κ, joint maximum subpower and logarithmic root are all paid.