A fixed smooth dyadic cutoff

The bump is chosen once, independently of every scale and Fourier frequency. Its outer radius is one around 3 / 2, so its support is even smaller than the interval [1 / 2, 3] required for dyadic smoothing.

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.dyadicBump : ContDiffBump (3 / 2)

Fixed inner and outer radii; there is no scale-dependent choice of bump.

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.dyadicBump = { rIn := 1 / 2, rOut := 1, rIn_pos := MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.dyadicBump._proof_3, rIn_lt_rOut := MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.dyadicBump._proof_4 }

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.dyadicCutoff (x : ℝ) : ℝ

The real-valued fixed cutoff.

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.dyadicCutoff x = ↑MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.dyadicBump x

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.dyadicCutoff_contDiff : ContDiff ℝ (↑⊤) dyadicCutoff

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.dyadicCutoff_nonneg (x : ℝ) : 0 ≤ dyadicCutoff x

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.dyadicCutoff_le_one (x : ℝ) : dyadicCutoff x ≤ 1

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.dyadicCutoff_eq_one {x : ℝ} (hx : x ∈ Set.Icc 1 2) : dyadicCutoff x = 1

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.dyadicCutoff_tsupport_subset : tsupport dyadicCutoff ⊆ Set.Icc (1 / 2) 3

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.dyadicCutoff_hasCompactSupport : HasCompactSupport dyadicCutoff

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.scaledDyadicCutoff (M x : ℝ) : ℝ

Dilation of the same fixed cutoff, not a newly chosen bump.

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.scaledDyadicCutoff M x = MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.dyadicCutoff (x / M)

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.scaledDyadicCutoff_contDiff (M : ℝ) : ContDiff ℝ (↑⊤) (scaledDyadicCutoff M)

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.scaledDyadicCutoff_nonneg (M x : ℝ) : 0 ≤ scaledDyadicCutoff M x

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.scaledDyadicCutoff_le_one (M x : ℝ) : scaledDyadicCutoff M x ≤ 1

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.scaledDyadicCutoff_eq_one {M x : ℝ} (hM : 0 < M) (hx : x ∈ Set.Icc M (2 * M)) : scaledDyadicCutoff M x = 1

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.scaledDyadicCutoff_tsupport_subset {M : ℝ} (hM : 0 < M) : tsupport (scaledDyadicCutoff M) ⊆ Set.Icc (M / 2) (3 * M)

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.scaledDyadicCutoff_hasCompactSupport {M : ℝ} (hM : 0 < M) : HasCompactSupport (scaledDyadicCutoff M)

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.dyadicCutoffSchwartz : SchwartzMap ℝ ℂ

The complex-valued Schwartz function used with Mathlib's Fourier transform.

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.dyadicCutoffSchwartz = MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.dyadicCutoffSchwartz._proof_1.toSchwartzMap MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.dyadicCutoffSchwartz._proof_2

@[simp]

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.dyadicCutoffSchwartz_apply (x : ℝ) : dyadicCutoffSchwartz x = ↑(dyadicCutoff x)

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.scaledDyadicCutoffSchwartz (M : ℝ) (hM : 0 < M) : SchwartzMap ℝ ℂ

The dilation is also a genuine Schwartz function at every positive scale.

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.scaledDyadicCutoffSchwartz M hM = ⋯.toSchwartzMap ⋯

@[simp]

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.scaledDyadicCutoffSchwartz_apply (M : ℝ) (hM : 0 < M) (x : ℝ) : (scaledDyadicCutoffSchwartz M hM) x = ↑(scaledDyadicCutoff M x)

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.scaledDyadicCutoff_fourier {M : ℝ} (hM : 0 < M) (w : ℝ) : FourierTransform.fourier (fun (x : ℝ) => ↑(scaledDyadicCutoff M x)) w = M • (FourierTransform.fourier dyadicCutoffSchwartz) (M * w)

Fourier normalization is Mathlib's exp (-2 * π * I * x * w).

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.schwartz_norm_le_rapidDecay (f : SchwartzMap ℝ ℂ) (k : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∀ (x : ℝ), ‖f x‖ ≤ C / (1 + |x|) ^ k

A global rapid-decay bound, including frequency zero.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.scaledDyadicCutoff_fourier_rapidDecay (k : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∀ (M : ℝ), 0 < M → ∀ (w : ℝ), ‖FourierTransform.fourier (fun (x : ℝ) => ↑(scaledDyadicCutoff M x)) w‖ ≤ C * M / (1 + |M * w|) ^ k

The constant is chosen before both the positive scale and the frequency.