Documentation

MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvryExtractedAnalyticReduction

Analytic reduction of the original C.2 error on its full modulus range #

The well-factorable factors are selected before the varying residue. The dyadic block is selected afterwards from the actual retained frequencies. Neither the first signed coefficient nor the real Fourier factor is replaced by a pointwise absolute-value majorant.

source
noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wExtractedBlockExponential (H : ℕ → ℕ → ℕ) (N Q : Finset ℕ) (β c₁ γ ζ : ℕ → ℝ) (a : ℤ) (P : WOriginalTuple → Prop) (R S ξ : ℝ) (b : ℕ) (u : ℝ) :
ℂ

The actual dyadic exponential piece after removing the Fourier transform. Its signed coefficients and every original fiber mask remain inside the sum; the integration variable is the original real variable.

Equations
Instances For
    Inspect dependencies

    MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wExtractedBlockExponential · compiled type and proof/definition references.

    source
    theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wExtractedFrequencyBlock_eq_integral {M : ℝ} (hM : 0 < M) (H : ℕ → ℕ → ℕ) (N Q : Finset ℕ) (β c₁ γ ζ : ℕ → ℝ) (a : ℤ) (P : WOriginalTuple → Prop) (R S ξ : ℝ) (b : ℕ) :
    ∑ t ∈ frequencyBlock (wExtractedFrequencies H N Q a P R S ξ) Prod.snd b, wExtractedFrequencyTerm M β c₁ γ ζ a t = ∫ (u : ℝ), ↑(scaledDyadicCutoff M u) * wExtractedBlockExponential H N Q β c₁ γ ζ a P R S ξ b u
    Inspect dependencies

    MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wExtractedFrequencyBlock_eq_integral · compiled type and proof/definition references.

    source
    theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wExtractedFrequencyBlock_le_max {M : ℝ} (hM : 0 < M) (H : ℕ → ℕ → ℕ) (N Q : Finset ℕ) (β c₁ γ ζ : ℕ → ℝ) (a : ℤ) (P : WOriginalTuple → Prop) (R S ξ : ℝ) (b : ℕ) :
    ∃ y ∈ Set.Icc (1 / 2) 3, (∀ z ∈ Set.Icc (1 / 2) 3, ‖wExtractedBlockExponential H N Q β c₁ γ ζ a P R S ξ b (M * z)‖ ≤ ‖wExtractedBlockExponential H N Q β c₁ γ ζ a P R S ξ b (M * y)‖) ∧ ‖∑ t ∈ frequencyBlock (wExtractedFrequencies H N Q a P R S ξ) Prod.snd b, wExtractedFrequencyTerm M β c₁ γ ζ a t‖ ≤ 3 * M * ‖wExtractedBlockExponential H N Q β c₁ γ ζ a P R S ξ b (M * y)‖
    Inspect dependencies

    MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wExtractedFrequencyBlock_le_max · compiled type and proof/definition references.

    source
    theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wMaskedFactorExtractedTruncated_fullLevel_dyadic_bound {M Z L : ℝ} (hM : 0 < M) (hZ : 0 ≤ Z) (hL : 0 ≤ L) (N : Finset ℕ) (β c₁ γ ζ : ℕ → ℝ) (a : ℤ) (P : WOriginalTuple → Prop) (R S ξ : ℝ) :
    ∃ j ≤ Nat.log 2 ⌈L ^ 2 / M * Z⌉₊, |wMaskedFactorExtractedTruncated M (wUniformCutoff M Z) N (Finset.Ioc 0 ⌊L⌋₊) β c₁ γ ζ a P R S ξ| ≤ ↑(Nat.log 2 ⌈L ^ 2 / M * Z⌉₊ + 1) * ‖∑ t ∈ frequencyBlock (wExtractedFrequencies (wUniformCutoff M Z) N (Finset.Ioc 0 ⌊L⌋₊) a P R S ξ) Prod.snd j, wExtractedFrequencyTerm M β c₁ γ ζ a t‖
    Inspect dependencies

    MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wMaskedFactorExtractedTruncated_fullLevel_dyadic_bound · compiled type and proof/definition references.

    source
    theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wMaskedFactorExtractedTruncated_fullLevel_exponential_bound {M Z L : ℝ} (hM : 0 < M) (hZ : 0 ≤ Z) (hL : 0 ≤ L) (N : Finset ℕ) (β c₁ γ ζ : ℕ → ℝ) (a : ℤ) (P : WOriginalTuple → Prop) (R S ξ : ℝ) :
    ∃ b ≤ Nat.log 2 ⌈L ^ 2 / M * Z⌉₊, ∃ y ∈ Set.Icc (1 / 2) 3, |wMaskedFactorExtractedTruncated M (wUniformCutoff M Z) N (Finset.Ioc 0 ⌊L⌋₊) β c₁ γ ζ a P R S ξ| ≤ 3 * M * ↑(Nat.log 2 ⌈L ^ 2 / M * Z⌉₊ + 1) * ‖wExtractedBlockExponential (wUniformCutoff M Z) N (Finset.Ioc 0 ⌊L⌋₊) β c₁ γ ζ a P R S ξ b (M * y)‖

    A quantitative integral-to-maximum bound for the current extracted W, on the genuine full-level modulus interval. There is no supplied upper bound or cancellation hypothesis for the selected exponential piece.

    Inspect dependencies

    MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wMaskedFactorExtractedTruncated_fullLevel_exponential_bound · compiled type and proof/definition references.

    source
    theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wellFactorable_signedError_sq_le_fullLevel_dyadic_c2 {ι : Type u_1} {κ k i j : ℕ} (A : ℕ) {T : ι → ℝ} {N : ι → Finset ℕ} {β : ι → ℕ → ℝ} (hSW : BetaCoprimeSWFamily κ T N β) (hT : ∀ (z : ι), 1 ≤ T z) (hN : ∀ (z : ι), ∀ n ∈ N z, T z ≤ ↑n ∧ ↑n ≤ 2 * T z) (hβ : ∀ (z : ι), ∀ n ∈ N z, |β z n| ≤ ↑((fouvryTau k) n)) {ε η : ℝ} (hε : 0 < ε) (hη : 0 < η) :
    ∀ᶠ (x : ℝ) in Filter.atTop, ∀ (z : ι) (M ν : ℝ), 1 ≤ M → 4 * M * T z = x → ε ≤ ν → ν ≤ 1 / 10 → T z = x ^ ν → ∀ (U : Finset ℕ), (∀ m ∈ U, M ≤ ↑m ∧ ↑m ≤ 2 * M) → ∀ (α c : ℕ → ℝ), (∀ m ∈ U, |α m| ≤ ↑((fouvryTau i) m)) → SignedWellFactorable j (x ^ ((5 - 5 * ν) / 9 - ε)) c → have L := x ^ ((5 - 5 * ν) / 9 - ε); have R₀ := x ^ c2RExponent ν ε; have S₀ := x ^ c2SExponent ν ε; have J := Nat.log 2 ⌈L ^ 2 / M * x ^ η⌉₊; R₀ * S₀ = L ∧ ∃ (γ : ℕ → ℝ) (ζ : ℕ → ℝ), factorSupported R₀ γ ∧ factorSupported S₀ ζ ∧ (∀ (r : ℕ), |γ r| ≤ ↑((fouvryTau j) r)) ∧ (∀ (s : ℕ), |ζ s| ≤ ↑((fouvryTau j) s)) ∧ c = factorConvolution γ ζ ∧ ∀ (a : ℤ), a ≠ 0 → |↑a| ≤ x → ∃ b ≤ J, signedError U (N z) (Finset.Ioc 0 ⌊L⌋₊) α (β z) c a ^ 2 ≤ (8 * ∑ m ∈ U, α m ^ 2) * ↑(J + 1) * ‖∑ t ∈ frequencyBlock (wExtractedFrequencies (wUniformCutoff M (x ^ η)) (N z) (Finset.Ioc 0 ⌊L⌋₊) a (c2FiveSmallMask x η) R₀ S₀ (highOmegaCutoff x)) Prod.snd b, wExtractedFrequencyTerm M (betaClean (β z) a) (factorConvolution γ (betaLowOmega ζ (highOmegaCutoff x))) γ ζ a t‖ + x ^ 2 / Real.log x ^ A

    No modulus-subset parameter occurs at this analytic endpoint. The scale-only number of shells is explicit and the original signed error, full WF weight, and original SW family remain on the left.

    Inspect dependencies

    MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wellFactorable_signedError_sq_le_fullLevel_dyadic_c2 · compiled type and proof/definition references.

    source
    theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wellFactorable_signedError_sq_le_fullLevel_exponential_c2 {ι : Type u_1} {κ k i j : ℕ} (A : ℕ) {T : ι → ℝ} {N : ι → Finset ℕ} {β : ι → ℕ → ℝ} (hSW : BetaCoprimeSWFamily κ T N β) (hT : ∀ (z : ι), 1 ≤ T z) (hN : ∀ (z : ι), ∀ n ∈ N z, T z ≤ ↑n ∧ ↑n ≤ 2 * T z) (hβ : ∀ (z : ι), ∀ n ∈ N z, |β z n| ≤ ↑((fouvryTau k) n)) {ε η : ℝ} (hε : 0 < ε) (hη : 0 < η) :
    ∀ᶠ (x : ℝ) in Filter.atTop, ∀ (z : ι) (M ν : ℝ), 1 ≤ M → 4 * M * T z = x → ε ≤ ν → ν ≤ 1 / 10 → T z = x ^ ν → ∀ (U : Finset ℕ), (∀ m ∈ U, M ≤ ↑m ∧ ↑m ≤ 2 * M) → ∀ (α c : ℕ → ℝ), (∀ m ∈ U, |α m| ≤ ↑((fouvryTau i) m)) → SignedWellFactorable j (x ^ ((5 - 5 * ν) / 9 - ε)) c → have L := x ^ ((5 - 5 * ν) / 9 - ε); have R₀ := x ^ c2RExponent ν ε; have S₀ := x ^ c2SExponent ν ε; have J := Nat.log 2 ⌈L ^ 2 / M * x ^ η⌉₊; R₀ * S₀ = L ∧ ∃ (γ : ℕ → ℝ) (ζ : ℕ → ℝ), factorSupported R₀ γ ∧ factorSupported S₀ ζ ∧ (∀ (r : ℕ), |γ r| ≤ ↑((fouvryTau j) r)) ∧ (∀ (s : ℕ), |ζ s| ≤ ↑((fouvryTau j) s)) ∧ c = factorConvolution γ ζ ∧ ∀ (a : ℤ), a ≠ 0 → |↑a| ≤ x → ∃ b ≤ J, ∃ y ∈ Set.Icc (1 / 2) 3, signedError U (N z) (Finset.Ioc 0 ⌊L⌋₊) α (β z) c a ^ 2 ≤ (24 * M * ∑ m ∈ U, α m ^ 2) * ↑(J + 1) * ‖wExtractedBlockExponential (wUniformCutoff M (x ^ η)) (N z) (Finset.Ioc 0 ⌊L⌋₊) (betaClean (β z) a) (factorConvolution γ (betaLowOmega ζ (highOmegaCutoff x))) γ ζ a (c2FiveSmallMask x η) R₀ S₀ (highOmegaCutoff x) b (M * y)‖ + x ^ 2 / Real.log x ^ A

    Original C.2 error reduced to an attained, explicitly constructed exponential piece. The threshold still precedes the family index, nu, scales and residue; the legitimate WF factors still precede a. This is not an IV.3 cancellation estimate for that piece.

    Inspect dependencies

    MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wellFactorable_signedError_sq_le_fullLevel_exponential_c2 · compiled type and proof/definition references.