Actual local frequency scales

The floor cutoff is the already-paid actual cutoff, not a hypothetical replacement. The ceiling version keeps its extra unit. All dyadic claims below have an actual member; an empty block is handled separately.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.directLocalScale_lcm_eq {H : ℕ → ℕ → ℕ} {N Q : Finset ℕ} (hN : ∀ n ∈ N, 0 < n) (hQ : ∀ q ∈ Q, 0 < q) {a : ℤ} {P : WOriginalTuple → Prop} {R S ξ : ℝ} {b : ℕ} {K : WExtractedKey} {t : WExtractedTuple × ℤ} (ht : t ∈ wExtractedKeyFiber H N Q a P R S ξ b K) : (wExtractedOriginal t.1).1.1.lcm (wExtractedOriginal t.1).1.2 = K.D * (wGCDTuple (wExtractedOriginal t.1)).k₁ * t.1.1.2.1 * t.1.1.2.2

Exact original lcm on a fixed extracted key.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.directLocalScale_lcm_le {H : ℕ → ℕ → ℕ} {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 H N Q a P R S ξ b K) j positive) : ↑((wExtractedOriginal t.1).1.1.lcm (wExtractedOriginal t.1).1.2) ≤ 8 * (↑K.D * 2 ^ j 1 * 2 ^ j 3 * 2 ^ j 4)

The lcm is compared with the local k,r,s scales, never the global level.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.directLocalScale_floor_frequency_le {M Z : ℝ} (hM : 0 < M) (hZ : 0 ≤ Z) {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) : 2 ^ j 0 ≤ 8 * (↑K.D * 2 ^ j 1 * 2 ^ j 3 * 2 ^ j 4) / M * Z

The true floor-retained local H has no rounding loss.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.directLocalScale_ceil_frequency_lt {M Z : ℝ} (hM : 0 < M) (hZ : 0 ≤ Z) {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 (wUniformCutoff M Z) N Q a P R S ξ b K) j positive) : 2 ^ j 0 < 8 * (↑K.D * 2 ^ j 1 * 2 ^ j 3 * 2 ^ j 4) / M * Z + 1

The ceiling-retained local H keeps the mandatory additive one.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.directLocalScale_frequency_change_variables {M T x A Z : ℝ} (hM : M ≠ 0) (hT : T ≠ 0) (hx : x = 4 * M * T) : 8 * A / M * Z = 32 * A * Z * T / x

Recover x=4MT before any enlargement to global parameters.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.directLocalScale_floor_block_empty {M Z : ℝ} (hM : 0 < M) (hZ : 0 ≤ Z) {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) (hsmall : 8 * (↑K.D * 2 ^ j 1 * 2 ^ j 3 * 2 ^ j 4) / M * Z < 1) : wAnalyticDyadicBlock (wExtractedKeyFiber (wFloorCutoff M Z) N Q a P R S ξ b K) j positive = ∅

Below the first retained integer the actual floor block is empty.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.directLocalScale_zero_cutoff_block (N Q : Finset ℕ) (a : ℤ) (P : WOriginalTuple → Prop) (R S ξ : ℝ) (b : ℕ) (K : WExtractedKey) (j : Fin 5 → ℕ) (positive : Bool) : wAnalyticDyadicBlock (wExtractedKeyFiber (fun (x x_1 : ℕ) => 0) N Q a P R S ξ b K) j positive = ∅

Zero cutoff has no nonzero-frequency shell, including b=0.