Local monomials after reciprocal payment

These are algebraic normalization tools, not asserted producers of main or secondary energy. Exponents are arbitrary and are only enlarged to global scales when their post-payment values are nonnegative.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.directLocalScale_key_bounds {Y : ℝ} (hY : 0 ≤ Y) {K : WExtractedKey} (hK : K ∈ wExtractedKeyBox Y) : ↑K.D ≤ Y ^ 3 ∧ ↑K.D' ≤ Y ^ 5

The small key costs at most Y^3 in D and Y^5 in D'.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.directLocalScale_fullLevel_coordinates {H : ℕ → ℕ → ℕ} {N : Finset ℕ} (hN : ∀ n ∈ N, 0 < n) {L R S : ℝ} (hL : 0 ≤ L) (hR : 0 ≤ R) (hS : 0 ≤ S) {a : ℤ} {P : WOriginalTuple → Prop} {ξ : ℝ} {b : ℕ} {K : WExtractedKey} {j : Fin 5 → ℕ} {positive : Bool} {t : WExtractedTuple × ℤ} (ht : t ∈ wAnalyticDyadicBlock (wExtractedKeyFiber H N (Finset.Ioc 0 ⌊L⌋₊) a P R S ξ b K) j positive) : 2 ^ j 1 ≤ L ∧ 2 ^ j 3 ≤ R ∧ 2 ^ j 4 ≤ S

Global upper coordinates are consequences of an actual full-level member. This theorem does not itself replace any local scale in a denominator.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.directNormalization_monomial {D k r s H B p u v w : ℝ} (hD : 0 < D) (hk : 0 < k) (hr : 0 < r) (hs : 0 < s) (hH : 0 ≤ H) (hB : 0 ≤ B) (hp : 0 ≤ p) (hHB : H ≤ D * k * r * s * B) : (D * k * r * s)⁻¹ * H ^ p * k ^ u * r ^ v * s ^ w ≤ B ^ p * D ^ (p - 1) * k ^ (p + u - 1) * r ^ (p + v - 1) * s ^ (p + w - 1)

Exact exponents after multiplying the local reciprocal and using H≤Dkrs B.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.directNormalization_floor_monomial {M T x Z : ℝ} (hM : 0 < M) (hT : 0 < T) (hZ : 0 ≤ Z) (hx : x = 4 * M * T) {N Q : Finset ℕ} (hN : ∀ n ∈ N, 0 < n) (hQ : ∀ q ∈ Q, 0 < q) {a : ℤ} {P : WOriginalTuple → Prop} {R S ξ : ℝ} {b : ℕ} {K : WExtractedKey} {j : Fin 5 → ℕ} {positive : Bool} {t : WExtractedTuple × ℤ} (ht : t ∈ wAnalyticDyadicBlock (wExtractedKeyFiber (wFloorCutoff M Z) N Q a P R S ξ b K) j positive) (p u v w : ℝ) (hp : 0 ≤ p) : wBlockAmplitude K j * (2 ^ j 0) ^ p * (2 ^ j 1) ^ u * (2 ^ j 3) ^ v * (2 ^ j 4) ^ w ≤ (32 * Z * T / x) ^ p * ↑K.D ^ (p - 1) * (2 ^ j 1) ^ (p + u - 1) * (2 ^ j 3) ^ (p + v - 1) * (2 ^ j 4) ^ (p + w - 1)

The preceding scalar rule instantiated with the proved actual floor cutoff.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.directNormalization_frequency_power {Z T x : ℝ} (hZ : 0 ≤ Z) (hT : 0 ≤ T) (hx : 0 ≤ x) (p : ℝ) : (32 * Z * T / x) ^ p = 32 ^ p * Z ^ p * T ^ p / x ^ p

An explicit expansion of the only frequency loss; no exponent is silently absorbed.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.directNormalization_global_monomial {B D k r s L R S p u v w : ℝ} (hB : 0 ≤ B) (hD : 0 ≤ D) (hk : 0 ≤ k) (hr : 0 ≤ r) (hs : 0 ≤ s) (hkL : k ≤ L) (hrR : r ≤ R) (hsS : s ≤ S) (hu : 0 ≤ p + u - 1) (hv : 0 ≤ p + v - 1) (hw : 0 ≤ p + w - 1) : B ^ p * D ^ (p - 1) * k ^ (p + u - 1) * r ^ (p + v - 1) * s ^ (p + w - 1) ≤ B ^ p * D ^ (p - 1) * L ^ (p + u - 1) * R ^ (p + v - 1) * S ^ (p + w - 1)

Only nonnegative exponents after reciprocal payment may be globally enlarged.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.directNormalization_key_nonpositive_power (K : WExtractedKey) (hD : 0 < K.D) {p : ℝ} (hp : p ≤ 1) : ↑K.D ^ (p - 1) ≤ 1

At p≤1 the positive integer key denominator helps, rather than costing Y.