Disjoint dyadic pieces of the retained frequencies

The half-open shells avoid duplicating powers of two. Both signs stay in the same shell, and zero is removed using its actual zero summand. The original tuple-dependent cutoff is retained, not enlarged.

def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.frequencyBlock {ι : Type u_1} (T : Finset ι) (h : ι → ℤ) (j : ℕ) : Finset ι

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.frequencyBlock T h j = {t ∈ T | h t ≠ 0 ∧ Nat.log 2 (h t).natAbs = j}

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.mem_frequencyBlock_iff {ι : Type u_1} {T : Finset ι} {h : ι → ℤ} {j : ℕ} {t : ι} : t ∈ frequencyBlock T h j ↔ t ∈ T ∧ 2 ^ j ≤ (h t).natAbs ∧ (h t).natAbs < 2 ^ (j + 1)

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.sum_eq_frequencyBlocks {ι : Type u_1} {A : Type u_2} [AddCommMonoid A] (T : Finset ι) (h : ι → ℤ) (F : ι → A) (B : ℕ) (hB : ∀ t ∈ T, (h t).natAbs ≤ B) (hzero : ∀ t ∈ T, h t = 0 → F t = 0) : ∑ t ∈ T, F t = ∑ j ∈ Finset.range (Nat.log 2 B + 1), ∑ t ∈ frequencyBlock T h j, F t

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.exists_frequencyBlock_norm_bound {ι : Type u_1} (T : Finset ι) (h : ι → ℤ) (F : ι → ℂ) (B : ℕ) (hB : ∀ t ∈ T, (h t).natAbs ≤ B) (hzero : ∀ t ∈ T, h t = 0 → F t = 0) : ∃ j ≤ Nat.log 2 B, ‖∑ t ∈ T, F t‖ ≤ ↑(Nat.log 2 B + 1) * ‖∑ t ∈ frequencyBlock T h j, F t‖

A genuine logarithmic-loss reduction: the chosen shell is a maximum of the actual complex shell sums, not a bound supplied by the caller.

@[reducible, inline]

abbrev MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.WExtractedTuple : Type

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.WExtractedTuple = (MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.FactorExtractionTuple × ℕ × ℕ × ℕ)

def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wExtractedOriginal (z : WExtractedTuple) : WOriginalTuple

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wExtractedOriginal z = ((z.2.1, z.1.1.1 * z.1.2.1 * (z.1.1.2 * z.1.2.2)), z.2.2)

def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wExtractedCoefficient (β c₁ γ ζ : ℕ → ℝ) (z : WExtractedTuple) : ℝ

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wExtractedCoefficient β c₁ γ ζ z = γ (z.1.1.1 * z.1.2.1) * ζ (z.1.1.2 * z.1.2.2) * (c₁ z.2.1 * β z.2.2.1 * β z.2.2.2)

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wExtractedFrequencies (H : ℕ → ℕ → ℕ) (N Q : Finset ℕ) (a : ℤ) (P : WOriginalTuple → Prop) (R S ξ : ℝ) : Finset (WExtractedTuple × ℤ)

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wExtractedFrequencies H N Q a P R S ξ = (MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wFactorExtractionTuples N Q a P R S ξ).biUnion fun (z : MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.FactorExtractionTuple × ℕ × ℕ × ℕ) => {z} ×ˢ Finset.Icc (-↑(H (MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wExtractedOriginal z).1.1 (MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wExtractedOriginal z).1.2)) ↑(H (MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wExtractedOriginal z).1.1 (MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wExtractedOriginal z).1.2)

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.mem_wExtractedFrequencies_iff {H : ℕ → ℕ → ℕ} {N Q : Finset ℕ} {a : ℤ} {P : WOriginalTuple → Prop} {R S ξ : ℝ} {t : WExtractedTuple × ℤ} : t ∈ wExtractedFrequencies H N Q a P R S ξ ↔ t.1 ∈ wFactorExtractionTuples N Q a P R S ξ ∧ -↑(H (wExtractedOriginal t.1).1.1 (wExtractedOriginal t.1).1.2) ≤ t.2 ∧ t.2 ≤ ↑(H (wExtractedOriginal t.1).1.1 (wExtractedOriginal t.1).1.2)

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wExtractedFrequencyTerm (M : ℝ) (β c₁ γ ζ : ℕ → ℝ) (a : ℤ) (t : WExtractedTuple × ℤ) : ℂ

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wExtractedFrequencyTerm M β c₁ γ ζ a t = ↑(MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wExtractedCoefficient β c₁ γ ζ t.1) * MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wPoissonFrequency M a (MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wExtractedOriginal t.1).1.1 (MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wExtractedOriginal t.1).1.2 (MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wExtractedOriginal t.1).2.1 (MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wExtractedOriginal t.1).2.2 t.2

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wExtractedFrequencyTerm_zero (M : ℝ) (β c₁ γ ζ : ℕ → ℝ) (a : ℤ) (z : WExtractedTuple) : wExtractedFrequencyTerm M β c₁ γ ζ a (z, 0) = 0

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wMaskedFactorExtractedTruncated_eq_frequencies (M : ℝ) (H : ℕ → ℕ → ℕ) (N Q : Finset ℕ) (β c₁ γ ζ : ℕ → ℝ) (a : ℤ) (P : WOriginalTuple → Prop) (R S ξ : ℝ) : wMaskedFactorExtractedTruncated M H N Q β c₁ γ ζ a P R S ξ = (∑ t ∈ wExtractedFrequencies H N Q a P R S ξ, wExtractedFrequencyTerm M β c₁ γ ζ a t).re

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wExtractedMaxFrequency (H : ℕ → ℕ → ℕ) (N Q : Finset ℕ) (a : ℤ) (P : WOriginalTuple → Prop) (R S ξ : ℝ) : ℕ

This maximum only bounds the already retained frequency sets. The individual cutoffs remain tests in wExtractedFrequencies.

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wExtractedMaxFrequency H N Q a P R S ξ = (MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wFactorExtractionTuples N Q a P R S ξ).sup fun (z : MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.FactorExtractionTuple × ℕ × ℕ × ℕ) => H (MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wExtractedOriginal z).1.1 (MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wExtractedOriginal z).1.2

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wExtractedFrequencies_natAbs_le {H : ℕ → ℕ → ℕ} {N Q : Finset ℕ} {a : ℤ} {P : WOriginalTuple → Prop} {R S ξ : ℝ} {t : WExtractedTuple × ℤ} (ht : t ∈ wExtractedFrequencies H N Q a P R S ξ) : t.2.natAbs ≤ wExtractedMaxFrequency H N Q a P R S ξ

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wMaskedFactorExtractedTruncated_dyadic_bound (M : ℝ) (H : ℕ → ℕ → ℕ) (N Q : Finset ℕ) (β c₁ γ ζ : ℕ → ℝ) (a : ℤ) (P : WOriginalTuple → Prop) (R S ξ : ℝ) : ∃ j ≤ Nat.log 2 (wExtractedMaxFrequency H N Q a P R S ξ), |wMaskedFactorExtractedTruncated M H N Q β c₁ γ ζ a P R S ξ| ≤ ↑(Nat.log 2 (wExtractedMaxFrequency H N Q a P R S ξ) + 1) * ‖∑ t ∈ frequencyBlock (wExtractedFrequencies H N Q a P R S ξ) Prod.snd j, wExtractedFrequencyTerm M β c₁ γ ζ a t‖

The actual signed extracted W is controlled by one actual dyadic Fourier piece, with an explicit logarithmic number of pieces.