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.

theorem MooreBound.smooth_urysohn_support_Ioo {a b c d : ℝ} (h1 : a < b) (h3 : c < d) : ∃ (Ψ : ℝ → ℝ), ContDiff ℝ (↑⊤) Ψ ∧ HasCompactSupport Ψ ∧ (Set.Icc b c).indicator 1 ≤ Ψ ∧ Ψ ≤ (Set.Ioo a d).indicator 1 ∧ Function.support Ψ = Set.Ioo a d

theorem MooreBound.SmoothExistence : ∃ (ν : ℝ → ℝ), ContDiff ℝ (↑⊤) ν ∧ (∀ (x : ℝ), 0 ≤ ν x) ∧ Function.support ν ⊆ Set.Icc (1 / 2) 2 ∧ ∫ (x : ℝ) in Set.Ici 0, ν x / x = 1