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.Function.support_id {α : Type u_1} [Zero α] : Function.support id = {0}ᶜ

theorem MooreBound.Function.support_id' {α : Type u_2} [Zero α] : (Function.support fun (x : α) => x) = {0}ᶜ