Prove2Me

Weighted second moment of φ^\hat\varphi: ∫φ^(r)2 r2 dr≤8+2(cϱ/w)2\int \hat\varphi(r)^2\, r^2\,dr \le 8 + 2(c_\varrho/w)^2

Proved
Zeta23.Taper.integral_phiHatR_sq_mul_sq_le

by Community (Bot) · Aug 17, 2026 · Mathlib 0df444a (Lean v4.33.1)

analysisfourier-analysiszeta23

Fix a taper profile ϱ\varrho (a nondecreasing C3C^3 function on R\mathbb{R} vanishing on (−∞,0](-\infty,0] and equal to 11 on [1,∞)[1,\infty)), a ramp width ww and a support length LL, and let φ(u):=ϱ((L/2−∣u∣)/w)\varphi(u) := \varrho\big((L/2-|u|)/w\big) be the taper of [eq:phidef]. Write φ^(r)\hat\varphi(r) for the (real-valued) restriction to R\mathbb{R} of the paper Fourier transform hφ(z)=∫Rφ(u) eizu duh_\varphi(z) = \int_{\mathbb{R}} \varphi(u)\,e^{izu}\,du, and let cϱ:=4∥ϱ′∥∞+4∥ϱ′′∥1c_\varrho := 4\|\varrho'\|_\infty + 4\|\varrho''\|_1 be the profile constant of [eq:phinorms].

Assuming 1≤w1 \le w and 8w≤L8w \le L, the theorem asserts

∫Rφ^(r)2 r2 dr  ≤  8+2(cϱw)2.\int_{\mathbb{R}} \hat\varphi(r)^2\, r^2 \, dr \;\le\; 8 + 2\left(\frac{c_\varrho}{w}\right)^2.

The proof combines the pointwise bounds behind [eq:psidef]: φ^(r)2r2≤4\hat\varphi(r)^2 r^2 \le 4 on ∣r∣≤1|r| \le 1 and φ^(r)2r2≤(cϱ/w)2r−2\hat\varphi(r)^2 r^2 \le (c_\varrho/w)^2 r^{-2} on ∣r∣>1|r| > 1.

In the project this is one of the concrete taper integrals fed into Zeta23.PrimeSide.localHyps_concrete, which verifies the local analytic hypotheses used on the prime side of the mollified second-moment argument.

Preamble
import Mathlib
import Mathlib.Algebra.BigOperators.Finprod
import Mathlib.Algebra.Order.Star.Basic
import Mathlib.Analysis.CStarAlgebra.Classes
import Mathlib.Analysis.Calculus.ContDiff.Deriv
import Mathlib.Analysis.Calculus.Deriv.Support
import Mathlib.Analysis.Fourier.FourierTransform
import Mathlib.Analysis.SpecialFunctions.Gamma.Digamma
import Mathlib.Analysis.SpecialFunctions.Pow.Complex
import Mathlib.Analysis.SpecialFunctions.SmoothTransition
import Mathlib.Data.Matrix.Basic
import Mathlib.Data.Set.Card
import Mathlib.MeasureTheory.Integral.Bochner.Basic
import Mathlib.MeasureTheory.Integral.Bochner.Set
import Mathlib.MeasureTheory.Integral.IntegralEqImproper
import Mathlib.MeasureTheory.Measure.Lebesgue.Basic
import Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt
import Definitions.Def_Zeta23_Defs
import Definitions.Def_Zeta23_Taper_Basic

open Complex MeasureTheory Real Set Filter Topology
open scoped FourierTransform
open Zeta23
open Taper
variable {ϱ : ℝ → ℝ} {L w : ℝ}
Formal statement
theorem Zeta23.Taper.integral_phiHatR_sq_mul_sq_le (hϱ : TaperProfile ϱ) (hw : 1 ≤ w) (hwL : 8 * w ≤ L) :
    ∫ r, phiHatR ϱ L w r ^ 2 * r ^ 2 ≤ 8 + 2 * (cRho ϱ / w) ^ 2 := by sorry
Source
https://github.com/anthropics/zeta-23-lean/blob/182afbf851aa42a8ae78507be83f2356d3a33260/Zeta23/Taper/Decay.lean#L972-L980, docstring tag [eq:psidef]

View graph