Ported for Lean Pool from PrimeNumberTheoremAnd commit 0c7abf7be7765dc5ffd21afc1c37b018199ec3c9, via wewantmoore commit d59bd80ea93fabb9faf769e790ab47692645e022 (both Apache-2.0). The port adds the MooreBound namespace and updates Mathlib APIs and proof style. Wiener and Consequences retain the PNT and prime-interval dependency closure; unrelated later developments and LeanArchitect annotations are omitted.

@[instance_reducible]

def MooreBound.realFunctionComplexCoe {E : Type u_1} : Coe (E → ℝ) (E → ℂ)

Pointwise complexification of a real-valued function, local to the Fourier proofs.

Equations

• MooreBound.realFunctionComplexCoe = { coe := fun (f : E → ℝ) (n : E) => ↑(f n) }

theorem MooreBound.nnnorm_eq_of_mem_circle (z : Circle) : ‖↑z‖₊ = 1

theorem MooreBound.nnnorm_circle_smul (z : Circle) (s : ℂ) : ‖z • s‖₊ = ‖s‖₊

noncomputable def MooreBound.e (u : ℝ) : BoundedContinuousFunction ℝ ℂ

The negative-frequency Fourier character as a bounded continuous function.

Equations

• MooreBound.e u = { toFun := fun (v : ℝ) => ↑(Real.fourierChar (-v * u)), continuous_toFun := ⋯, map_bounded' := ⋯ }

@[simp]

theorem MooreBound.e_apply (u v : ℝ) : (e u) v = ↑(Real.fourierChar (-v * u))

theorem MooreBound.hasDerivAt_e {u x : ℝ} : HasDerivAt (⇑(e u)) (-2 * ↑Real.pi * ↑u * Complex.I * (e u) x) x

theorem MooreBound.fourierIntegral_deriv_aux2 (e : BoundedContinuousFunction ℝ ℂ) {f : ℝ → ℂ} (hf : MeasureTheory.Integrable f MeasureTheory.volume) : MeasureTheory.Integrable (⇑e * f) MeasureTheory.volume

@[simp]

theorem MooreBound.F_neg {f : ℝ → ℂ} {u : ℝ} : FourierTransform.fourier (fun (x : ℝ) => -f x) u = -FourierTransform.fourier f u

@[simp]

theorem MooreBound.F_add {f g : ℝ → ℂ} (hf : MeasureTheory.Integrable f MeasureTheory.volume) (hg : MeasureTheory.Integrable g MeasureTheory.volume) (x : ℝ) : FourierTransform.fourier (fun (x : ℝ) => f x + g x) x = FourierTransform.fourier f x + FourierTransform.fourier g x

@[simp]

theorem MooreBound.F_sub {f g : ℝ → ℂ} (hf : MeasureTheory.Integrable f MeasureTheory.volume) (hg : MeasureTheory.Integrable g MeasureTheory.volume) (x : ℝ) : FourierTransform.fourier (fun (x : ℝ) => f x - g x) x = FourierTransform.fourier f x - FourierTransform.fourier g x

@[simp]

theorem MooreBound.F_mul {f : ℝ → ℂ} {c : ℂ} {u : ℝ} : FourierTransform.fourier (fun (x : ℝ) => c * f x) u = c * FourierTransform.fourier f u

theorem MooreBound.fourierIntegral_self_add_deriv_deriv (f : W21) (u : ℝ) : (1 + ↑u ^ 2) * FourierTransform.fourier f.toFun u = FourierTransform.fourier (fun (u : ℝ) => f.toFun u - 1 / (4 * ↑Real.pi ^ 2) * deriv^[2] f.toFun u) u

@[simp]

theorem MooreBound.deriv_ofReal : deriv Complex.ofReal = fun (x : ℝ) => 1

theorem MooreBound.tendsto_intervalIntegral_zero_of_uniform_norm_bound {f : ℝ → ℝ → ℂ} {lo hi : ℝ} {B : ℝ → ℝ} (hB : Filter.Tendsto (fun (T : ℝ) => B T * |hi - lo|) Filter.atTop (nhds 0)) (hf : ∀ᶠ (T : ℝ) in Filter.atTop, ∀ x ∈ Set.uIoc lo hi, ‖f T x‖ ≤ B T) : Filter.Tendsto (fun (T : ℝ) => ∫ (x : ℝ) in lo..hi, f T x) Filter.atTop (nhds 0)

If, eventually in T, the integrand f T is bounded on uIoc lo hi by B T and B T * |hi - lo| → 0, then the interval integral ∫ x in lo..hi, f T x → 0.

theorem MooreBound.tendsto_const_mul_log_add_two_div_add_two_atTop (K : ℝ) : Filter.Tendsto (fun (T : ℝ) => K * (Real.log (T + 2) / (T + 2))) Filter.atTop (nhds 0)

The decay K * (log (T + 2) / (T + 2)) → 0 as T → ∞, for any constant K.

theorem MooreBound.norm_fourier_le_integral_deriv_div (g : ℝ → ℂ) (hg : MeasureTheory.Integrable g MeasureTheory.volume) (hdiff : Differentiable ℝ g) (hg' : MeasureTheory.Integrable (deriv g) MeasureTheory.volume) {w : ℝ} (hw : w ≠ 0) : ‖FourierTransform.fourier g w‖ ≤ (∫ (x : ℝ), ‖deriv g x‖) / (2 * Real.pi * |w|)

Fourier-transform decay from an integrable derivative: for integrable, differentiable g with integrable derivative, ‖𝓕 g w‖ ≤ (∫ ‖deriv g x‖) / (2π·|w|).

theorem MooreBound.norm_oscillatory_integral_le_integral_deriv_div (g : ℝ → ℂ) (hg : MeasureTheory.Integrable g MeasureTheory.volume) (hdiff : Differentiable ℝ g) (hg' : MeasureTheory.Integrable (deriv g) MeasureTheory.volume) {T : ℝ} (hT : 0 < T) : ‖∫ (y : ℝ), g y * Complex.exp (↑T * Complex.I * ↑y)‖ ≤ (∫ (x : ℝ), ‖deriv g x‖) / T

The oscillatory-integral form of the decay bound: for 0 < T, ‖∫ g y · exp(T·i·y)‖ ≤ (∫ ‖deriv g x‖) / T.

theorem MooreBound.norm_oscillatory_integral_le_integral_deriv_div_abs (g : ℝ → ℂ) (hg : MeasureTheory.Integrable g MeasureTheory.volume) (hdiff : Differentiable ℝ g) (hg' : MeasureTheory.Integrable (deriv g) MeasureTheory.volume) {T : ℝ} (hT : T ≠ 0) : ‖∫ (y : ℝ), g y * Complex.exp (↑T * Complex.I * ↑y)‖ ≤ (∫ (x : ℝ), ‖deriv g x‖) / |T|

The |T| variant of the oscillatory-integral decay bound: for T ≠ 0, ‖∫ g y · exp(T·i·y)‖ ≤ (∫ ‖deriv g x‖) / |T|.