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.

structure MooreBound.CS (n : ℕ) (E : Type u_2) [NormedAddCommGroup E] [NormedSpace ℝ E] : Type u_2

A function with n continuous derivatives and compact support.

• toFun : ℝ → E

  The underlying compactly supported function.

• h1 : ContDiff ℝ (↑n) self.toFun
• h2 : HasCompactSupport self.toFun

theorem MooreBound.CS.ext_iff {n : ℕ} {E : Type u_2} {inst✝ : NormedAddCommGroup E} {inst✝¹ : NormedSpace ℝ E} {x y : CS n E} : x = y ↔ x.toFun = y.toFun

theorem MooreBound.CS.ext {n : ℕ} {E : Type u_2} {inst✝ : NormedAddCommGroup E} {inst✝¹ : NormedSpace ℝ E} {x y : CS n E} (toFun : x.toFun = y.toFun) : x = y

structure MooreBound.truncextends MooreBound.CS 2 ℝ : Type

A compactly supported C² cutoff equal to one on [-1,1] and zero outside (-2,2).

• toFun : ℝ → ℝ
• h1 : ContDiff ℝ (↑2) self.toFun
• h2 : HasCompactSupport self.toFun
• h3 : (Set.Icc (-1) 1).indicator 1 ≤ self.toFun
• h4 : self.toFun ≤ (Set.Ioo (-2) 2).indicator 1

structure MooreBound.W1 (n : ℕ) (E : Type u_2) [NormedAddCommGroup E] [NormedSpace ℝ E] : Type u_2

A Cⁿ function whose derivatives through order n are integrable.

• toFun : ℝ → E

  The underlying function with integrable derivatives.

• smooth : ContDiff ℝ (↑n) self.toFun
• integrable ⦃k : ℕ⦄ : k ≤ n → MeasureTheory.Integrable (iteratedDeriv k self.toFun) MeasureTheory.volume

@[reducible, inline]

abbrev MooreBound.W21 : Type

Complex C² functions with integrable derivatives through order two.

Equations

• MooreBound.W21 = MooreBound.W1 2 ℂ

noncomputable def MooreBound.funscale {E : Type u_2} (g : ℝ → E) (R x : ℝ) : E

Precompose a function with multiplication by the reciprocal scale.

Equations

• MooreBound.funscale g R x = g (R⁻¹ • x)

theorem MooreBound.contDiff_ofReal : ContDiff ℝ (↑⊤) Complex.ofReal

theorem MooreBound.tendsto_funscale {E : Type u_1} [NormedAddCommGroup E] {f : ℝ → E} (hf : ContinuousAt f 0) (x : ℝ) : Filter.Tendsto (fun (R : ℝ) => funscale f R x) Filter.atTop (nhds (f 0))

@[instance_reducible]

instance MooreBound.CS.instCoeFunForallReal {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : ℕ} : CoeFun (CS n E) fun (x : CS n E) => ℝ → E

Equations

• MooreBound.CS.instCoeFunForallReal = { coe := MooreBound.CS.toFun }

@[instance_reducible]

instance MooreBound.CS.instCoeRealComplex {n : ℕ} : Coe (CS n ℝ) (CS n ℂ)

Equations

• MooreBound.CS.instCoeRealComplex = { coe := fun (f : MooreBound.CS n ℝ) => { toFun := fun (x : ℝ) => ↑(f.toFun x), h1 := ⋯, h2 := ⋯ } }

def MooreBound.CS.neg {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : ℕ} (f : CS n E) : CS n E

Pointwise negation preserves smoothness and compact support.

Equations

• f.neg = { toFun := -f.toFun, h1 := ⋯, h2 := ⋯ }

@[instance_reducible]

instance MooreBound.CS.instNeg {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : ℕ} : Neg (CS n E)

Equations

• MooreBound.CS.instNeg = { neg := MooreBound.CS.neg }

@[simp]

theorem MooreBound.CS.neg_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : ℕ} {f : CS n E} {x : ℝ} : (-f).toFun x = -f.toFun x

def MooreBound.CS.smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : ℕ} (R : ℝ) (f : CS n E) : CS n E

Multiply a compactly supported smooth function by a real scalar.

Equations

• MooreBound.CS.smul R f = { toFun := R • f.toFun, h1 := ⋯, h2 := ⋯ }

@[instance_reducible]

instance MooreBound.CS.instHSMulReal {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : ℕ} : HSMul ℝ (CS n E) (CS n E)

Equations

• MooreBound.CS.instHSMulReal = { hSMul := MooreBound.CS.smul }

@[simp]

theorem MooreBound.CS.smul_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : ℕ} {f : CS n E} {R x : ℝ} : (R • f).toFun x = R • f.toFun x

theorem MooreBound.CS.continuous {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : ℕ} (f : CS n E) : Continuous f.toFun

noncomputable def MooreBound.CS.deriv {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : ℕ} (f : CS (n + 1) E) : CS n E

Differentiate a compactly supported function, lowering its smoothness index.

Equations

• f.deriv = { toFun := deriv f.toFun, h1 := ⋯, h2 := ⋯ }

theorem MooreBound.CS.hasDerivAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : ℕ} (f : CS (n + 1) E) (x : ℝ) : HasDerivAt f.toFun (f.deriv.toFun x) x

theorem MooreBound.CS.deriv_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : ℕ} {f : CS (n + 1) E} {x : ℝ} : f.deriv.toFun x = _root_.deriv f.toFun x

theorem MooreBound.CS.deriv_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : ℕ} {R : ℝ} {f : CS (n + 1) E} : (R • f).deriv = R • f.deriv

noncomputable def MooreBound.CS.scale {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : ℕ} (g : CS n E) (R : ℝ) : CS n E

Rescale a compactly supported function; use the zero function at scale zero.

Equations

• g.scale R = if h : R = 0 then { toFun := 0, h1 := ⋯, h2 := ⋯ } else { toFun := fun (x : ℝ) => MooreBound.funscale g.toFun R x, h1 := ⋯, h2 := ⋯ }

theorem MooreBound.CS.deriv_scale {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : ℕ} {R : ℝ} {f : CS (n + 1) E} : (f.scale R).deriv = R⁻¹ • f.deriv.scale R

theorem MooreBound.CS.deriv_scale' {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : ℕ} {R v : ℝ} {f : CS (n + 1) E} : (f.scale R).deriv.toFun v = R⁻¹ • f.deriv.toFun (R⁻¹ • v)

theorem MooreBound.CS.hasDerivAt_scale {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : ℕ} (f : CS (n + 1) E) (R x : ℝ) : HasDerivAt (f.scale R).toFun (R⁻¹ • _root_.deriv f.toFun (R⁻¹ • x)) x

theorem MooreBound.CS.tendsto_scale {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : ℕ} (f : CS n E) (x : ℝ) : Filter.Tendsto (fun (R : ℝ) => (f.scale R).toFun x) Filter.atTop (nhds (f.toFun 0))

theorem MooreBound.CS.bounded {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : ℕ} {f : CS n E} : ∃ (C : ℝ), ∀ (v : ℝ), ‖f.toFun v‖ ≤ C

@[instance_reducible]

instance MooreBound.trunc.instCoeFunForallReal : CoeFun trunc fun (x : trunc) => ℝ → ℝ

Equations

• MooreBound.trunc.instCoeFunForallReal = { coe := fun (f : MooreBound.trunc) => f.toFun }

@[instance_reducible]

instance MooreBound.trunc.instCoeCSOfNatNatReal : Coe trunc (CS 2 ℝ)

Equations

• MooreBound.trunc.instCoeCSOfNatNatReal = { coe := MooreBound.trunc.toCS }

theorem MooreBound.trunc.nonneg (g : trunc) (x : ℝ) : 0 ≤ g.toFun x

theorem MooreBound.trunc.le_one (g : trunc) (x : ℝ) : g.toFun x ≤ 1

theorem MooreBound.trunc.zero (g : trunc) : g.toFun =ᶠ[nhds 0] 1

@[simp]

theorem MooreBound.trunc.zero_at {g : trunc} : g.toFun 0 = 1

@[instance_reducible]

instance MooreBound.W1.instCoeFunForallReal {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : ℕ} : CoeFun (W1 n E) fun (x : W1 n E) => ℝ → E

Equations

• MooreBound.W1.instCoeFunForallReal = { coe := MooreBound.W1.toFun }

theorem MooreBound.W1.continuous {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : ℕ} (f : W1 n E) : Continuous f.toFun

theorem MooreBound.W1.differentiable {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : ℕ} (f : W1 (n + 1) E) : Differentiable ℝ f.toFun

theorem MooreBound.W1.iteratedDeriv_sub {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : ℕ} {f g : ℝ → E} (hf : ContDiff ℝ (↑n) f) (hg : ContDiff ℝ (↑n) g) : iteratedDeriv n (f - g) = iteratedDeriv n f - iteratedDeriv n g

noncomputable def MooreBound.W1.deriv {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : ℕ} (f : W1 (n + 1) E) : W1 n E

Differentiate a function with integrable derivatives, lowering its index.

Equations

• f.deriv = { toFun := deriv f.toFun, smooth := ⋯, integrable := ⋯ }

theorem MooreBound.W1.hasDerivAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : ℕ} (f : W1 (n + 1) E) (x : ℝ) : HasDerivAt f.toFun (f.deriv.toFun x) x

def MooreBound.W1.sub {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : ℕ} (f g : W1 n E) : W1 n E

Subtract two functions with integrable derivatives.

Equations

• f.sub g = { toFun := f.toFun - g.toFun, smooth := ⋯, integrable := ⋯ }

@[instance_reducible]

instance MooreBound.W1.instSub {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : ℕ} : Sub (W1 n E)

Equations

• MooreBound.W1.instSub = { sub := MooreBound.W1.sub }

theorem MooreBound.W1.integrable_iteratedDeriv_Schwarz {n : ℕ} {f : SchwartzMap ℝ ℂ} : MeasureTheory.Integrable (iteratedDeriv n ⇑f) MeasureTheory.volume

noncomputable def MooreBound.W1.ofSchwartz {n : ℕ} (f : SchwartzMap ℝ ℂ) : W1 n ℂ

A Schwartz function has integrable derivatives of every finite order.

Equations

• MooreBound.W1.ofSchwartz f = { toFun := ⇑f, smooth := ⋯, integrable := ⋯ }

noncomputable def MooreBound.W21.norm (f : ℝ → ℂ) : ℝ

The L¹ size of a function plus the scaled L¹ size of its second derivative.

Equations

• MooreBound.W21.norm f = (∫ (v : ℝ), ‖f v‖) + (4 * Real.pi ^ 2)⁻¹ * ∫ (v : ℝ), ‖deriv (deriv f) v‖

theorem MooreBound.W21.norm_nonneg {f : ℝ → ℂ} : 0 ≤ norm f

@[instance_reducible]

noncomputable instance MooreBound.W21.instNorm : Norm W21

Equations

• MooreBound.W21.instNorm = { norm := MooreBound.W21.norm ∘ MooreBound.W1.toFun }

@[instance_reducible]

noncomputable instance MooreBound.W21.instCoeSchwartzMapRealComplex : Coe (SchwartzMap ℝ ℂ) W21

Equations

• MooreBound.W21.instCoeSchwartzMapRealComplex = { coe := MooreBound.W1.ofSchwartz }

def MooreBound.W21.ofCS2 (f : CS 2 ℂ) : W21

Regard a compactly supported C² function as an element of W21.

Equations

• MooreBound.W21.ofCS2 f = { toFun := f.toFun, smooth := ⋯, integrable := ⋯ }

@[instance_reducible]

instance MooreBound.W21.instCoeCSOfNatNatComplex : Coe (CS 2 ℂ) W21

Equations

• MooreBound.W21.instCoeCSOfNatNatComplex = { coe := MooreBound.W21.ofCS2 }

@[instance_reducible]

instance MooreBound.W21.instHMulCSOfNatNatComplex : HMul (CS 2 ℂ) W21 (CS 2 ℂ)

Equations

• MooreBound.W21.instHMulCSOfNatNatComplex = { hMul := fun (g : MooreBound.CS 2 ℂ) (f : MooreBound.W21) => { toFun := g.toFun * f.toFun, h1 := ⋯, h2 := ⋯ } }

@[instance_reducible]

instance MooreBound.W21.instHMulCSOfNatNatRealComplex : HMul (CS 2 ℝ) W21 (CS 2 ℂ)

Equations

• MooreBound.W21.instHMulCSOfNatNatRealComplex = { hMul := fun (g : MooreBound.CS 2 ℝ) (f : MooreBound.W21) => { toFun := fun (x : ℝ) => ↑(g.toFun x), h1 := ⋯, h2 := ⋯ } * f }

theorem MooreBound.W21.hf (f : W21) : MeasureTheory.Integrable f.toFun MeasureTheory.volume

theorem MooreBound.W21.hf' (f : W21) : MeasureTheory.Integrable (deriv f.toFun) MeasureTheory.volume

theorem MooreBound.W21.hf'' (f : W21) : MeasureTheory.Integrable (deriv (deriv f.toFun)) MeasureTheory.volume

theorem MooreBound.W21_approximation (f : W21) (g : trunc) : Filter.Tendsto (fun (R : ℝ) => ‖f - W21.ofCS2 (g.scale R * f)‖) Filter.atTop (nhds 0)